RAM snapshot word-width decoder — proof internals #
The proof constructs the exact scanner, successor-body, and loopback frames
needed by TM.ForWorkOnesLoopSpec. The only changed tapes are the source
cursor and the canonical binary width counter.
theorem
Complexity.RAM.RegisterStore.Machine.wordTargetRewind_reachesIn_frame_internal
{n : ℕ}
(targetIdx : Fin n)
(bits : List Bool)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(htarget : (work₀ targetIdx).HasBinaryPrefix bits)
(htargetStart : (work₀ targetIdx).cells 0 = Γ.start)
(hinput : inp₀.read ≠ Γ.start)
(hother : ∀ (i : Fin n), i ≠ targetIdx → (work₀ i).read ≠ Γ.start ∧ 1 ≤ (work₀ i).head)
(houtput : out₀.read ≠ Γ.start)
(houtputHead : 1 ≤ out₀.head)
:
∃ (c' : Cfg n (TM.rewindWorkTM targetIdx).Q),
∃ t ≤ bits.length + 3,
(TM.rewindWorkTM targetIdx).reachesIn t
{ state := (TM.rewindWorkTM targetIdx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (TM.rewindWorkTM targetIdx).halted c' ∧ c'.input = inp₀ ∧ (c'.work targetIdx).HasBinaryString bits ∧ (∀ (i : Fin n), i ≠ targetIdx → c'.work i = work₀ i) ∧ c'.output = out₀
theorem
Complexity.RAM.RegisterStore.Machine.payloadBitTM_reachesIn_frame_internal
{n : ℕ}
(sourceIdx targetIdx : Fin n)
(hindices : sourceIdx ≠ targetIdx)
(bit : Bool)
(suffix pre : List Bool)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(hsource : (work₀ sourceIdx).HasBinarySuffix (bit :: suffix))
(htarget : (work₀ targetIdx).HasBinaryPrefix pre)
(hinput : inp₀.read ≠ Γ.start)
(hother : ∀ (i : Fin n), i ≠ sourceIdx → i ≠ targetIdx → (work₀ i).read ≠ Γ.start)
(houtput : out₀.read ≠ Γ.start)
:
∃ (c' : Cfg n (payloadBitTM sourceIdx targetIdx).Q),
(payloadBitTM sourceIdx targetIdx).reachesIn 1
{ state := (payloadBitTM sourceIdx targetIdx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (payloadBitTM sourceIdx targetIdx).halted c' ∧ c'.input = inp₀ ∧ (c'.work sourceIdx).HasBinarySuffix suffix ∧ (c'.work targetIdx).HasBinaryPrefix (pre ++ [bit]) ∧ (∀ (i : Fin n), i ≠ sourceIdx → i ≠ targetIdx → c'.work i = work₀ i) ∧ c'.output = out₀
theorem
Complexity.RAM.RegisterStore.Machine.wordSeparatorTM_reachesIn_frame_internal
{n : ℕ}
(sourceIdx : Fin n)
(bits : List Bool)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(hsource : (work₀ sourceIdx).HasBinarySuffix (false :: bits))
(hinput : inp₀.read ≠ Γ.start)
(hother : ∀ (i : Fin n), i ≠ sourceIdx → (work₀ i).read ≠ Γ.start)
(houtput : out₀.read ≠ Γ.start)
:
∃ (c' : Cfg n (wordSeparatorTM sourceIdx).Q),
(wordSeparatorTM sourceIdx).reachesIn 1
{ state := (wordSeparatorTM sourceIdx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (wordSeparatorTM sourceIdx).halted c' ∧ c'.input = inp₀ ∧ (c'.work sourceIdx).HasBinarySuffix bits ∧ (∀ (i : Fin n), i ≠ sourceIdx → c'.work i = work₀ i) ∧ c'.output = out₀
theorem
Complexity.RAM.RegisterStore.Machine.wordPayloadTM_reachesIn_frame_internal
{n : ℕ}
(sourceIdx targetIdx counterIdx widthIdx : Fin n)
(hdistinct : PayloadLoopDistinct sourceIdx targetIdx counterIdx widthIdx)
(payload rest : List Bool)
(width : ℕ)
(hwidthLength : payload.length = width)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(hsource : (work₀ sourceIdx).HasBinarySuffix (payload ++ rest))
(htarget : (work₀ targetIdx).HasBinaryPrefix [])
(hcounter : (work₀ counterIdx).HasBinaryNat 0)
(hwidth : (work₀ widthIdx).HasBinaryNat width)
(hinput : inp₀.read ≠ Γ.start)
(hother : ∀ (i : Fin n), i ≠ sourceIdx → i ≠ targetIdx → i ≠ counterIdx → i ≠ widthIdx → (work₀ i).read ≠ Γ.start)
(houtput : out₀.read ≠ Γ.start)
:
∃ (c' : Cfg n (wordPayloadTM sourceIdx targetIdx counterIdx widthIdx).Q),
(wordPayloadTM sourceIdx targetIdx counterIdx widthIdx).reachesIn (wordPayloadTime width)
{ state := (wordPayloadTM sourceIdx targetIdx counterIdx widthIdx).qstart, input := inp₀, work := work₀,
output := out₀ }
c' ∧ (wordPayloadTM sourceIdx targetIdx counterIdx widthIdx).halted c' ∧ c'.input = inp₀ ∧ (c'.work sourceIdx).HasBinarySuffix rest ∧ (c'.work targetIdx).HasBinaryPrefix payload ∧ (c'.work counterIdx).HasBinaryNat width ∧ (c'.work widthIdx).HasBinaryNat width ∧ (∀ (i : Fin n), i ≠ sourceIdx → i ≠ targetIdx → i ≠ counterIdx → i ≠ widthIdx → c'.work i = work₀ i) ∧ c'.output = out₀
theorem
Complexity.RAM.RegisterStore.Machine.wordWidthTM_reachesIn_frame_internal
{n : ℕ}
(sourceIdx widthIdx : Fin n)
(hindices : sourceIdx ≠ widthIdx)
(width : ℕ)
(payload : List Bool)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(hsource : (work₀ sourceIdx).HasBinarySuffix (List.replicate width true ++ false :: payload))
(hwidth : (work₀ widthIdx).HasBinaryNat 0)
(hinput : inp₀.read ≠ Γ.start)
(hother : ∀ (i : Fin n), i ≠ sourceIdx → i ≠ widthIdx → (work₀ i).read ≠ Γ.start)
(houtput : out₀.read ≠ Γ.start)
:
∃ (c' : Cfg n (wordWidthTM sourceIdx widthIdx).Q),
(wordWidthTM sourceIdx widthIdx).reachesIn (wordWidthTime width)
{ state := (wordWidthTM sourceIdx widthIdx).qstart, input := inp₀, work := work₀, output := out₀ } c' ∧ (wordWidthTM sourceIdx widthIdx).halted c' ∧ c'.input = inp₀ ∧ (c'.work sourceIdx).HasBinarySuffix (false :: payload) ∧ (c'.work widthIdx).HasBinaryNat width ∧ (∀ (i : Fin n), i ≠ sourceIdx → i ≠ widthIdx → c'.work i = work₀ i) ∧ c'.output = out₀
theorem
Complexity.RAM.RegisterStore.Machine.wordDecodeTM_reachesIn_frame_internal
{n : ℕ}
(sourceIdx targetIdx counterIdx widthIdx : Fin n)
(hdistinct : PayloadLoopDistinct sourceIdx targetIdx counterIdx widthIdx)
(payload rest : List Bool)
(width : ℕ)
(hwidthLength : payload.length = width)
(inp₀ : Tape)
(work₀ : Fin n → Tape)
(out₀ : Tape)
(hsource : (work₀ sourceIdx).HasBinarySuffix (List.replicate width true ++ false :: (payload ++ rest)))
(htarget : (work₀ targetIdx).HasBinaryPrefix [])
(hcounter : (work₀ counterIdx).HasBinaryNat 0)
(hwidth : (work₀ widthIdx).HasBinaryNat 0)
(hinput : inp₀.read ≠ Γ.start)
(hother : ∀ (i : Fin n), i ≠ sourceIdx → i ≠ targetIdx → i ≠ counterIdx → i ≠ widthIdx → (work₀ i).read ≠ Γ.start)
(houtput : out₀.read ≠ Γ.start)
:
∃ (c' : Cfg n (wordDecodeTM sourceIdx targetIdx counterIdx widthIdx).Q),
(wordDecodeTM sourceIdx targetIdx counterIdx widthIdx).reachesIn (wordDecodeTime width)
{ state := (wordDecodeTM sourceIdx targetIdx counterIdx widthIdx).qstart, input := inp₀, work := work₀,
output := out₀ }
c' ∧ (wordDecodeTM sourceIdx targetIdx counterIdx widthIdx).halted c' ∧ c'.input = inp₀ ∧ (c'.work sourceIdx).HasBinarySuffix rest ∧ (c'.work targetIdx).HasBinaryPrefix payload ∧ (c'.work counterIdx).HasBinaryNat width ∧ (c'.work widthIdx).HasBinaryNat width ∧ (∀ (i : Fin n), i ≠ sourceIdx → i ≠ targetIdx → i ≠ counterIdx → i ≠ widthIdx → c'.work i = work₀ i) ∧ c'.output = out₀
theorem
Complexity.RAM.RegisterStore.Machine.wordWidthTM_isTransducer_internal
{n : ℕ}
(sourceIdx widthIdx : Fin n)
:
(wordWidthTM sourceIdx widthIdx).IsTransducer
theorem
Complexity.RAM.RegisterStore.Machine.payloadBitTM_isTransducer_internal
{n : ℕ}
(sourceIdx targetIdx : Fin n)
:
(payloadBitTM sourceIdx targetIdx).IsTransducer
theorem
Complexity.RAM.RegisterStore.Machine.wordSeparatorTM_isTransducer_internal
{n : ℕ}
(sourceIdx : Fin n)
:
(wordSeparatorTM sourceIdx).IsTransducer
theorem
Complexity.RAM.RegisterStore.Machine.wordPayloadTM_isTransducer_internal
{n : ℕ}
(sourceIdx targetIdx counterIdx widthIdx : Fin n)
:
(wordPayloadTM sourceIdx targetIdx counterIdx widthIdx).IsTransducer
theorem
Complexity.RAM.RegisterStore.Machine.wordDecodeTM_isTransducer_internal
{n : ℕ}
(sourceIdx targetIdx counterIdx widthIdx : Fin n)
:
(wordDecodeTM sourceIdx targetIdx counterIdx widthIdx).IsTransducer