The bounded-iteration machine's tape layout — proof internals

The tape layout and phase contracts that Complexitylib.Classes.P.Cobham.Internal.Iterate assembles into the bounded-iteration machine: two unary fuel registers (one consumed by the outer loop, one reused by every reset), one junk tape for the register arithmetic, and then TM.applyTM's own tapes placed after them. The running value needs no tape of its own — it lives on applyTM's virtual-input tape, which is exactly where the next call wants it.

Main results

• Complexity.rfIdx, wfIdx, junkIdx, appIdx, vinIdx, resIdx — the layout
• Complexity.placedApply_hoareTime — one embedded application of the iterated function
• Complexity.iterPark_hoareTime, iterResetScratch_hoareTime, iterFinish_hoareTime — the phase contracts around it

def Complexity.rfIdx {k : ℕ} : Fin (3 + (k + 2) + 0)

The outer loop's fuel register.

Equations

• Complexity.rfIdx = ⟨0, ⋯⟩

def Complexity.wfIdx {k : ℕ} : Fin (3 + (k + 2) + 0)

The reset's fuel register, restored by every reset.

Equations

• Complexity.wfIdx = ⟨1, ⋯⟩

def Complexity.junkIdx {k : ℕ} : Fin (3 + (k + 2) + 0)

Holds the input's padding block; never read again.

Equations

• Complexity.junkIdx = ⟨2, ⋯⟩

def Complexity.appIdx {k : ℕ} (j : Fin (k + 2)) : Fin (3 + (k + 2) + 0)

Where TM.applyTM's tape j sits in the composite layout.

Equations

• Complexity.appIdx j = Complexity.TM.placeWorkIdx 3 0 j

def Complexity.vinIdx {k : ℕ} : Fin (3 + (k + 2) + 0)

The running value's tape — applyTM's virtual input.

Equations

• Complexity.vinIdx = Complexity.appIdx (Fin.last k).castSucc

def Complexity.resIdx {k : ℕ} : Fin (3 + (k + 2) + 0)

Where one application of the iterated function leaves its result.

Equations

• Complexity.resIdx = Complexity.appIdx (Fin.last (k + 1))

@[simp]

theorem Complexity.rfIdx_val {k : ℕ} : ↑rfIdx = 0

@[simp]

theorem Complexity.wfIdx_val {k : ℕ} : ↑wfIdx = 1

@[simp]

theorem Complexity.junkIdx_val {k : ℕ} : ↑junkIdx = 2

@[simp]

theorem Complexity.appIdx_val {k : ℕ} (j : Fin (k + 2)) : ↑(appIdx j) = 3 + ↑j

theorem Complexity.not_middle_iff {k : ℕ} (i : Fin (3 + (k + 2) + 0)) : ¬TM.placeWorkInMiddle 3 (k + 2) i ↔ ↑i < 3

The three bookkeeping tapes are exactly the ones outside applyTM's block.

theorem Complexity.appIdx_middle {k : ℕ} (j : Fin (k + 2)) : TM.placeWorkInMiddle 3 (k + 2) (appIdx j)

theorem Complexity.appIdx_injective {k : ℕ} : Function.Injective appIdx

theorem Complexity.rfIdx_not_middle {k : ℕ} : ¬TM.placeWorkInMiddle 3 (k + 2) rfIdx

theorem Complexity.wfIdx_not_middle {k : ℕ} : ¬TM.placeWorkInMiddle 3 (k + 2) wfIdx

theorem Complexity.junkIdx_not_middle {k : ℕ} : ¬TM.placeWorkInMiddle 3 (k + 2) junkIdx

theorem Complexity.wfIdx_ne_appIdx {k : ℕ} (j : Fin (k + 2)) : wfIdx ≠ appIdx j

theorem Complexity.rfIdx_ne_appIdx {k : ℕ} (j : Fin (k + 2)) : rfIdx ≠ appIdx j

theorem Complexity.junkIdx_ne_appIdx {k : ℕ} (j : Fin (k + 2)) : junkIdx ≠ appIdx j

theorem Complexity.layout_cases {k : ℕ} (i : Fin (3 + (k + 2) + 0)) : i = rfIdx ∨ i = wfIdx ∨ i = junkIdx ∨ ∃ (j : Fin (k + 2)), i = appIdx j

The layout is exhaustive. Every tape of the composite machine is one of the three bookkeeping tapes or one of TM.applyTM's own, so a predicate that names all four kinds pins down the whole tape family.

theorem Complexity.placedApply_hoareTime {k : ℕ} (M : TM k) {G : List Bool → List Bool} {T : ℕ → ℕ} (hcomp : M.ComputesInTime G T) (y : List Bool) (inp₀ : Tape) (hinp : TM.Parked inp₀) (hinpSI : inp₀.StartInvariant) (H : ℕ) (hHy : y.length ≤ H) (hHT : 1 + T y.length ≤ H) (extras : Fin (3 + (k + 2) + 0) → Tape) (hextraSI : ∀ (i : Fin (3 + (k + 2) + 0)), ¬TM.placeWorkInMiddle 3 (k + 2) i → (extras i).StartInvariant) (hextraH : ∀ (i : Fin (3 + (k + 2) + 0)), ¬TM.placeWorkInMiddle 3 (k + 2) i → 1 ≤ (extras i).head) : (TM.placeWorkTM 3 0 M.applyTM).HoareTime (fun (inp : Tape) (work : Fin (3 + (k + 2) + 0) → Tape) (out : Tape) => inp = inp₀ ∧ (∀ (j : Fin (k + 2)), work (appIdx j) = M.applyPre y inp₀ j) ∧ (∀ (i : Fin (3 + (k + 2) + 0)), ¬TM.placeWorkInMiddle 3 (k + 2) i → work i = extras i) ∧ out = TM.parkedBlank) (fun (inp : Tape) (work : Fin (3 + (k + 2) + 0) → Tape) (out : Tape) => inp = inp₀ ∧ out = TM.parkedBlank ∧ (work resIdx).HasOutput (G y) ∧ (∀ (j : Fin (k + 2)), (work (appIdx j)).StartInvariant ∧ (work (appIdx j)).head ≤ H ∧ ∀ (c : ℕ), H < c → (work (appIdx j)).cells c = Γ.blank) ∧ ∀ (i : Fin (3 + (k + 2) + 0)), ¬TM.placeWorkInMiddle 3 (k + 2) i → work i = extras i) (T y.length)

One application of the iterated function, in the composite layout. The bookkeeping tapes are held fixed; applyTM's block goes from its entry shape for y to a state where the result tape holds G y and every tape of the block is still confined to cells 1 … H — the two facts Complexity.resetTapesTM needs to clean up afterwards.

def Complexity.resetTargets (k : ℕ) : List (Fin (3 + (k + 2) + 0))

The tapes cleaned between two applications of the iterated function: the witness machine's own scratch together with the virtual-input tape. The result tape is deliberately excluded — it still carries the value being moved.

Equations

• Complexity.resetTargets k = List.map (fun (j : Fin (k + 1)) => Complexity.appIdx j.castSucc) (List.finRange (k + 1))

theorem Complexity.resetTargets_nodup {k : ℕ} : (resetTargets k).Nodup

@[simp]

theorem Complexity.resetTargets_length {k : ℕ} : (resetTargets k).length = k + 1

theorem Complexity.mem_resetTargets_iff {k : ℕ} (i : Fin (3 + (k + 2) + 0)) : i ∈ resetTargets k ↔ ∃ (j : Fin (k + 1)), appIdx j.castSucc = i

theorem Complexity.wfIdx_notMem_resetTargets {k : ℕ} : wfIdx ∉ resetTargets k

theorem Complexity.resIdx_notMem_resetTargets {k : ℕ} : resIdx ∉ resetTargets k

theorem Complexity.vinIdx_mem_resetTargets {k : ℕ} : vinIdx ∈ resetTargets k

def Complexity.resetResult (k : ℕ) : List (Fin (3 + (k + 2) + 0))

The tape cleaned after the result has been moved back.

Equations

• Complexity.resetResult k = [Complexity.resIdx]

theorem Complexity.resetResult_nodup {k : ℕ} : (resetResult k).Nodup

theorem Complexity.wfIdx_notMem_resetResult {k : ℕ} : wfIdx ∉ resetResult k

theorem Complexity.iterPark_hoareTime {k : ℕ} (H : ℕ) (inp₀ : Tape) (hinpP : TM.Parked inp₀) (hinpSI : inp₀.StartInvariant) (W : Fin (3 + (k + 2) + 0) → Tape) (hSI : ∀ (i : Fin (3 + (k + 2) + 0)), (W i).StartInvariant) (hB : (W resIdx).head ≤ H) : (TM.skipTM.seqTM (TM.rewindWorkTM resIdx)).HoareTime (fun (inp : Tape) (work : Fin (3 + (k + 2) + 0) → Tape) (out : Tape) => inp = inp₀ ∧ work = W ∧ out = TM.parkedBlank) (fun (inp : Tape) (work : Fin (3 + (k + 2) + 0) → Tape) (out : Tape) => inp = inp₀ ∧ out = TM.parkedBlank ∧ (work resIdx).head = 1 ∧ (work resIdx).cells = (W resIdx).cells ∧ ∀ (i : Fin (3 + (k + 2) + 0)), i ≠ resIdx → work i = { head := max (W i).head 1, cells := (W i).cells }) (1 + 1 + (H + 1 + 2))

Phases 2–3 of the body. δ_right_of_start only constrains a head that reads ▷, so an arbitrary witness machine may halt with a head parked on cell 0. One idle step lifts every head to at least cell 1, and one rewind then brings the result tape's head back to exactly cell 1 — the shape both Complexity.resetTapesTM (which preserves non-target tapes only when they are parked) and TM.copyWorkToWorkTM (which wants its source at cell 1) require.

theorem Complexity.rfIdx_ne_wfIdx {k : ℕ} : rfIdx ≠ wfIdx

theorem Complexity.junkIdx_ne_wfIdx {k : ℕ} : junkIdx ≠ wfIdx

theorem Complexity.resIdx_ne_wfIdx {k : ℕ} : resIdx ≠ wfIdx

theorem Complexity.rfIdx_notMem_resetTargets {k : ℕ} : rfIdx ∉ resetTargets k

theorem Complexity.junkIdx_notMem_resetTargets {k : ℕ} : junkIdx ∉ resetTargets k

theorem Complexity.iterResetScratch_hoareTime {k : ℕ} (H : ℕ) (hH : 1 ≤ H) (inp₀ : Tape) (hinpP : TM.Parked inp₀) (hinpSI : inp₀.StartInvariant) (W : Fin (3 + (k + 2) + 0) → Tape) (hSI : ∀ (i : Fin (3 + (k + 2) + 0)), (W i).StartInvariant) (hB : ∀ (j : Fin (k + 1)), (W (appIdx j.castSucc)).head ≤ H) (hfar : ∀ (j : Fin (k + 1)) (c : ℕ), H < c → (W (appIdx j.castSucc)).cells c = Γ.blank) (hwf : W wfIdx = TM.regTape H) : (TM.resetTapesTM (resetTargets k) wfIdx).HoareTime (fun (inp : Tape) (work : Fin (3 + (k + 2) + 0) → Tape) (out : Tape) => inp = inp₀ ∧ out = TM.parkedBlank ∧ (work resIdx).head = 1 ∧ (work resIdx).cells = (W resIdx).cells ∧ ∀ (i : Fin (3 + (k + 2) + 0)), i ≠ resIdx → work i = { head := max (W i).head 1, cells := (W i).cells }) (fun (inp : Tape) (work : Fin (3 + (k + 2) + 0) → Tape) (out : Tape) => inp = inp₀ ∧ out = TM.parkedBlank ∧ (work resIdx).head = 1 ∧ (work resIdx).cells = (W resIdx).cells ∧ (∀ (j : Fin (k + 1)), work (appIdx j.castSucc) = TM.parkedBlank) ∧ work wfIdx = TM.regTape H ∧ work rfIdx = { head := max (W rfIdx).head 1, cells := (W rfIdx).cells } ∧ work junkIdx = { head := max (W junkIdx).head 1, cells := (W junkIdx).cells }) ((k + 1) * (H + 4) + H * 4 + 8 + 1 + ((k + 1) * (H + 4) + 1))

Phase 4 of the body. Blank the witness machine's scratch tapes and the virtual-input tape, leaving the result tape (which carries the value being moved), both fuel registers, and the junk tape exactly as they were.

theorem Complexity.applyPre_eq {k : ℕ} (M : TM k) (x : List Bool) (inp₀ : Tape) (j : Fin (k + 2)) : M.applyPre x inp₀ j = if j = (Fin.last k).castSucc then (Tape.init (List.map Γ.ofBool x)).move Dir3.right else TM.parkedBlank

TM.applyPre in closed form: the virtual-input tape carries the value, and every other tape of the block is blank.

theorem Complexity.resIdx_ne_vinIdx {k : ℕ} : resIdx ≠ vinIdx

theorem Complexity.rfIdx_ne_resIdx {k : ℕ} : rfIdx ≠ resIdx

theorem Complexity.junkIdx_ne_resIdx {k : ℕ} : junkIdx ≠ resIdx

theorem Complexity.wfIdx_ne_resIdx {k : ℕ} : wfIdx ≠ resIdx

theorem Complexity.rfIdx_ne_vinIdx {k : ℕ} : rfIdx ≠ vinIdx

theorem Complexity.junkIdx_ne_vinIdx {k : ℕ} : junkIdx ≠ vinIdx

theorem Complexity.wfIdx_ne_vinIdx {k : ℕ} : wfIdx ≠ vinIdx

theorem Complexity.junkIdx_ne_rfIdx {k : ℕ} : junkIdx ≠ rfIdx

theorem Complexity.iterFinish_hoareTime {k : ℕ} (M : TM k) (H : ℕ) (x : List Bool) (hx : x.length + 1 ≤ H) (inp₀ : Tape) (hinpP : TM.Parked inp₀) (hinpSI : inp₀.StartInvariant) (resT rfT junkT : Tape) (hresH : resT.head = 1) (hresOut : resT.HasOutput x) (hresSI : resT.StartInvariant) (hresFar : ∀ (c : ℕ), H < c → resT.cells c = Γ.blank) (hrfP : TM.Parked rfT) (hrfSI : rfT.StartInvariant) (hjunkP : TM.Parked junkT) (hjunkSI : junkT.StartInvariant) : ((TM.copyToVirtualInputTM resIdx vinIdx).seqTM (TM.resetTapesTM (resetResult k) wfIdx)).HoareTime (fun (inp : Tape) (work : Fin (3 + (k + 2) + 0) → Tape) (out : Tape) => inp = inp₀ ∧ out = TM.parkedBlank ∧ work resIdx = resT ∧ work rfIdx = rfT ∧ work junkIdx = junkT ∧ work wfIdx = TM.regTape H ∧ ∀ (j : Fin (k + 1)), work (appIdx j.castSucc) = TM.parkedBlank) (fun (inp : Tape) (work : Fin (3 + (k + 2) + 0) → Tape) (out : Tape) => inp = inp₀ ∧ out = TM.parkedBlank ∧ work rfIdx = rfT ∧ work junkIdx = junkT ∧ work wfIdx = TM.regTape H ∧ ∀ (j : Fin (k + 2)), work (appIdx j) = M.applyPre x inp₀ j) (2 * x.length + 5 + 1 + (1 * (H + 4) + H * 4 + 8 + 1 + (1 * (H + 4) + 1)))

Phases 5–6 of the body. Move the freshly computed value from the result tape onto the virtual-input tape — where the next application will read it — and then blank the result tape, restoring TM.applyPre's entry shape for the new value.