Assembling the counting loop's body

⚠️ Unreviewed by Bolton

The loop invariant names every tape: the counter and the two tallies carry their numbers, the horizon and the wipe's register carry theirs, and everything else rests blank. This file records what that bank looks like at each named index and proves the body's stages against it.

Main results

• NTM.bodyBank — the bank the loop invariant pins, with its value at every named index
• NTM.blankSlot_hoareTime — the body's first stage: blank the verdict slot
• NTM.publish_hoareTime — the stage that copies the verdict into the output slot
• NTM.simCfg_entry — the simulation stage is entered on exactly the loop's own bank
• NTM.afterSim, NTM.simTM_hoareTime — the tape state the simulation stage leaves the body in
• NTM.afterPark, NTM.parkStage_hoareTime — the cleanup stage that follows it
• NTM.afterPublish, NTM.publishStage_hoareTime — the stage that publishes the verdict
• NTM.afterBump, NTM.bumpStage_hoareTime — the arithmetic stage
• NTM.wipeStage_hoareTime — the wipe, which returns the bank to the loop invariant's shape
• NTM.afterSim_trans, NTM.afterPark_trans, NTM.afterPublish_trans, NTM.afterBump_trans — the body's intermediate states survive a phase boundary
• NTM.bodyTM, NTM.bodyTM_hoareTime, NTM.bodyTM_hoareTime_mid — the loop's body, its contract, and that contract in the shape the loop rule asks for
• NTM.tallyLoop_full, NTM.tallyLoop_full_bounded — body and test together, running the tally to its horizon, with both running times written in terms of the horizon alone
• NTM.tallyLoop_keepsWindow_bounded, NTM.tallyLoop_keepsWindowOn — and the loop's space bound at the same layout, packaged for composition
• NTM.prologueTM, NTM.prologueTM_hoareTime — the machine's prologue and its contract
• NTM.ppPark_hoareTime, NTM.ppMachine, NTM.ppMachine_hoareTime — the parking step, the whole counting machine, and its contract
• NTM.loopEpilogue_keepsWindowOn, NTM.prologueRest_keepsWindowOn, NTM.ppMachine_keepsWindow — the parts composed in space, and the whole machine's window
• NTM.lt_iff_succ_sub_eq_zero, NTM.epilogueTM — the comparison the machine ends with
• NTM.epiloguePreTM_hoareTime — the epilogue's arithmetic
• NTM.epilogueEq_hoareTime — its comparison
• NTM.afterEq, NTM.epiloguePostTM_hoareTime — its publication
• NTM.epilogueTM_hoareTime, NTM.epilogueTM_keepsWindowOn — the three chained, in time and space
• NTM.binaryEqTime_le_of_le, NTM.bodyTime_le — the two running times are uniform over the loop
• NTM.bodyTM_keepsWindowOn — one pass of the body stays inside a window of its own width
• NTM.bodyBank_eq_of — the bridge from the wipe's result back to the loop invariant

def Complexity.NTM.bodyBank (k N H v a r : ℕ) : Fin (bodyTapes k) → Tape

The bank the loop invariant pins at count v with tallies a and r.

Equations

• Complexity.NTM.bodyBank k N H v a r = Complexity.tallyWork (Complexity.NTM.cIdx k) (Complexity.NTM.aIdx k) (Complexity.NTM.rIdx k) (Complexity.NTM.bodyRest k N H) (v, a, r)

theorem Complexity.NTM.bodyBank_cIdx (k N H v a r : ℕ) : bodyBank k N H v a r (cIdx k) = natTape v

theorem Complexity.NTM.bodyBank_aIdx (k N H v a r : ℕ) : bodyBank k N H v a r (aIdx k) = natTape a

theorem Complexity.NTM.bodyBank_rIdx (k N H v a r : ℕ) : bodyBank k N H v a r (rIdx k) = natTape r

theorem Complexity.NTM.bodyBank_rest (k N H v a r : ℕ) (j : Fin (bodyTapes k)) (hc : j ≠ cIdx k) (ha : j ≠ aIdx k) (hr : j ≠ rIdx k) : bodyBank k N H v a r j = bodyRest k N H j

theorem Complexity.NTM.bodyBank_parked (k N H v a r : ℕ) (j : Fin (bodyTapes k)) : TM.Parked (bodyBank k N H v a r j)

theorem Complexity.NTM.bodyBank_cells_zero (k N H v a r : ℕ) (j : Fin (bodyTapes k)) : (bodyBank k N H v a r j).cells 0 = Γ.start

theorem Complexity.NTM.bodyBank_startInvariant (k N H v a r : ℕ) (j : Fin (bodyTapes k)) : (bodyBank k N H v a r j).StartInvariant

theorem Complexity.NTM.bodyBank_wipeTarget (k N H v a r : ℕ) (j : Fin (bodyTapes k)) (hj : ↑j < k ∨ j = vIdx k) : bodyBank k N H v a r j = TM.blankTape

Every tape the body wipes rests blank in the loop's bank.

theorem Complexity.NTM.bodyBank_zIdx_read (k N H v a r : ℕ) : (bodyBank k N H v a r (zIdx k)).read = Γ.blank

The permanently blank register reads a blank, which is what makes it usable as the source of a blanking write.

theorem Complexity.NTM.blankSlot_hoareTime (k N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) : (TM.writeOutputBitTM (zIdx k)).HoareTime (fun (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) => inp = I ∧ work = bodyBank k N H v a r ∧ ∃ (s : Γw), s ≠ Γw.one ∧ out = outSlot s) (fun (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) => inp = I ∧ work = bodyBank k N H v a r ∧ out = outSlot Γw.blank) 1

The body's first stage: blank the verdict slot. The loop returns to its start state with the previous check's verdict still in the slot; the wipe that ends the body needs it blank, and so does the simulation, whose real output tape must start blank.

theorem Complexity.NTM.bodyBank_eq_of (k N H v a r : ℕ) (W : Fin (bodyTapes k) → Tape) (hc : W (cIdx k) = natTape v) (ha : W (aIdx k) = natTape a) (hr : W (rIdx k) = natTape r) (hn : W (nIdx k) = natTape N) (hreg : W (regIdx k) = TM.regTape H) (hrest : ∀ j ∉ wipeTargets k, j ≠ cIdx k → j ≠ aIdx k → j ≠ rIdx k → j ≠ nIdx k → j ≠ regIdx k → W j = TM.blankTape) : (fun (j : Fin (bodyTapes k)) => if j ∈ wipeTargets k then TM.blankTape else W j) = bodyBank k N H v a r

The bridge back to the loop invariant. After the body's wipe, a bank that carries the right numbers on the named registers and rests blank elsewhere is the bank the loop invariant pins at the next index.

theorem Complexity.NTM.simCfg_entry {k : ℕ} (tm : NTM k) (x : List Bool) (N H v a r : ℕ) (extras : Fin (0 + (k + 1) + 6) → Tape) (hex : ∀ (j : Fin (0 + (k + 1) + 6)), extras j = bodyBank k N H v a r j.castSucc) : tm.simCfg 6 extras (tm.simEntry x v) = { state := (tm.simTM 6).qstart, input := (Tape.init (List.map Γ.ofBool x)).move Dir3.right, work := bodyBank k N H v a r, output := TM.blankTape }

The stage's entry configuration is the loop's own bank. Placing the simulation beside the registers and redirecting its output puts exactly the tapes the loop invariant names where the stage expects them: the machine's own tapes blank, the counter at v, the registers untouched, and the verdict tape blank.

theorem Complexity.NTM.bodyBank_head (k N H v a r : ℕ) (j : Fin (bodyTapes k)) : (bodyBank k N H v a r j).head = 1

Every tape of the loop's bank is parked at cell one.

def Complexity.NTM.bodyInput (x : List Bool) : Tape

The real input tape, parked at cell one, with x on it.

Equations

• Complexity.NTM.bodyInput x = (Complexity.Tape.init (List.map Complexity.Γ.ofBool x)).move Complexity.Dir3.right

theorem Complexity.NTM.bodyInput_startInvariant (x : List Bool) : (bodyInput x).StartInvariant

@[simp]

theorem Complexity.NTM.bodyInput_head (x : List Bool) : (bodyInput x).head = 1

theorem Complexity.NTM.bodyInput_parked (x : List Bool) : TM.Parked (bodyInput x)

def Complexity.NTM.afterSim (k N H v a r T : ℕ) (I : Tape) (b : Bool) : TM.TapePred (bodyTapes k)

The tape state the simulation stage leaves the body in. Nothing is pinned but the registers: the simulated machine's tapes and the verdict tape hold whatever the run put there, and the heads are only bounded. What survives is enough — the counter's digits, the registers, the verdict bit, and a blank real output.

Equations

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

theorem Complexity.NTM.simTM_hoareTime {k : ℕ} (tm : NTM k) (x : List Bool) (hne : tm.qstart ≠ tm.qhalt) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (T v : ℕ) (hT : 1 ≤ T) (hfT : f x.length ≤ T) (N H a r : ℕ) : (tm.simTM 6).HoareTime (fun (inp : Tape) (work : Fin (0 + (k + 1) + 6 + 1) → Tape) (out : Tape) => inp = bodyInput x ∧ work = bodyBank k N H v a r ∧ out = TM.blankTape) (afterSim k N H v a r T (bodyInput x) (tm.acceptsAt x T v)) T

The simulation stage's contract. From the loop's bank with a blank output slot, the stage halts within the horizon and leaves the body in NTM.afterSim, carrying the acceptance bit of path v.

def Complexity.NTM.afterPark (k N H v a r T : ℕ) (I : Tape) (b : Bool) : TM.TapePred (bodyTapes k)

The tape state after the body's cleanup. Every head is parked, the counter has been rewound and reads as v again, and the verdict tape is at cell one so its bit can be published. The simulated machine's own tapes still hold whatever the run left; the wipe deals with them.

Equations

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

theorem Complexity.NTM.parkStage_hoareTime (k N H v a r T : ℕ) (I : Tape) (b : Bool) (hIhead : I.head = 1) (hcne : cIdx k ≠ vIdx k) : (TM.parkRewindTM [cIdx k, vIdx k]).HoareTime (afterSim k N H v a r T I b) (afterPark k N H v a r T I b) (1 + 1 + (2 * (max (1 + T + 2) (2 * (1 + T + 3) + 1) + 1) + 1))

The body's cleanup stage. It asks only for start-invariance, which is all a halted simulation guarantees, and returns the counter and the verdict tape at cell one.

def Complexity.NTM.afterPublish (k N H v a r T : ℕ) (I : Tape) (b : Bool) : TM.TapePred (bodyTapes k)

The tape state once the verdict is published. The slot now holds a symbol that is 1 exactly when the path accepted, which is what TM.ifTM branches on.

Equations

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

theorem Complexity.NTM.publishStage_hoareTime (k N H v a r T : ℕ) (I : Tape) (b : Bool) (hI : TM.Parked I) : (TM.writeOutputBitTM (vIdx k)).HoareTime (afterPark k N H v a r T I b) (afterPublish k N H v a r T I b) 1

The body's publishing stage. One transition copies the verdict tape's cell into the output slot; nothing else on any tape moves.

def Complexity.NTM.afterBump (k N H v a r T : ℕ) (I : Tape) (b : Bool) : TM.TapePred (bodyTapes k)

The tape state after the tallies are bumped. The count has advanced, the chosen tally has grown by one, and the verdict slot is blank again — ready for the wipe, which needs it so.

Equations

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

theorem Complexity.NTM.bumpStage_hoareTime (k N H v a r T : ℕ) (I : Tape) (b : Bool) (hI : TM.Parked I) (hIz : I.cells 0 = Γ.start) (hT : 1 ≤ T) : (TM.tallyBumpTM (cIdx k) (aIdx k) (rIdx k) (zIdx k)).HoareTime (afterPublish k N H v a r T I b) (afterBump k N H v a r T I b) (3 * (max (1 + 1 + max (TM.binarySuccTime a) (TM.binarySuccTime r) + 5) (TM.binarySuccTime v) + 1) + 1)

The body's arithmetic stage. The verdict in the slot picks which tally grows; the count grows too, and the slot is blanked on the way out.

theorem Complexity.NTM.wipeStage_hoareTime (k N T v a r : ℕ) (I : Tape) (b : Bool) (hIsi : I.StartInvariant) (hIp : TM.Parked I) : (TM.wipeRewindTM (wipeTargets k) (regIdx k)).HoareTime (afterBump k N (1 + T) v a r T I b) (fun (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) => inp = I ∧ work = bodyBank k N (1 + T) (v + 1) (a + if b = true then 1 else 0) (r + if b = true then 0 else 1) ∧ out = outSlot Γw.blank) ((wipeTargets k).length * (1 + T + 4) + (1 + T) * 4 + 8 + 1 + ((wipeTargets k).length * (1 + T + 4) + 1))

The body's last stage. Blanking the simulated machine's tapes and the verdict tape returns the bank to exactly the shape the loop invariant names — at the next index, with the tallies advanced. This is where the body closes.

theorem Complexity.NTM.afterSim_trans (k N H v a r T : ℕ) (I : Tape) (b : Bool) (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) (h : afterSim k N H v a r T I b inp work out) : afterSim k N H v a r T I b (TM.transitionInput inp) (fun (i : Fin (bodyTapes k)) => TM.transitionTape (work i)) (TM.transitionTape out)

The post-simulation state survives a phase boundary. It is stated in terms of cells and head bounds rather than exact tapes, which is what makes it stable: a transition preserves every cell and never pushes a head outward. A predicate that pinned the tapes could not survive here, because a halted simulation may leave a head on the marker, which the boundary then moves.

theorem Complexity.NTM.afterPark_trans (k N H v a r T : ℕ) (I : Tape) (b : Bool) (hI : TM.Parked I) (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) (h : afterPark k N H v a r T I b inp work out) : afterPark k N H v a r T I b (TM.transitionInput inp) (fun (i : Fin (bodyTapes k)) => TM.transitionTape (work i)) (TM.transitionTape out)

The pinned states between the body's later stages survive a phase boundary too, and for the easy reason: every tape they name is parked, so the boundary is the identity.

theorem Complexity.NTM.afterPublish_trans (k N H v a r T : ℕ) (I : Tape) (b : Bool) (hI : TM.Parked I) (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) (h : afterPublish k N H v a r T I b inp work out) : afterPublish k N H v a r T I b (TM.transitionInput inp) (fun (i : Fin (bodyTapes k)) => TM.transitionTape (work i)) (TM.transitionTape out)

The same, once the verdict is in the slot.

theorem Complexity.NTM.afterBump_trans (k N H v a r T : ℕ) (I : Tape) (b : Bool) (hI : TM.Parked I) (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) (h : afterBump k N H v a r T I b inp work out) : afterBump k N H v a r T I b (TM.transitionInput inp) (fun (i : Fin (bodyTapes k)) => TM.transitionTape (work i)) (TM.transitionTape out)

The same, once the tallies have been bumped.

def Complexity.NTM.bodyTM {k : ℕ} (tm : NTM k) : TM (bodyTapes k)

The counting loop's body. Blank the verdict slot, simulate one path, put the heads back, publish the verdict, bump the tallies and the count, and wipe the scratch tapes.

Equations

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

def Complexity.NTM.bodyTime (k T v a r : ℕ) : ℕ

The body's running time: the six stages plus the five transitions between them.

Equations

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

theorem Complexity.NTM.bodyTM_hoareTime {k : ℕ} (tm : NTM k) (x : List Bool) (hne : tm.qstart ≠ tm.qhalt) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (T v : ℕ) (hT : 1 ≤ T) (hfT : f x.length ≤ T) (N a r : ℕ) : tm.bodyTM.HoareTime (fun (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) => inp = bodyInput x ∧ work = bodyBank k N (1 + T) v a r ∧ ∃ (s : Γw), s ≠ Γw.one ∧ out = outSlot s) (fun (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) => inp = bodyInput x ∧ work = bodyBank k N (1 + T) (v + 1) (a + if tm.acceptsAt x T v = true then 1 else 0) (r + if tm.acceptsAt x T v = true then 0 else 1) ∧ out = outSlot Γw.blank) (bodyTime k T v a r)

The body's contract. One pass advances the count by one and the accepting or rejecting tally by one, according to whether the path selected by the counter accepts.

def Complexity.NTM.bodyMid (k N T : ℕ) (x : List Bool) (tm : NTM k) (v : ℕ) : TM.TapePred (bodyTapes k)

The tape state the body hands to the test: the bank at the next index, verdict slot blank.

Equations

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

theorem Complexity.NTM.bodyTM_hoareTime_mid {k : ℕ} (tm : NTM k) (x : List Bool) (hne : tm.qstart ≠ tm.qhalt) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (T : ℕ) (hT : 1 ≤ T) (hfT : f x.length ≤ T) (N bBody v : ℕ) (hbound : bodyTime k T v (tally (tm.acceptsAt x T) v) (tally (fun (u : ℕ) => !tm.acceptsAt x T u) v) ≤ bBody) : tm.bodyTM.HoareTime (tallyPre (cIdx k) (aIdx k) (rIdx k) (bodyInput x) (bodyRest k N (1 + T)) (tm.acceptsAt x T) v) (bodyMid k N T x tm v) bBody

The body meets the loop rule's obligation. Its contract is the tally step: the count advances and exactly one of the two tallies grows.

theorem Complexity.NTM.tallyLoop_full {k : ℕ} (tm : NTM k) (x : List Bool) (hne : tm.qstart ≠ tm.qhalt) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (T N : ℕ) (hT : 1 ≤ T) (hfT : f x.length ≤ T) (hN : 1 ≤ N) (bBody bTest B : ℕ) (hbBody : ∀ v < N, bodyTime k T v (tally (tm.acceptsAt x T) v) (tally (fun (u : ℕ) => !tm.acceptsAt x T u) v) ≤ bBody) (hbTest : ∀ w ≤ N, TM.binaryEqTime w.bits N.bits + 1 + (3 * (max (3 * (B + 3) + 1) (TM.resetBinaryWorkTime B 1) + 1) + 1) ≤ bTest) (hBw : ∀ w ≤ N, 1 + 1 + TM.binaryEqTime w.bits N.bits ≤ B) : (tm.bodyTM.loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).HoareTime (tallyPre (cIdx k) (aIdx k) (rIdx k) (bodyInput x) (bodyRest k N (1 + T)) (tm.acceptsAt x T) 0) (tallyPost (cIdx k) (aIdx k) (rIdx k) (bodyInput x) (bodyRest k N (1 + T)) (tm.acceptsAt x T) N N) (N * (bBody + bTest + 5))

The counting loop. Body and test together run the tally to its horizon: the counter walks from 0 to N, and the two tallies end holding how many of the paths accepted and how many did not.

theorem Complexity.NTM.binaryEqTime_le_of_le (w N : ℕ) (h : w ≤ N) : TM.binaryEqTime w.bits N.bits = N.bits.length + 1

The comparison's running time is uniform over the loop. Every count the loop compares is at most the horizon, and a smaller number has no more binary digits, so one bound serves every iteration — which is what the loop rule demands.

theorem Complexity.NTM.tally_le (P : ℕ → Bool) (v : ℕ) : tally P v ≤ v

A tally over [0, v) counts at most v things.

def Complexity.NTM.bodyTimeBound (k T N : ℕ) : ℕ

The body's running time with every value-dependent part replaced by its bound at the horizon.

Equations

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

theorem Complexity.NTM.bodyTime_le (k T N v : ℕ) (P : ℕ → Bool) (hv : v ≤ N) : bodyTime k T v (tally P v) (tally (fun (u : ℕ) => !P u) v) ≤ bodyTimeBound k T N

The body's running time is uniform over the loop. Only three parts of it depend on the iteration — the three counter increments — and each is bounded by the width of the horizon, since neither the count nor either tally ever exceeds it.

def Complexity.NTM.testB (N : ℕ) : ℕ

The head bound the test's rewinds need: enough for the horizon's digits.

Equations

• Complexity.NTM.testB N = N.bits.length + 3

def Complexity.NTM.testTimeBound (N : ℕ) : ℕ

The test's running time at the horizon.

Equations

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

theorem Complexity.NTM.tallyLoop_full_bounded {k : ℕ} (tm : NTM k) (x : List Bool) (hne : tm.qstart ≠ tm.qhalt) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (T N : ℕ) (hT : 1 ≤ T) (hfT : f x.length ≤ T) (hN : 1 ≤ N) : (tm.bodyTM.loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).HoareTime (tallyPre (cIdx k) (aIdx k) (rIdx k) (bodyInput x) (bodyRest k N (1 + T)) (tm.acceptsAt x T) 0) (tallyPost (cIdx k) (aIdx k) (rIdx k) (bodyInput x) (bodyRest k N (1 + T)) (tm.acceptsAt x T) N N) (N * (bodyTimeBound k T N + testTimeBound N + 5))

The counting loop with concrete bounds. Both running times are now written in terms of the horizon alone, which is what a polynomial space bound will need.

theorem Complexity.NTM.bodyTM_keepsWindowOn {k : ℕ} (tm : NTM k) (x : List Bool) (hne : tm.qstart ≠ tm.qhalt) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (T v : ℕ) (hT : 1 ≤ T) (hfT : f x.length ≤ T) (N a r : ℕ) : tm.bodyTM.KeepsWindowOn (fun (c : Cfg (bodyTapes k) tm.bodyTM.Q) => c.state = tm.bodyTM.qstart ∧ c.input = bodyInput x ∧ c.work = bodyBank k N (1 + T) v a r ∧ ∃ (s : Γw), s ≠ Γw.one ∧ c.output = outSlot s) x.length (1 + bodyTime k T v a r)

The body keeps a window. Its running time bounds how far any head can drift during one pass, and every tape it starts from is parked at cell one, so the whole pass stays inside a window of that width — independent of which iteration it is.

theorem Complexity.NTM.tallyLoop_keepsWindow_bounded {k : ℕ} (tm : NTM k) (x : List Bool) (hne : tm.qstart ≠ tm.qhalt) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (T N : ℕ) (hT : 1 ≤ T) (hfT : f x.length ≤ T) (hN : 1 ≤ N) (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) : tallyPre (cIdx k) (aIdx k) (rIdx k) (bodyInput x) (bodyRest k N (1 + T)) (tm.acceptsAt x T) 0 inp work out → ∀ (c : Cfg (bodyTapes k) (tm.bodyTM.loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).Q), (tm.bodyTM.loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).reaches { state := (tm.bodyTM.loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).qstart, input := inp, work := work, output := out } c → c.WithinDecisionSpace x.length (1 + (bodyTimeBound k T N + testTimeBound N + 5))

The counting loop's space bound at the concrete layout. Every configuration the loop ever reaches fits inside a window one iteration wide — and one iteration's width is a polynomial in the horizon, not in the exponentially many iterations.

theorem Complexity.NTM.lt_iff_succ_sub_eq_zero (r a : ℕ) : r < a ↔ r + 1 - a = 0

The comparison the epilogue actually performs. Testing r < a directly would need a strict comparator; testing (r + 1) - a = 0 needs only truncated subtraction and an equality test against zero, both of which the subroutine library already has — and it avoids having to complement the verdict afterwards.

def Complexity.NTM.epiloguePreTM (k : ℕ) : TM (bodyTapes k)

The counting machine's epilogue. Bump the rejecting tally, subtract the accepting one from it, clear the counter to reuse as scratch, test the difference against zero, and publish the answer. The counter's value is spent by this point, which is what frees a register for the test's result.

Equations

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

def Complexity.NTM.epiloguePostTM (k : ℕ) : TM (bodyTapes k)

The epilogue's tail: put the equality test's answer at cell one and publish it.

Equations

• Complexity.NTM.epiloguePostTM k = (Complexity.TM.bigSeqTM (List.map Complexity.TM.rewindWorkTM [Complexity.NTM.cIdx k])).seqTM (Complexity.TM.writeOutputBitTM (Complexity.NTM.cIdx k))

def Complexity.NTM.epilogueTM (k : ℕ) : TM (bodyTapes k)

The counting machine's epilogue. Bump the rejecting tally, subtract the accepting one from it, clear the counter to reuse as scratch, test the difference against zero, and publish the answer.

Equations

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

def Complexity.NTM.epilogueBank (k N H a r : ℕ) : Fin (bodyTapes k) → Tape

The bank the epilogue's arithmetic leaves behind.

Equations

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

theorem Complexity.NTM.epiloguePreTM_hoareTime (k N H a r : ℕ) (I O : Tape) (hI : TM.Parked I) (hO : TM.Parked O) : (epiloguePreTM k).HoareTime (fun (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) => inp = I ∧ work = bodyBank k N H N a r ∧ out = O) (fun (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) => inp = I ∧ work = epilogueBank k N H a r ∧ out = O) (3 * (max (max (TM.binarySuccTime r) (TM.binaryRippleSubTime (r + 1) a)) (TM.resetBinaryWorkTime 1 N.bits.length) + 1) + 1)

The epilogue's arithmetic, contracted. Three pinned stages: bump the rejecting tally, subtract the accepting one from it, and clear the counter — whose value is spent — to free a register for the comparison that follows.

def Complexity.NTM.afterEq (k : ℕ) (b : Bool) (I : Tape) (B : ℕ) : TM.TapePred (bodyTapes k)

The state between the epilogue's comparison and its publication: the answer sits on the counter tape, which the comparison used as its result register.

Equations

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

theorem Complexity.NTM.epiloguePostTM_hoareTime (k : ℕ) (b : Bool) (I : Tape) (B : ℕ) (hI : TM.Parked I) : (epiloguePostTM k).HoareTime (afterEq k b I B) (fun (_inp : Tape) (_work : Fin (bodyTapes k) → Tape) (out : Tape) => out = outSlot (TM.readBackWrite (Γ.ofBool b))) (1 * (B + 3) + 1 + 1 + 1)

The epilogue's publication. Rewind the register holding the comparison's answer and copy its bit into the output slot, where the surrounding obligation reads it.

theorem Complexity.NTM.epilogueBank_cIdx (k N H a r : ℕ) : epilogueBank k N H a r (cIdx k) = TM.blankTape

theorem Complexity.NTM.epilogueBank_resIdx (k N H a r : ℕ) (hsc : resIdx k ≠ cIdx k) : epilogueBank k N H a r (resIdx k) = natTape (r + 1 - a)

theorem Complexity.NTM.epilogueBank_zIdx (k N H a r : ℕ) : epilogueBank k N H a r (zIdx k) = TM.blankTape

theorem Complexity.NTM.epilogueBank_parked (k N H a r : ℕ) (j : Fin (bodyTapes k)) : TM.Parked (epilogueBank k N H a r j)

theorem Complexity.NTM.epilogueBank_cells_zero (k N H a r : ℕ) (j : Fin (bodyTapes k)) : (epilogueBank k N H a r j).cells 0 = Γ.start

theorem Complexity.NTM.epilogueEq_hoareTime (k N H a r : ℕ) (I : Tape) (hI : TM.Parked I) (hIsi : I.StartInvariant) : (TM.binaryEqTM (resIdx k) (zIdx k) (cIdx k)).HoareTime (fun (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) => inp = I ∧ work = epilogueBank k N H a r ∧ out = outSlot Γw.one) (afterEq k (decide (r < a)) I 2) (TM.binaryEqTime (r + 1 - a).bits (Nat.bits 0))

The epilogue's comparison. Testing the difference against zero decides r < a; the answer lands on the counter tape, which the arithmetic stage cleared for exactly this purpose.

theorem Complexity.NTM.afterEq_trans (k : ℕ) (b : Bool) (I : Tape) (B : ℕ) (hI : TM.Parked I) (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) (h : afterEq k b I B inp work out) : afterEq k b I B (TM.transitionInput inp) (fun (i : Fin (bodyTapes k)) => TM.transitionTape (work i)) (TM.transitionTape out)

The state between the epilogue's comparison and its publication survives a phase boundary: every tape it names is parked, so the boundary is the identity.

def Complexity.NTM.epilogueTime (N a r : ℕ) : ℕ

The epilogue's running time: its three stages and the two transitions between them.

Equations

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

theorem Complexity.NTM.epilogueTM_hoareTime (k N H a r : ℕ) (I : Tape) (hI : TM.Parked I) (hIsi : I.StartInvariant) : (epilogueTM k).HoareTime (fun (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) => inp = I ∧ work = bodyBank k N H N a r ∧ out = outSlot Γw.one) (fun (_inp : Tape) (_work : Fin (bodyTapes k) → Tape) (out : Tape) => out = outSlot (TM.readBackWrite (Γ.ofBool (decide (r < a))))) (epilogueTime N a r)

The epilogue's contract. From the bank the loop leaves — the counter at the horizon, the two tallies holding their counts — the machine writes 1 into the verdict slot exactly when the rejecting tally is smaller than the accepting one.

theorem Complexity.NTM.epilogueTM_keepsWindowOn (k N H a r : ℕ) (x : List Bool) : (epilogueTM k).KeepsWindowOn (fun (c : Cfg (bodyTapes k) (epilogueTM k).Q) => c.state = (epilogueTM k).qstart ∧ c.input = bodyInput x ∧ c.work = bodyBank k N H N a r ∧ c.output = outSlot Γw.one) x.length (1 + epilogueTime N a r)

The epilogue keeps a window. It runs for a bounded time from tapes parked at cell one, so no head can leave a window of that width.

theorem Complexity.NTM.outAcc_nil_iff (out : Tape) : TM.OutAcc [] out ↔ out = TM.blankTape

The register-arithmetic subroutines state their contracts in the TM.EmitPred shape, whose output component is an accumulator of emitted bits. With nothing emitted that is just the blank tape, so those contracts are pinned after all.

theorem Complexity.NTM.hoareTime_emit_of_pinned {m : ℕ} {tm : TM m} {inp₀ : Tape} {W W' : Fin m → Tape} {b : ℕ} (h : tm.HoareTime (fun (inp : Tape) (work : Fin m → Tape) (out : Tape) => inp = inp₀ ∧ work = W ∧ out = TM.blankTape) (fun (inp : Tape) (work : Fin m → Tape) (out : Tape) => inp = inp₀ ∧ work = W' ∧ out = TM.blankTape) b) : tm.HoareTime (TM.EmitPred inp₀ W []) (TM.EmitPred inp₀ W' []) b

A pinned contract with a blank output is an TM.EmitPred contract with nothing emitted.

theorem Complexity.NTM.bodyInput_eq (x : List Bool) : bodyInput x = { head := 1, cells := (Tape.init (List.map Γ.ofBool x)).cells }

The machine's own input tape, in the shape the register subroutines name it.

def Complexity.NTM.prologueTM (k : ℕ) (p : Polynomial ℕ) : TM (bodyTapes k)

The counting machine's prologue. Measure the input, evaluate the horizon polynomial on a unary register, turn that register into the binary horizon with one increment, bump the wipe height, and clear the scratch.

Equations

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

def Complexity.NTM.prologueBank (k T lx : ℕ) : Fin (bodyTapes k) → Tape

The bank the prologue's five stages leave behind.

Equations

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

theorem Complexity.NTM.prologueBank_eq (k T lx : ℕ) : Function.update (prologueBank k T lx) (resIdx k) (TM.regTape 0) = bodyBank k (2 ^ T) (1 + T) 0 0 0

The prologue lands on the loop's starting bank. The horizon sits on nIdx, the wipe height on regIdx, and everything else — the counter, both tallies, the scratch registers — is blank, which is what NTM.bodyBank at index zero says.

def Complexity.NTM.prologueCap (p : Polynomial ℕ) (lx : ℕ) : ℕ

A bound covering the input length and every Horner accumulator the prologue forms.

Equations

• Complexity.NTM.prologueCap p lx = ((Complexity.TM.polyCoeffs p).sum + 1) * (lx + 1) ^ (Complexity.TM.polyCoeffs p).length

theorem Complexity.NTM.le_prologueCap (p : Polynomial ℕ) (lx : ℕ) : lx ≤ prologueCap p lx

def Complexity.NTM.prologueTime (p : Polynomial ℕ) (lx : ℕ) : ℕ

The prologue's running time.

Equations

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

theorem Complexity.NTM.prologueTM_hoareTime (k : ℕ) (p : Polynomial ℕ) (x : List Bool) : (prologueTM k p).HoareTime (fun (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) => inp = { head := 1, cells := (Tape.init (List.map Γ.ofBool x)).cells } ∧ (work = fun (x : Fin (bodyTapes k)) => TM.blankTape) ∧ out = TM.blankTape) (fun (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) => inp = { head := 1, cells := (Tape.init (List.map Γ.ofBool x)).cells } ∧ work = bodyBank k (2 ^ Polynomial.eval x.length p) (1 + Polynomial.eval x.length p) 0 0 0 ∧ out = TM.blankTape) (prologueTime p x.length)

The prologue's contract. From the blank bank it lands on the loop's starting bank: the horizon on nIdx, the wipe height on regIdx, everything else blank.

theorem Complexity.NTM.prologueTM_keepsWindowOn (k : ℕ) (p : Polynomial ℕ) (x : List Bool) : (prologueTM k p).KeepsWindowOn (fun (c : Cfg (bodyTapes k) (prologueTM k p).Q) => c.state = (prologueTM k p).qstart ∧ c.input = { head := 1, cells := (Tape.init (List.map Γ.ofBool x)).cells } ∧ (c.work = fun (x : Fin (bodyTapes k)) => TM.blankTape) ∧ c.output = TM.blankTape) x.length (1 + prologueTime p x.length)

The prologue keeps a window. It runs for a bounded time from blank tapes parked at cell one, so nothing travels beyond a window of that width.

def Complexity.NTM.ppMachine (k : ℕ) (tm : NTM k) (p : Polynomial ℕ) : TM (bodyTapes k)

The whole counting machine. Park the heads off the left marker, set up the horizon and the wipe height, run the tally to its horizon, then compare the two tallies and publish.

Equations

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

theorem Complexity.NTM.ppPark_hoareTime (k : ℕ) (x : List Bool) : TM.skipTM.HoareTime (fun (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool x) ∧ (work = fun (x : Fin (bodyTapes k)) => Tape.init []) ∧ out = Tape.init []) (fun (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) => inp = { head := 1, cells := (Tape.init (List.map Γ.ofBool x)).cells } ∧ (work = fun (x : Fin (bodyTapes k)) => TM.blankTape) ∧ out = TM.blankTape) 1

The parking step. One transition off the initial configuration puts every head at cell one, which is where every stage of the machine expects to be entered.

def Complexity.NTM.ppTime (k : ℕ) (tm : NTM k) (p : Polynomial ℕ) (x : List Bool) : ℕ

The whole machine's running time.

Equations

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

theorem Complexity.NTM.ppMachine_hoareTime (k : ℕ) (tm : NTM k) (x : List Bool) (hne : tm.qstart ≠ tm.qhalt) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (p : Polynomial ℕ) (hT : 1 ≤ Polynomial.eval x.length p) (hfT : f x.length ≤ Polynomial.eval x.length p) : (ppMachine k tm p).HoareTime (fun (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool x) ∧ (work = fun (x : Fin (bodyTapes k)) => Tape.init []) ∧ out = Tape.init []) (fun (_inp : Tape) (_work : Fin (bodyTapes k) → Tape) (out : Tape) => out = outSlot (TM.readBackWrite (Γ.ofBool (decide (tally (fun (u : ℕ) => !tm.acceptsAt x (Polynomial.eval x.length p) u) (2 ^ Polynomial.eval x.length p) < tally (tm.acceptsAt x (Polynomial.eval x.length p)) (2 ^ Polynomial.eval x.length p)))))) (ppTime k tm p x)

The counting machine's contract. From its initial configuration it halts with the verdict slot holding 1 exactly when the accepting paths outnumber the rejecting ones.

theorem Complexity.NTM.tallyLoop_keepsWindowOn {k : ℕ} (tm : NTM k) (x : List Bool) (hne : tm.qstart ≠ tm.qhalt) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (T N : ℕ) (hT : 1 ≤ T) (hfT : f x.length ≤ T) (hN : 1 ≤ N) : (tm.bodyTM.loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).KeepsWindowOn (fun (c : Cfg (bodyTapes k) (tm.bodyTM.loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).Q) => c.state = (tm.bodyTM.loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).qstart ∧ tallyPre (cIdx k) (aIdx k) (rIdx k) (bodyInput x) (bodyRest k N (1 + T)) (tm.acceptsAt x T) 0 c.input c.work c.output) x.length (1 + (bodyTimeBound k T N + testTimeBound N + 5))

The counting loop's space bound, packaged as a conditional window contract so it can be composed with the machine's other parts.

theorem Complexity.NTM.tallyPre_cfg_ok (k N H v a r : ℕ) (x : List Bool) (S : ℕ) (hS : 1 ≤ S) {Q : Type} (c : Cfg (bodyTapes k) Q) (h : c.input = bodyInput x ∧ c.work = bodyBank k N H v a r ∧ ∃ (s : Γw), s ≠ Γw.one ∧ c.output = outSlot s) : c.WithinDecisionSpace x.length S ∧ TM.CfgStartInvariant c

The loop's starting configuration is inside any window at least one cell wide, and carries its left markers.

theorem Complexity.NTM.loopEpilogue_keepsWindowOn {k : ℕ} (tm : NTM k) (x : List Bool) (hne : tm.qstart ≠ tm.qhalt) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (T N : ℕ) (hT : 1 ≤ T) (hfT : f x.length ≤ T) (hN : 1 ≤ N) (S : ℕ) (hS1 : 1 + (bodyTimeBound k T N + testTimeBound N + 5) ≤ S) (hS2 : 1 + epilogueTime N (tally (tm.acceptsAt x T) N) (tally (fun (u : ℕ) => !tm.acceptsAt x T u) N) ≤ S) : ((tm.bodyTM.loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).seqTM (epilogueTM k)).KeepsWindowOn (fun (c : Cfg (bodyTapes k) ((tm.bodyTM.loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).seqTM (epilogueTM k)).Q) => ∃ (d : Cfg (bodyTapes k) (tm.bodyTM.loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).Q), (d.state = (tm.bodyTM.loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).qstart ∧ tallyPre (cIdx k) (aIdx k) (rIdx k) (bodyInput x) (bodyRest k N (1 + T)) (tm.acceptsAt x T) 0 d.input d.work d.output) ∧ c = (tm.bodyTM.loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).phase1Wrap (epilogueTM k) d) x.length S

The loop and the epilogue, composed in space.

theorem Complexity.NTM.prologueRest_keepsWindowOn {k : ℕ} (tm : NTM k) (x : List Bool) (hne : tm.qstart ≠ tm.qhalt) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (p : Polynomial ℕ) (T N : ℕ) (hTdef : T = Polynomial.eval x.length p) (hNdef : N = 2 ^ T) (hT : 1 ≤ T) (hfT : f x.length ≤ T) (hN : 1 ≤ N) (S : ℕ) (hS0 : 1 + prologueTime p x.length ≤ S) (hS1 : 1 + (bodyTimeBound k T N + testTimeBound N + 5) ≤ S) (hS2 : 1 + epilogueTime N (tally (tm.acceptsAt x T) N) (tally (fun (u : ℕ) => !tm.acceptsAt x T u) N) ≤ S) : ((prologueTM k p).seqTM ((tm.bodyTM.loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).seqTM (epilogueTM k))).KeepsWindowOn (fun (c : Cfg (bodyTapes k) ((prologueTM k p).seqTM ((tm.bodyTM.loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).seqTM (epilogueTM k))).Q) => ∃ (d : Cfg (bodyTapes k) (prologueTM k p).Q), (d.state = (prologueTM k p).qstart ∧ d.input = bodyInput x ∧ (d.work = fun (x : Fin (bodyTapes k)) => TM.blankTape) ∧ d.output = TM.blankTape) ∧ c = (prologueTM k p).phase1Wrap ((tm.bodyTM.loopTM (TM.tallyTestTM (cIdx k) (nIdx k) (resIdx k))).seqTM (epilogueTM k)) d) x.length S

The prologue joined to the rest, in space.

theorem Complexity.NTM.ppMachine_keepsWindow {k : ℕ} (tm : NTM k) (x : List Bool) (hne : tm.qstart ≠ tm.qhalt) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (p : Polynomial ℕ) (T N : ℕ) (hTdef : T = Polynomial.eval x.length p) (hNdef : N = 2 ^ T) (hT : 1 ≤ T) (hfT : f x.length ≤ T) (hN : 1 ≤ N) (S : ℕ) (hS : 1 ≤ S) (hS0 : 1 + prologueTime p x.length ≤ S) (hS1 : 1 + (bodyTimeBound k T N + testTimeBound N + 5) ≤ S) (hS2 : 1 + epilogueTime N (tally (tm.acceptsAt x T) N) (tally (fun (u : ℕ) => !tm.acceptsAt x T u) N) ≤ S) (c' : Cfg (bodyTapes k) (ppMachine k tm p).Q) : (ppMachine k tm p).reaches ((ppMachine k tm p).initCfg x) c' → c'.WithinDecisionSpace x.length S

The whole machine keeps a polynomial window. Every configuration it reaches from its initial one fits inside S cells.

theorem Complexity.NTM.size_horizon (T : ℕ) : (2 ^ T).size = T + 1

The horizon's width is the exponent plus one. Every bound the machine's parts state in terms of the horizon's number of digits is therefore a bound in terms of the exponent — which is what makes them polynomial in the input length rather than exponential.

theorem Complexity.NTM.bits_length_horizon (T : ℕ) : (2 ^ T).bits.length = T + 1

noncomputable def Complexity.NTM.capPoly (p : Polynomial ℕ) : Polynomial ℕ

The Horner cap, as a polynomial. The space bound the surrounding obligation asks for must be a Polynomial ℕ, so each arithmetic expression the machine's parts are bounded by has to be mirrored by a polynomial whose evaluation reproduces it.

Equations

• Complexity.NTM.capPoly p = Polynomial.C ((Complexity.TM.polyCoeffs p).sum + 1) * (Polynomial.X + 1) ^ (Complexity.TM.polyCoeffs p).length

@[simp]

theorem Complexity.NTM.capPoly_eval (p : Polynomial ℕ) (n : ℕ) : Polynomial.eval n (capPoly p) = prologueCap p n

noncomputable def Complexity.NTM.opBudgetPoly (p : Polynomial ℕ) : Polynomial ℕ

The operation budget, as a polynomial.

Equations

• Complexity.NTM.opBudgetPoly p = Polynomial.C 32 * (Complexity.NTM.capPoly p + Polynomial.C 2) ^ 3

@[simp]

theorem Complexity.NTM.opBudgetPoly_eval (p : Polynomial ℕ) (n : ℕ) : Polynomial.eval n (opBudgetPoly p) = TM.opBudget (prologueCap p n)

noncomputable def Complexity.NTM.layerBudgetPoly (p : Polynomial ℕ) : Polynomial ℕ

The layer budget, as a polynomial.

Equations

• Complexity.NTM.layerBudgetPoly p = Polynomial.C 4 * Complexity.NTM.opBudgetPoly p + Polynomial.C 3

@[simp]

theorem Complexity.NTM.layerBudgetPoly_eval (p : Polynomial ℕ) (n : ℕ) : Polynomial.eval n (layerBudgetPoly p) = TM.layerBudget (prologueCap p n)

theorem Complexity.NTM.size_horizon_pred (T : ℕ) : (2 ^ T - 1).size = T

The predecessor of the horizon has exactly T digits, all of them ones.

theorem Complexity.NTM.binarySuccTime_horizon_pred (T : ℕ) : TM.binarySuccTime (2 ^ T - 1) ≤ 2 * T + 2

noncomputable def Complexity.NTM.prologueTimePoly (p : Polynomial ℕ) : Polynomial ℕ

The prologue's running time, as a polynomial. Only a bound is possible — the running time involves max, which no polynomial reproduces — so the maxima are replaced by sums.

Equations

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

theorem Complexity.NTM.prologueTime_le (p : Polynomial ℕ) (n : ℕ) : prologueTime p n ≤ Polynomial.eval n (prologueTimePoly p)

theorem Complexity.NTM.tally_size_le (P : ℕ → Bool) (N : ℕ) : (tally P N).size ≤ N.size

A tally has no more digits than its horizon. Every time bound the epilogue states in terms of the tallies' widths is therefore a bound in terms of the exponent.

theorem Complexity.NTM.tally_size_horizon_le (P : ℕ → Bool) (T : ℕ) : (tally P (2 ^ T)).size ≤ T + 1

theorem Complexity.NTM.tally_succ_size_horizon_le (P : ℕ → Bool) (T : ℕ) : (tally P (2 ^ T) + 1).size ≤ T + 2

One more than a tally still has no more than one extra digit.

theorem Complexity.NTM.loopWidth_le (k T : ℕ) : 1 + (bodyTimeBound k T (2 ^ T) + testTimeBound (2 ^ T) + 5) ≤ 2 * ((wipeTargets k).length * (T + 5)) + (40 * T + 300)

The loop's window is linear in the exponent. Its width is stated through the digit counts of the horizon and of the two tallies; each of those is T + O(1), so the width is too — even though the horizon itself is 2 ^ T.

theorem Complexity.NTM.epilogueWidth_le (T : ℕ) (P : ℕ → Bool) : 1 + epilogueTime (2 ^ T) (tally P (2 ^ T)) (tally (fun (u : ℕ) => !P u) (2 ^ T)) ≤ 40 * T + 200

The epilogue's window is linear in the exponent too. Its cost is stated through the digit counts of the two tallies and of their difference, all of which are T + O(1).

noncomputable def Complexity.NTM.ppSpacePoly (k : ℕ) (p : Polynomial ℕ) : Polynomial ℕ

The machine's space bound, as a polynomial. The sum of the three parts' widths: the prologue's, the loop's, and the epilogue's.

Equations

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

theorem Complexity.NTM.ppSpacePoly_eval (k : ℕ) (p : Polynomial ℕ) (n : ℕ) : Polynomial.eval n (ppSpacePoly k p) = Polynomial.eval n (prologueTimePoly p) + (2 * (wipeTargets k).length * (Polynomial.eval n p + 5) + 40 * Polynomial.eval n p + 300) + (40 * Polynomial.eval n p + 200)

theorem Complexity.NTM.prologue_le_ppSpacePoly (k : ℕ) (p : Polynomial ℕ) (n : ℕ) : 1 + prologueTime p n ≤ Polynomial.eval n (ppSpacePoly k p)

theorem Complexity.NTM.loop_le_ppSpacePoly (k : ℕ) (p : Polynomial ℕ) (n : ℕ) : 1 + (bodyTimeBound k (Polynomial.eval n p) (2 ^ Polynomial.eval n p) + testTimeBound (2 ^ Polynomial.eval n p) + 5) ≤ Polynomial.eval n (ppSpacePoly k p)

theorem Complexity.NTM.epilogue_le_ppSpacePoly (k : ℕ) (p : Polynomial ℕ) (n : ℕ) (P : ℕ → Bool) : 1 + epilogueTime (2 ^ Polynomial.eval n p) (tally P (2 ^ Polynomial.eval n p)) (tally (fun (u : ℕ) => !P u) (2 ^ Polynomial.eval n p)) ≤ Polynomial.eval n (ppSpacePoly k p)

def Complexity.NTM.ppCond {k : ℕ} (tm : NTM k) (p : Polynomial ℕ) (x : List Bool) : Prop

The comparison the surrounding obligation names: after 2 ^ p |x| tally steps, does the accepting component exceed the rejecting one?

Equations

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

theorem Complexity.NTM.ppMachine_decides (k : ℕ) (tm : NTM k) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (p : Polynomial ℕ) (hle : ∀ (n : ℕ), f n ≤ Polynomial.eval n p) (hne : tm.qstart ≠ tm.qhalt) (x : List Bool) : ∃ (c' : Cfg (bodyTapes k) (ppMachine k tm (p + 1)).Q), (ppMachine k tm (p + 1)).reaches ((ppMachine k tm (p + 1)).initCfg x) c' ∧ (ppMachine k tm (p + 1)).halted c' ∧ (tm.ppCond p x → c'.output.cells 1 = Γ.one) ∧ (¬tm.ppCond p x → c'.output.cells 1 = Γ.zero)

The counting machine decides the PP comparison. It runs at the horizon p.eval |x| + 1 — one more than the specification names, so that the horizon is never zero, which the simulation needs — and NTM.cmp_horizon_iff' says the comparison is the same either way.

theorem Complexity.NTM.ppMachine_space (k : ℕ) (tm : NTM k) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (p : Polynomial ℕ) (hle : ∀ (n : ℕ), f n ≤ Polynomial.eval n p) (hne : tm.qstart ≠ tm.qhalt) (x : List Bool) (c' : Cfg (bodyTapes k) (ppMachine k tm (p + 1)).Q) (hreach : (ppMachine k tm (p + 1)).reaches ((ppMachine k tm (p + 1)).initCfg x) c') : c'.WithinDecisionSpace x.length (Polynomial.eval x.length (ppSpacePoly k (p + 1)))

The counting machine runs in polynomial space. Every configuration it reaches fits inside NTM.ppSpacePoly cells — a polynomial in the input length, even though the machine's own running time is exponential.

theorem Complexity.NTM.natTape_two_read : (natTape 2).read = Γ.zero

Two is the smallest numeral whose low digit is zero. A blank register incremented twice therefore reads 0, which is how the trivial machine below produces a 0 to publish — the alphabet offers no other way to name one.

def Complexity.NTM.zeroTM (k : ℕ) : TM (bodyTapes k)

The trivial machine: it writes 0 and halts. This is what serves for a source machine that starts halted, where no path can accept and the comparison is always false.

Equations

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

def Complexity.NTM.zeroTime : ℕ

The trivial machine's running time.

Equations

• Complexity.NTM.zeroTime = 1 + 1 + (3 * (max (max (Complexity.TM.binarySuccTime 0) (Complexity.TM.binarySuccTime 1)) 1 + 1) + 1)

theorem Complexity.NTM.zeroTM_hoareTime (k : ℕ) (x : List Bool) : (zeroTM k).HoareTime (fun (inp : Tape) (work : Fin (bodyTapes k) → Tape) (out : Tape) => inp = Tape.init (List.map Γ.ofBool x) ∧ (work = fun (x : Fin (bodyTapes k)) => Tape.init []) ∧ out = Tape.init []) (fun (_inp : Tape) (_work : Fin (bodyTapes k) → Tape) (out : Tape) => out = outSlot Γw.zero) zeroTime

The trivial machine's contract. It halts with 0 in the verdict slot.

noncomputable def Complexity.NTM.zeroSpacePoly : Polynomial ℕ

The trivial machine's space bound, as a polynomial: a constant.

Equations

• Complexity.NTM.zeroSpacePoly = Polynomial.C Complexity.NTM.zeroTime

@[simp]

theorem Complexity.NTM.zeroSpacePoly_eval (n : ℕ) : Polynomial.eval n zeroSpacePoly = zeroTime

theorem Complexity.NTM.zeroTM_space (k : ℕ) (x : List Bool) (c' : Cfg (bodyTapes k) (zeroTM k).Q) (hreach : (zeroTM k).reaches ((zeroTM k).initCfg x) c') : c'.WithinDecisionSpace x.length (Polynomial.eval x.length zeroSpacePoly)

The trivial machine keeps a constant window. Its running time is constant, so the heads cannot travel far enough to leave one.

theorem Complexity.NTM.zeroTM_decides (k : ℕ) (x : List Bool) : ∃ (c' : Cfg (bodyTapes k) (zeroTM k).Q), (zeroTM k).reaches ((zeroTM k).initCfg x) c' ∧ (zeroTM k).halted c' ∧ c'.output.cells 1 = Γ.zero

The trivial machine publishes 0.

theorem Complexity.NTM.not_ppCond_of_qstart_eq_qhalt (k : ℕ) (tm : NTM k) (heq : tm.qstart = tm.qhalt) (p : Polynomial ℕ) (x : List Bool) : ¬tm.ppCond p x

A source that starts halted fails the comparison. No path accepts, so the accepting tally is zero and cannot exceed the rejecting one — which is why the trivial machine, publishing 0 unconditionally, decides this case.