The bounded-iteration machine — proof internals

Complexity.Cobham.iterate_mem_FP needs one machine: given a polynomial-time G, a machine that applies G to its own input |x| times. This file builds it out of the phase contracts of Complexitylib.Classes.P.Cobham.Internal.IterateLayout.

Layout

Three bookkeeping tapes (rfIdx the loop's fuel register, wfIdx the reset's fuel register, junkIdx scratch for the register arithmetic) followed by TM.applyTM's own block (appIdx), whose virtual input vinIdx carries the running value and whose last tape resIdx receives each result.

Phases

• Complexity.iterTail — the five phases that follow every application: park, rewind the result, blank the scratch, move the result into virtual-input position, blank the result tape. Shared by the loop body and the setup.
• Complexity.iterBody — one application of the iterated function followed by the tail; this is what the loop iterates.
• Complexity.iterSetup — bump, load |x| into the loop register, evaluate a padding polynomial into the reset register, put pair [] x on the result tape, then the tail.
• Complexity.iterTM — setup, loop, and one final application whose output is the real output tape.

A confinement frame for an arbitrary bounded run

Resetting the scratch of an opaque machine needs to know how far its heads can have travelled. Any b-step run from tapes parked at cell 1 and blank beyond it stays inside cell 1 + b.

theorem Complexity.hoareTime_confined {n : ℕ} {tm : TM n} {pre post : TapePred n} {b : ℕ} (h : tm.HoareTime pre post b) (W : Fin n → Tape) (H : ℕ) (hH : 1 + b ≤ H) (S : Fin n → Prop) (hWSI : ∀ (i : Fin n), (W i).StartInvariant) (hWh : ∀ (i : Fin n), S i → (W i).head = 1) (hWfar : ∀ (i : Fin n), S i → ∀ (j : ℕ), 1 < j → (W i).cells j = Γ.blank) : tm.HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => pre inp work out ∧ work = W ∧ inp.StartInvariant ∧ out.StartInvariant) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => post inp work out ∧ inp.StartInvariant ∧ out.StartInvariant ∧ ∀ (i : Fin n), (work i).StartInvariant ∧ (S i → (work i).head ≤ H ∧ ∀ (j : ℕ), H < j → (work i).cells j = Γ.blank)) b

Every bounded run is confined. From work tapes parked at cell 1 whose content is confined to cell 1, a b-step run leaves every work tape inside H and blank beyond H.

The shared tail

Every application of the iterated function — the loop body's, and the setup's pair [] x — leaves its result on resIdx with the scratch dirty. The five phases below restore the entry shape TM.applyPre demands.

def Complexity.iterTail (k : ℕ) : TM (3 + (k + 2) + 0)

Park, rewind the result, blank the witness machine's scratch and the virtual input, move the result into virtual-input position, blank the result tape.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.tailBound (k H m : ℕ) : ℕ

Complexity.iterTail's time bound.

Equations

• Complexity.tailBound k H m = 1 + 1 + (H + 1 + 2) + 1 + ((k + 1) * (H + 4) + H * 4 + 8 + 1 + ((k + 1) * (H + 4) + 1)) + 1 + (2 * m + 5 + 1 + (1 * (H + 4) + H * 4 + 8 + 1 + (1 * (H + 4) + 1)))

theorem Complexity.startInvariant_regTape (H : ℕ) : (TM.regTape H).StartInvariant

theorem Complexity.iterTail_hoareTime {k : ℕ} (M : TM k) (H : ℕ) (v : List Bool) (hv : v.length + 1 ≤ H) (inp₀ : Tape) (hinpP : TM.Parked inp₀) (hinpSI : inp₀.StartInvariant) (rfT junkT : Tape) (hrfP : TM.Parked rfT) (hrfSI : rfT.StartInvariant) (hjunkP : TM.Parked junkT) (hjunkSI : junkT.StartInvariant) : (iterTail k).HoareTime (fun (inp : Tape) (work : Fin (3 + (k + 2) + 0) → Tape) (out : Tape) => inp = inp₀ ∧ out = TM.parkedBlank ∧ (work resIdx).HasOutput v ∧ (∀ (j : Fin (k + 2)), (work (appIdx j)).StartInvariant ∧ (work (appIdx j)).head ≤ H ∧ ∀ (c : ℕ), H < c → (work (appIdx j)).cells c = Γ.blank) ∧ work rfIdx = rfT ∧ work wfIdx = TM.regTape H ∧ work junkIdx = junkT) (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 v inp₀ j) (tailBound k H v.length)

The tail's contract. From a result tape carrying v and a block whose tapes are confined to 1 … H, the five phases rebuild TM.applyPre M v.

One iteration

The loop body is one application of the iterated function followed by the tail.

theorem Complexity.transitionTape_of_startInvariant {t : Tape} (h : t.StartInvariant) : TM.transitionTape t = { head := max t.head 1, cells := t.cells }

One combinator seam on a tape satisfying the left-marker invariant: the cells are untouched and the head only ever bounces off ▷.

def Complexity.bookTapes {k : ℕ} (rfT junkT : Tape) (H : ℕ) : Fin (3 + (k + 2) + 0) → Tape

The three bookkeeping tapes, packaged as a placement frame.

Equations

• Complexity.bookTapes rfT junkT H i = if i = Complexity.rfIdx then rfT else if i = Complexity.wfIdx then Complexity.TM.regTape H else junkT

@[simp]

theorem Complexity.bookTapes_rf {k : ℕ} (rfT junkT : Tape) (H : ℕ) : bookTapes rfT junkT H rfIdx = rfT

@[simp]

theorem Complexity.bookTapes_wf {k : ℕ} (rfT junkT : Tape) (H : ℕ) : bookTapes rfT junkT H wfIdx = TM.regTape H

@[simp]

theorem Complexity.bookTapes_junk {k : ℕ} (rfT junkT : Tape) (H : ℕ) : bookTapes rfT junkT H junkIdx = junkT

theorem Complexity.eq_bookTapes_of_not_middle {k : ℕ} {work : Fin (3 + (k + 2) + 0) → Tape} {rfT junkT : Tape} {H : ℕ} (hrf : work rfIdx = rfT) (hwf : work wfIdx = TM.regTape H) (hjunk : work junkIdx = junkT) (i : Fin (3 + (k + 2) + 0)) : ¬TM.placeWorkInMiddle 3 (k + 2) i → work i = bookTapes rfT junkT H i

theorem Complexity.bookTapes_startInvariant {k : ℕ} {rfT junkT : Tape} {H : ℕ} (hrfSI : rfT.StartInvariant) (hjunkSI : junkT.StartInvariant) (i : Fin (3 + (k + 2) + 0)) : ¬TM.placeWorkInMiddle 3 (k + 2) i → (bookTapes rfT junkT H i).StartInvariant

theorem Complexity.bookTapes_head {k : ℕ} {rfT junkT : Tape} {H : ℕ} (hrfP : TM.Parked rfT) (hjunkP : TM.Parked junkT) (i : Fin (3 + (k + 2) + 0)) : ¬TM.placeWorkInMiddle 3 (k + 2) i → 1 ≤ (bookTapes rfT junkT H i).head

def Complexity.iterBody {k : ℕ} (M : TM k) : TM (3 + (k + 2) + 0)

The loop body: apply the iterated function once, then restore the entry shape.

Equations

• Complexity.iterBody M = (Complexity.TM.placeWorkTM 3 0 M.applyTM).seqTM (Complexity.iterTail k)

theorem Complexity.iterBody_hoareTime {k : ℕ} (M : TM k) {G : List Bool → List Bool} {T : ℕ → ℕ} (hcomp : M.ComputesInTime G T) (H : ℕ) (y : List Bool) (hHy : y.length ≤ H) (hHT : 1 + T y.length ≤ H) (hGy : (G y).length + 1 ≤ H) (inp₀ : Tape) (hinpP : TM.Parked inp₀) (hinpSI : inp₀.StartInvariant) (rfT junkT : Tape) (hrfP : TM.Parked rfT) (hrfSI : rfT.StartInvariant) (hjunkP : TM.Parked junkT) (hjunkSI : junkT.StartInvariant) : (iterBody M).HoareTime (fun (inp : Tape) (work : Fin (3 + (k + 2) + 0) → Tape) (out : Tape) => inp = inp₀ ∧ out = TM.parkedBlank ∧ (∀ (j : Fin (k + 2)), work (appIdx j) = M.applyPre y inp₀ j) ∧ work rfIdx = rfT ∧ work wfIdx = TM.regTape H ∧ work junkIdx = junkT) (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 (G y) inp₀ j) (T y.length + 1 + tailBound k H (G y).length)

The body's contract. From the entry shape for y, the body reaches the entry shape for G y, holding both registers and the junk tape fixed.

The loop

TM.forRegTM drives the body once per mark of the fuel register rfIdx, threading the iteration-indexed ghost family below.

def Complexity.iterFamily {k : ℕ} (M : TM k) (Y : ℕ → List Bool) (inp₀ junkT : Tape) (v H : ℕ) : ℕ → Fin (3 + (k + 2) + 0) → Tape

The whole tape family at iteration i: the entry shape for the i-th iterate on TM.applyTM's block, the two registers, and the junk tape.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Complexity.iterFamily_app {k : ℕ} {M : TM k} {Y : ℕ → List Bool} {inp₀ junkT : Tape} {v H : ℕ} (i : ℕ) (j : Fin (k + 2)) : iterFamily M Y inp₀ junkT v H i (appIdx j) = M.applyPre (Y i) inp₀ j

theorem Complexity.iterFamily_book {k : ℕ} {M : TM k} {Y : ℕ → List Bool} {inp₀ junkT : Tape} {v H : ℕ} (i : ℕ) (j : Fin (3 + (k + 2) + 0)) (hj : ¬TM.placeWorkInMiddle 3 (k + 2) j) : iterFamily M Y inp₀ junkT v H i j = bookTapes (TM.regTape v) junkT H j

@[simp]

theorem Complexity.iterFamily_rf {k : ℕ} {M : TM k} {Y : ℕ → List Bool} {inp₀ junkT : Tape} {v H : ℕ} (i : ℕ) : iterFamily M Y inp₀ junkT v H i rfIdx = TM.regTape v

@[simp]

theorem Complexity.iterFamily_wf {k : ℕ} {M : TM k} {Y : ℕ → List Bool} {inp₀ junkT : Tape} {v H : ℕ} (i : ℕ) : iterFamily M Y inp₀ junkT v H i wfIdx = TM.regTape H

@[simp]

theorem Complexity.iterFamily_junk {k : ℕ} {M : TM k} {Y : ℕ → List Bool} {inp₀ junkT : Tape} {v H : ℕ} (i : ℕ) : iterFamily M Y inp₀ junkT v H i junkIdx = junkT

theorem Complexity.iterFamily_parked {k : ℕ} {M : TM k} {Y : ℕ → List Bool} {inp₀ junkT : Tape} {v H : ℕ} (hjunkP : TM.Parked junkT) (i : ℕ) (j : Fin (3 + (k + 2) + 0)) (hj : j ≠ rfIdx) : TM.Parked (iterFamily M Y inp₀ junkT v H i j)

theorem Complexity.iterLoop_hoareTime {k : ℕ} {M : TM k} {Y : ℕ → List Bool} {inp₀ junkT : Tape} {v H : ℕ} {G : List Bool → List Bool} {T : ℕ → ℕ} (hcomp : M.ComputesInTime G T) (hY : ∀ (i : ℕ), Y (i + 1) = G (Y i)) (hlen : ∀ i ≤ v, (Y i).length + 1 ≤ H) (hT : ∀ i < v, 1 + T (Y i).length ≤ H) (b_iter : ℕ) (hb : ∀ i < v, T (Y i).length + 1 + tailBound k H (Y (i + 1)).length ≤ b_iter) (hinpP : TM.Parked inp₀) (hinpSI : inp₀.StartInvariant) (hjunkP : TM.Parked junkT) (hjunkSI : junkT.StartInvariant) : ((iterBody M).forRegTM rfIdx).HoareTime (TM.EmitPred inp₀ (iterFamily M Y inp₀ junkT v H 0) []) (TM.EmitPred inp₀ (iterFamily M Y inp₀ junkT v H v) []) (v * (b_iter + 2) + (v + 2))

The loop's contract. v applications of the iterated function, each returning the block to its entry shape.

The setup

Bump, load |x| into the loop register, evaluate the padding polynomial into the reset register, and put pair [] x on the result tape.

@[simp]

theorem Complexity.parkedBlank_head : TM.parkedBlank.head = 1

theorem Complexity.parkedBlank_cells (j : ℕ) : TM.parkedBlank.cells j = if j = 0 then Γ.start else Γ.blank

theorem Complexity.hasOutput_nil_parkedBlank : TM.parkedBlank.HasOutput []

def Complexity.emitStart {k : ℕ} (extras : Fin (3 + (k + 2) + 0) → Tape) : Fin (3 + (k + 2) + 0) → Tape

The tape family the emission phase starts from: TM.applyTM's block blank, the bookkeeping tapes as given.

Equations

• Complexity.emitStart extras i = if Complexity.TM.placeWorkInMiddle 3 (k + 2) i then Complexity.TM.parkedBlank else extras i

theorem Complexity.emitStart_middle {k : ℕ} (extras : Fin (3 + (k + 2) + 0) → Tape) (j : Fin (k + 2)) : emitStart extras (appIdx j) = TM.parkedBlank

theorem Complexity.emitStart_extra {k : ℕ} (extras : Fin (3 + (k + 2) + 0) → Tape) (i : Fin (3 + (k + 2) + 0)) (hi : ¬TM.placeWorkInMiddle 3 (k + 2) i) : emitStart extras i = extras i

theorem Complexity.placedEmit_hoareTime {k : ℕ} (x : List Bool) (H : ℕ) (hH : x.length + 4 ≤ 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 (TM.pairInputWorkTM (Fin.last k)).retargetOutput).HoareTime (fun (inp : Tape) (work : Fin (3 + (k + 1 + 1) + 0) → Tape) (out : Tape) => inp = (Tape.init (List.map Γ.ofBool x)).move Dir3.right ∧ out = TM.parkedBlank ∧ work = emitStart extras) (fun (inp : Tape) (work : Fin (3 + (k + 1 + 1) + 0) → Tape) (out : Tape) => inp.StartInvariant ∧ out = TM.parkedBlank ∧ (work resIdx).HasOutput (pair [] x) ∧ (∀ (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) (x.length + 3)

The setup's emission phase. From the bumped input holding x and an all-blank block, pair [] x lands on the result tape and the whole block stays inside H.

theorem Complexity.parkedBlank_eq_regTape_zero : TM.parkedBlank = TM.regTape 0

def Complexity.polyM (p : Polynomial ℕ) (n : ℕ) : ℕ

The register value cap the padding polynomial's evaluation runs under.

Equations

• Complexity.polyM p n = ((Complexity.TM.polyCoeffs p).sum + 1) * (n + 1) ^ (Complexity.TM.polyCoeffs p).length + n + Polynomial.eval n p

def Complexity.iterSetup (k : ℕ) (p : Polynomial ℕ) : TM (3 + (k + 2) + 0)

The setup machine: bump every head off cell 0, load |x| into the loop register, evaluate the padding polynomial into the reset register, and emit pair [] x onto the result tape.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.setupBound (p : Polynomial ℕ) (n : ℕ) : ℕ

Complexity.iterSetup's time bound.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.iterSetup_hoareTime {k : ℕ} (p : Polynomial ℕ) (x : List Bool) (H : ℕ) (hH : H = Polynomial.eval x.length p) (hHx : x.length + 4 ≤ H) : (iterSetup k p).HoareTime (fun (inp : Tape) (work : Fin (3 + (k + 2) + 0) → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool x) ∧ (work = fun (x : Fin (3 + (k + 2) + 0)) => Tape.init []) ∧ out = Tape.init []) (fun (inp : Tape) (work : Fin (3 + (k + 2) + 0) → Tape) (out : Tape) => inp.StartInvariant ∧ out = TM.parkedBlank ∧ (work resIdx).HasOutput (pair [] x) ∧ (∀ (j : Fin (k + 2)), (work (appIdx j)).StartInvariant ∧ (work (appIdx j)).head ≤ H ∧ ∀ (c : ℕ), H < c → (work (appIdx j)).cells c = Γ.blank) ∧ work rfIdx = TM.regTape x.length ∧ work wfIdx = TM.regTape H ∧ work junkIdx = TM.regTape H) (setupBound p x.length)

The whole machine

Setup, loop, and one final application whose output lands on the real output tape. Over-iteration is harmless, so that last application is just one more iteration.

theorem Complexity.not_middle_succ_cases {k : ℕ} (i : Fin (3 + (k + 2) + 0)) (hi : ¬TM.placeWorkInMiddle 3 (k + 1) i) : i = rfIdx ∨ i = wfIdx ∨ i = junkIdx ∨ i = resIdx

def Complexity.teardownExtras {k : ℕ} (v H : ℕ) : Fin (3 + (k + 2) + 0) → Tape

The frame of the final application: the three bookkeeping tapes and the result tape, which the last application no longer needs.

Equations

• Complexity.teardownExtras v H i = if i = Complexity.resIdx then Complexity.TM.parkedBlank else Complexity.bookTapes (Complexity.TM.regTape v) (Complexity.TM.regTape H) H i

def Complexity.iterMain {k : ℕ} (M : TM k) : TM (3 + (k + 2) + 0)

Setup, loop, and the final application.

Equations

• Complexity.iterMain M = ((Complexity.iterTail k).seqTM ((Complexity.iterBody M).forRegTM Complexity.rfIdx)).seqTM (Complexity.TM.placeWorkTM 3 1 M.retargetInputStarted)

theorem Complexity.iterMain_hoareTime {k : ℕ} (M : TM k) {G : List Bool → List Bool} {T : ℕ → ℕ} (hcomp : M.ComputesInTime G T) (H v : ℕ) (Y : ℕ → List Bool) (hY : ∀ (i : ℕ), Y (i + 1) = G (Y i)) (hlen : ∀ i ≤ v, (Y i).length + 1 ≤ H) (hT : ∀ i < v, 1 + T (Y i).length ≤ H) (b_iter : ℕ) (hb : ∀ i < v, T (Y i).length + 1 + tailBound k H (Y (i + 1)).length ≤ b_iter) : (iterMain M).HoareTime (fun (inp : Tape) (work : Fin (3 + (k + 2) + 0) → Tape) (out : Tape) => TM.Parked inp ∧ inp.StartInvariant ∧ out = TM.parkedBlank ∧ (work resIdx).HasOutput (Y 0) ∧ (∀ (j : Fin (k + 2)), (work (appIdx j)).StartInvariant ∧ (work (appIdx j)).head ≤ H ∧ ∀ (c : ℕ), H < c → (work (appIdx j)).cells c = Γ.blank) ∧ work rfIdx = TM.regTape v ∧ work wfIdx = TM.regTape H ∧ work junkIdx = TM.regTape H) (fun (_inp : Tape) (_work : Fin (3 + (k + 2) + 0) → Tape) (out : Tape) => out.HasOutput (G (Y v))) (tailBound k H (Y 0).length + 1 + (v * (b_iter + 2) + (v + 2)) + 1 + T (Y v).length)

The main run. From the result tape carrying the initial value, the machine iterates v + 1 times and writes the last value to the real output.

def Complexity.iterTM {k : ℕ} (M : TM k) (p : Polynomial ℕ) : TM (3 + (k + 2) + 0)

The complete iteration machine.

Equations

• Complexity.iterTM M p = (Complexity.iterSetup k p).seqTM (Complexity.iterMain M)

theorem Complexity.tailBound_mono (k H : ℕ) {m m' : ℕ} (h : m ≤ m') : tailBound k H m ≤ tailBound k H m'

def Complexity.iterBound (k : ℕ) (tp p r : Polynomial ℕ) (n : ℕ) : ℕ

Complexity.iterTM's time bound.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.iterTM_computesInTime {k : ℕ} (M : TM k) {G : List Bool → List Bool} {tp : Polynomial ℕ} (hcomp : M.ComputesInTime G fun (x : ℕ) => Polynomial.eval x tp) (p r : Polynomial ℕ) (hp₁ : ∀ (n : ℕ), n + 4 ≤ Polynomial.eval n p) (hp₂ : ∀ (n : ℕ), Polynomial.eval n r + 1 ≤ Polynomial.eval n p) (hp₃ : ∀ (n : ℕ), 1 + Polynomial.eval (Polynomial.eval n r) tp ≤ Polynomial.eval n p) (hr : ∀ (x : List Bool), ∀ i ≤ x.length, (G^[i] (pair [] x)).length ≤ Polynomial.eval x.length r) : (iterTM M p).ComputesInTime (fun (x : List Bool) => G^[x.length + 1] (pair [] x)) (iterBound k tp p r)

The iteration machine computes the iterate. On input x it applies G to pair [] x exactly |x| + 1 times, provided the padding polynomial p dominates the length bound r and the source machine's own bound tp.

Polynomial bounds

Complexity.iterBound is a sum of products of polynomial evaluations, so the closure API of Complexitylib.Asymptotics.PolyBound bounds it directly.

theorem Complexity.polyBound_iterBound (k : ℕ) (tp p r : Polynomial ℕ) : PolyBound (iterBound k tp p r)

theorem Complexity.iterate_input_mem_FP {G : List Bool → List Bool} (hG : G ∈ FP) (r : Polynomial ℕ) (hr : ∀ (x : List Bool), ∀ i ≤ x.length, (G^[i] (pair [] x)).length ≤ Polynomial.eval x.length r) : (fun (x : List Bool) => G^[x.length + 1] (pair [] x)) ∈ FP

FP is closed under iterating a polynomial-time function once per input bit, provided every intermediate value stays polynomially bounded.