Parts of the path-counting machine

⚠️ Unreviewed by Bolton

The machine that will witness PP ⊆ PSPACE enumerates choice sequences, runs one path of the probabilistic machine along each, and keeps a running count. Its inner call is NTM.choiceTM, which is time-bounded rather than space-bounded: every path halts within the protocol's own time bound, so the window follows from TM.keepsWindowOn_of_haltsIn with no space hypothesis at all. That is simpler than the corresponding step for PH ⊆ PSPACE, whose inner call is only space-bounded.

An architectural constraint on the body

The body must clear the simulated machine's work tapes between iterations, and the only content-agnostic reset available is TM.resetTapesTM, whose wipe phase (TM.wipeLoop_hoareTime) requires the real output tape blank. The rewind phase (TM.rewindList_hoareTime) does not — it asks only that the output be TM.Parked.

That rules out the obvious design. TM.ifTM branches on the real output tape's verdict cell, so using the simulation as a conditional's test would leave the verdict sitting on the output and block the next iteration's wipe; and there is no subroutine that clears the output tape. The verdict therefore has to be written to a work tape — the simulation output-retargeted, as in NTM.choiceTM_placed_keepsWindow — and republished on the output only for the moment the branch needs it. TM.writeOutputBitTM is the one-transition subroutine that does the republishing; the library had no way to move a bit from a work tape to the output, which is why the constraint above looked fatal.

Main results

• NTM.acceptCount_add, NTM.mem_iff_polyHorizon — the comparison is stable under enlarging the horizon, so the machine may use a polynomial bound in place of the protocol's own (uncomputable) time function
• hasBinaryString_unique, hasBinaryNat_value_unique — a binary tape determines its contents
• tallyState, tallyIdx, tallyIdx_tallyState — the counting machine's tape state, and the index read back off it
• natTape, tallyWork, tallyState_iff — that state, fully pinned
• binarySucc_tallyState, binarySucc_tallyState_counter, binarySucc_tallyState_rej — the three increment stages, from the library's canonical successor
• NTM.choiceStream_of_hasBinaryString, NTM.choiceStream_eq_choicesOfNat — a binary counter tape is the choice sequence of its value
• NTM.choiceTM_choiceCells — the path simulation leaves the counter's digits alone
• NTM.choiceTM_dropChoice_eq, NTM.choiceTM_verdict — what the simulation computes from a counter value, and that its verdict is the enumeration's acceptance test
• NTM.choiceTM_haltsIn — a path simulation halts within the protocol's time bound
• NTM.choiceTM_keepsWindowOn — and therefore keeps a window
• NTM.choiceTM_placed_keepsWindow, NTM.choiceTM_lifted_keepsWindow — and so does the call once placed in the larger machine, with or without output retargeting
• natTape_parked — the numeric tapes satisfy the side condition the reset subroutines demand
• NTM.acceptCount_eq_card_range — the accepting-path count is a count over counter values
• NTM.tally, NTM.tally_eq_card — the running accumulation computes that count
• NTM.mem_iff_two_mul_tally — what the counting machine decides
• NTM.tally_add_compl, NTM.lt_two_mul_tally_iff, NTM.mem_iff_tally_lt_tally — and the same as a comparison of two counters, so the machine never forms 2 ^ T
• NTM.acceptsAt, NTM.mem_iff_tally_lt_tally_poly — the complete machine specification
• NTM.tallyStep, NTM.tallyStep_iterate — the loop invariant on (counter, accepting tally, rejecting tally)
• NTM.mem_iff_iterate_tallyStep — membership as one iterated function and a comparison
• NTM.outSlot, NTM.tallyPre, NTM.tallyPost, NTM.tallyLoop_hoareTime_of_hoare — the counting loop from a Hoare contract for the body and one for the test, chained through fully pinned tape states, which is the interface a machine construction meets
• NTM.tallyLoop_keepsWindow_of_hoare — the same loop's space bound, one iteration wide
• NTM.delayNTM_char, NTM.acceptCount_eq_zero_of_qstart_eq_qhalt, NTM.not_mem_of_qstart_eq_qhalt — the PP characterisation transported to the delayed machine, and the degenerate case that licenses it
• NTM.choiceTM_delay_dropChoice_eq, NTM.choiceTM_delay_haltsIn — what the loop body's simulation computes, entered where a composed machine can enter it
• NTM.tally_eq_acceptCount, NTM.tally_cmp_iff — the tally is the accepting count
• NTM.cmp_horizon_iff, NTM.cmp_horizon_iff' — the PP comparison does not depend on the horizon, past the point where every path has halted
• NTM.tallyLoop_hoareTime, NTM.tallyLoop_hoareTime_of_body — the counting loop, granted only that the body advances the triple

A binary tape determines its contents

The indexed loop rule reads the iteration count back off the tapes, so the counter's encoding has to be unambiguous. It is: a tape's digits are pinned cell by cell and the first blank marks the end, so two representations on the same tape coincide.

theorem Complexity.hasBinaryString_unique {t : Tape} {b b' : List Bool} (h : t.HasBinaryString b) (h' : t.HasBinaryString b') : b = b'

A tape carries at most one binary string.

theorem Complexity.hasBinaryNat_value_unique {t : Tape} {v v' : ℕ} (h : t.HasBinaryNat v) (h' : t.HasBinaryNat v') : v = v'

A tape carries at most one natural number.

The counting machine's tape state

def Complexity.tallyState {n : ℕ} (cIdx aIdx rIdx : Fin n) (I : Tape) (rest : Fin n → Tape) (st : ℕ × ℕ × ℕ) : TapePred n

The tape state of the counting machine. Three designated work tapes carry the counter and the two tallies in canonical binary; every other tape, the input, and the output are pinned.

Equations

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

noncomputable def Complexity.tallyIdx {n : ℕ} (cIdx : Fin n) : Tape → (Fin n → Tape) → Tape → ℕ

The iteration count read back off the counter tape. The input and output tapes are ignored; they are present because TM.loopTM_hoareTime_indexed takes the index as a function of the whole tape state.

Equations

• Complexity.tallyIdx cIdx x✝¹ work x✝ = Classical.epsilon fun (v : ℕ) => (work cIdx).HasBinaryNat v

theorem Complexity.tallyIdx_tallyState {n : ℕ} (cIdx aIdx rIdx : Fin n) (I : Tape) (rest : Fin n → Tape) (st : ℕ × ℕ × ℕ) (inp : Tape) (work : Fin n → Tape) (out : Tape) (h : tallyState cIdx aIdx rIdx I rest st inp work out) : tallyIdx cIdx inp work out = st.1

Reading the index back is faithful. This is the hypothesis TM.loopTM_hoareTime_indexed needs: the loop's variant can be computed from the tapes it is looking at.

def Complexity.natTape (v : ℕ) : Tape

The canonical tape for a natural number.

Equations

• Complexity.natTape v = (Complexity.Tape.init (List.map Complexity.Γ.ofBool v.bits)).move Complexity.Dir3.right

def Complexity.tallyWork {n : ℕ} (cIdx aIdx rIdx : Fin n) (rest : Fin n → Tape) (st : ℕ × ℕ × ℕ) : Fin n → Tape

The work bank of the counting machine at a given state.

Equations

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

theorem Complexity.tallyState_iff {n : ℕ} (cIdx aIdx rIdx : Fin n) (hca : cIdx ≠ aIdx) (hcr : cIdx ≠ rIdx) (har : aIdx ≠ rIdx) (I : Tape) (rest : Fin n → Tape) (st : ℕ × ℕ × ℕ) (inp : Tape) (work : Fin n → Tape) (out : Tape) : tallyState cIdx aIdx rIdx I rest st inp work out ↔ inp = I ∧ work = tallyWork cIdx aIdx rIdx rest st ∧ out.read ≠ Γ.start

The tape state is fully pinned. Tape.HasBinaryNat determines a tape outright, so the counting machine's state names every tape exactly — which is what lets the library's framed subroutine contracts, whose preconditions pin all three tape components, be applied to it.

theorem Complexity.natTape_read_ne_start (v : ℕ) : (natTape v).read ≠ Γ.start

Canonical number tapes read a digit or a blank, never the left marker.

theorem Complexity.tallyWork_read_ne_start {n : ℕ} (cIdx aIdx rIdx : Fin n) (rest : Fin n → Tape) (hrest : ∀ (i : Fin n), (rest i).read ≠ Γ.start) (st : ℕ × ℕ × ℕ) (i : Fin n) : (tallyWork cIdx aIdx rIdx rest st i).read ≠ Γ.start

The work bank of the counting machine reads off the left marker on every tape.

theorem Complexity.natTape_parked (v : ℕ) : TM.Parked (natTape v)

A canonical number tape is parked: its head is off the left marker and no cell beyond the marker holds one. This is the side condition the rewind and wipe subroutines ask of every tape they carry along.

theorem Complexity.binarySucc_tallyState {n : ℕ} (cIdx aIdx rIdx : Fin n) (hca : cIdx ≠ aIdx) (hcr : cIdx ≠ rIdx) (har : aIdx ≠ rIdx) (I : Tape) (rest : Fin n → Tape) (v a r : ℕ) (hI : I.read ≠ Γ.start) (hrest : ∀ (i : Fin n), (rest i).read ≠ Γ.start) : (TM.binarySuccTM aIdx).HoareTime (tallyState cIdx aIdx rIdx I rest (v, a, r)) (tallyState cIdx aIdx rIdx I rest (v, a + 1, r)) (TM.binarySuccTime a)

The three increment stages. Advancing one of the numeric tapes by one is the library's canonical successor applied to the pinned state; the output tape is carried along untouched, whatever it holds.

theorem Complexity.binarySucc_tallyState_counter {n : ℕ} (cIdx aIdx rIdx : Fin n) (hca : cIdx ≠ aIdx) (hcr : cIdx ≠ rIdx) (har : aIdx ≠ rIdx) (I : Tape) (rest : Fin n → Tape) (v a r : ℕ) (hI : I.read ≠ Γ.start) (hrest : ∀ (i : Fin n), (rest i).read ≠ Γ.start) : (TM.binarySuccTM cIdx).HoareTime (tallyState cIdx aIdx rIdx I rest (v, a, r)) (tallyState cIdx aIdx rIdx I rest (v + 1, a, r)) (TM.binarySuccTime v)

The counter-increment stage.

theorem Complexity.binarySucc_tallyState_rej {n : ℕ} (cIdx aIdx rIdx : Fin n) (hca : cIdx ≠ aIdx) (hcr : cIdx ≠ rIdx) (har : aIdx ≠ rIdx) (I : Tape) (rest : Fin n → Tape) (v a r : ℕ) (hI : I.read ≠ Γ.start) (hrest : ∀ (i : Fin n), (rest i).read ≠ Γ.start) : (TM.binarySuccTM rIdx).HoareTime (tallyState cIdx aIdx rIdx I rest (v, a, r)) (tallyState cIdx aIdx rIdx I rest (v, a, r + 1)) (TM.binarySuccTime r)

The rejecting-tally-increment stage.

theorem Complexity.NTM.choiceTM_haltsIn {k : ℕ} (tm : NTM k) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (x : List Bool) (c : Cfg (k + 1) tm.Q) (hdrop : dropChoice c = tm.initCfg x) (hinv : (c.work (Fin.last k)).StartInvariant) (hhead : 1 ≤ (c.work (Fin.last k)).head) : ∃ (c' : Cfg (k + 1) tm.choiceTM.Q), ∃ t ≤ f x.length + 1, tm.choiceTM.reachesIn t c c' ∧ tm.choiceTM.halted c'

A path simulation halts within the protocol's own time bound. All paths of tm halt within f |x| steps, and choiceTM follows one of them step for step, so it halts too.

theorem Complexity.NTM.choiceTM_keepsWindowOn {k : ℕ} (tm : NTM k) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (x : List Bool) {inputLength h₀ : ℕ} : tm.choiceTM.KeepsWindowOn (fun (c : Cfg (k + 1) tm.choiceTM.Q) => dropChoice c = tm.initCfg x ∧ (c.work (Fin.last k)).StartInvariant ∧ 1 ≤ (c.work (Fin.last k)).head ∧ (∀ (i : Fin (k + 1)), (c.work i).head ≤ h₀) ∧ c.input.head ≤ inputLength + h₀ + 1 ∧ c.output.head ≤ h₀ + 1) inputLength (h₀ + (f x.length + 1))

A path simulation keeps a window. Since every path halts within f |x| + 1 steps and a head moves at most one cell per step, nothing travels more than that far beyond where it started. No space hypothesis on tm is needed — its time bound does the work.

theorem Complexity.NTM.acceptCount_eq_card_range {k : ℕ} (tm : NTM k) (x : List Bool) (T : ℕ) : tm.acceptCount x T = {v ∈ Finset.range (2 ^ T) | have c' := tm.trace T (choicesOfNat T v) (tm.initCfg x); c'.state = tm.qhalt ∧ c'.output.cells 1 = Γ.one}.card

The accepting-path count is a count over counter values. NTM.acceptCount ranges over functions Fin T → Bool; the counting machine ranges over the numbers below 2 ^ T. The correspondence of choicesOfNat and natOfChoices identifies the two counts, so the machine's tally is the quantity PP compares against half.

The running tally

A counting loop does not compute a cardinality; it accumulates. tally is that accumulation, and tally_eq_card identifies it with the cardinality — which is the loop invariant the machine's correctness proof will carry.

def Complexity.NTM.tally (P : ℕ → Bool) : ℕ → ℕ

The running count of the values below N satisfying P, as a loop accumulates it.

Equations

• Complexity.NTM.tally P 0 = 0
• Complexity.NTM.tally P N.succ = Complexity.NTM.tally P N + if P N = true then 1 else 0

theorem Complexity.NTM.tally_eq_card (P : ℕ → Bool) (N : ℕ) : tally P N = {v ∈ Finset.range N | P v = true}.card

The accumulation computes the cardinality.

theorem Complexity.NTM.mem_iff_two_mul_tally {k : ℕ} {L : Language} {tm : NTM k} {f : ℕ → ℕ} (hchar : ∀ (x : List Bool), x ∈ L ↔ 2 ^ f x.length < 2 * tm.acceptCount x (f x.length)) (x : List Bool) : x ∈ L ↔ 2 ^ f x.length < 2 * tally (fun (v : ℕ) => decide (have c' := tm.trace (f x.length) (choicesOfNat (f x.length) v) (tm.initCfg x); c'.state = tm.qhalt ∧ c'.output.cells 1 = Γ.one)) (2 ^ f x.length)

What the counting machine decides. Membership is a comparison between 2 ^ T and twice a running tally over counter values — an accumulation a loop performs and a comparison of two binary naturals. Neither probability, nor rationals, nor a quantifier over functions remains.

theorem Complexity.NTM.tally_add_compl (P : ℕ → Bool) (N : ℕ) : tally P N + tally (fun (v : ℕ) => !P v) N = N

A tally and its complement partition the range.

theorem Complexity.NTM.lt_two_mul_tally_iff (P : ℕ → Bool) (N : ℕ) : N < 2 * tally P N ↔ tally (fun (v : ℕ) => !P v) N < tally P N

The threshold is a comparison of two counters. More than half of the range satisfies P exactly when the tally of P exceeds the tally of its complement. The machine therefore never has to form 2 ^ T or multiply: it keeps two counters and compares them.

theorem Complexity.NTM.mem_iff_tally_lt_tally {k : ℕ} {L : Language} {tm : NTM k} {f : ℕ → ℕ} (hchar : ∀ (x : List Bool), x ∈ L ↔ 2 ^ f x.length < 2 * tm.acceptCount x (f x.length)) (x : List Bool) : x ∈ L ↔ tally (fun (v : ℕ) => !decide (have c' := tm.trace (f x.length) (choicesOfNat (f x.length) v) (tm.initCfg x); c'.state = tm.qhalt ∧ c'.output.cells 1 = Γ.one)) (2 ^ f x.length) < tally (fun (v : ℕ) => decide (have c' := tm.trace (f x.length) (choicesOfNat (f x.length) v) (tm.initCfg x); c'.state = tm.qhalt ∧ c'.output.cells 1 = Γ.one)) (2 ^ f x.length)

What the counting machine decides, as a comparison of two counters.

The counter tape is the choice sequence

theorem Complexity.NTM.choiceStream_of_hasBinaryString {k : ℕ} {tm : NTM k} (c : Cfg (k + 1) tm.Q) (bits : List Bool) (h : (c.work (Fin.last k)).HasBinaryString bits) (j : ℕ) : choiceStream c j = bits.getD j false

What the path simulator reads off a binary counter tape. NTM.choiceStream maps every cell that is not Γ.one to false, including the blanks past the counter's last digit — and those are exactly the high bits of the number, which are zero. So a tape carrying a binary string is the choice sequence it encodes, padded with false for free.

The count is stable under enlarging the horizon

A counting machine cannot evaluate the protocol's own time bound f — it is an arbitrary function known only to be O(n^m). It must therefore count over a polynomial horizon it can compute. That is sound because every path has already halted: extending the horizon multiplies both the accepting count and the total by the same factor, so the comparison is unchanged.

theorem Complexity.NTM.acceptCount_add {k : ℕ} (tm : NTM k) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (x : List Bool) (b : ℕ) : tm.acceptCount x (f x.length + b) = tm.acceptCount x (f x.length) * 2 ^ b

Extending the horizon multiplies the accepting count by the number of extensions.

theorem Complexity.NTM.mem_iff_polyHorizon {k : ℕ} {L : Language} {tm : NTM k} {f : ℕ → ℕ} {p : Polynomial ℕ} (hall : tm.AllPathsHaltIn f) (hle : ∀ (n : ℕ), f n ≤ Polynomial.eval n p) (hchar : ∀ (x : List Bool), x ∈ L ↔ 2 ^ f x.length < 2 * tm.acceptCount x (f x.length)) (x : List Bool) : x ∈ L ↔ 2 ^ Polynomial.eval x.length p < 2 * tm.acceptCount x (Polynomial.eval x.length p)

The comparison is unchanged by a larger, computable horizon. Counting over p |x| choice sequences instead of f |x| scales both sides by the same power of two. This is what lets the machine use a polynomial it can evaluate in place of the protocol's own time function.

theorem Complexity.NTM.cmp_horizon_iff {k : ℕ} (tm : NTM k) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (x : List Bool) (T : ℕ) (hT : f x.length ≤ T) : 2 ^ T < 2 * tm.acceptCount x T ↔ 2 ^ f x.length < 2 * tm.acceptCount x (f x.length)

The PP comparison does not depend on the horizon, as long as the horizon is past the point where every path has halted. Extending it multiplies both the accepting count and the total by the same power of two. This is what lets the counting machine run to a horizon of its own choosing rather than the one its specification names.

theorem Complexity.NTM.cmp_horizon_iff' {k : ℕ} (tm : NTM k) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (x : List Bool) (T T' : ℕ) (hT : f x.length ≤ T) (hT' : f x.length ≤ T') : 2 ^ T < 2 * tm.acceptCount x T ↔ 2 ^ T' < 2 * tm.acceptCount x T'

Two horizons past the halting point give the same comparison.

def Complexity.NTM.acceptsAt {k : ℕ} (tm : NTM k) (x : List Bool) (T v : ℕ) : Bool

The per-value acceptance test the counting loop performs: run the path selected by counter value v and report whether it halts accepting.

Equations

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

theorem Complexity.NTM.acceptCount_eq_zero_of_qstart_eq_qhalt {k : ℕ} {tm : NTM k} (heq : tm.qstart = tm.qhalt) (x : List Bool) (T : ℕ) : tm.acceptCount x T = 0

The degenerate machine decides the empty language. A machine that starts halted never moves, and its output tape is blank, so no choice sequence is accepting and the PP comparison fails on every input. Ruling this case out is what licenses the qstart ≠ qhalt hypothesis the delay construction needs.

theorem Complexity.NTM.not_mem_of_qstart_eq_qhalt {k : ℕ} {L : Language} {tm : NTM k} {f : ℕ → ℕ} (heq : tm.qstart = tm.qhalt) (hchar : ∀ (x : List Bool), x ∈ L ↔ 2 ^ f x.length < 2 * tm.acceptCount x (f x.length)) (x : List Bool) : x ∉ L

theorem Complexity.NTM.delayNTM_char {k : ℕ} {L : Language} {tm : NTM k} {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (hne : tm.qstart ≠ tm.qhalt) (hchar : ∀ (x : List Bool), x ∈ L ↔ 2 ^ f x.length < 2 * tm.acceptCount x (f x.length)) (x : List Bool) : x ∈ L ↔ 2 ^ (f x.length + 2) < 2 * tm.delayNTM.acceptCount x (f x.length + 2)

The PP characterisation survives the delay. NTM.delayNTM spends two extra steps and doubles the count of accepting paths; the horizon's own doubling absorbs exactly that, so the comparison 2 ^ T < 2 * acceptCount is unchanged. This is what lets the counting machine simulate a machine whose first transition ignores its choice bit — the only kind a composed machine can enter, since no stage can be handed a head at cell zero.

theorem Complexity.NTM.tally_eq_acceptCount {k : ℕ} (tm : NTM k) (x : List Bool) (T : ℕ) : tally (fun (v : ℕ) => tm.acceptsAt x T v) (2 ^ T) = tm.acceptCount x T

The tally is the accepting count. Enumerating the counter over [0, 2 ^ T) visits every choice sequence exactly once, so accumulating the acceptance test over that range counts the accepting paths.

theorem Complexity.NTM.tally_cmp_iff {k : ℕ} (tm : NTM k) (x : List Bool) (T : ℕ) : tally (fun (v : ℕ) => !tm.acceptsAt x T v) (2 ^ T) < tally (fun (v : ℕ) => tm.acceptsAt x T v) (2 ^ T) ↔ 2 ^ T < 2 * tm.acceptCount x T

The comparison the machine performs is the PP comparison.

theorem Complexity.NTM.mem_iff_tally_lt_tally_poly {k : ℕ} {L : Language} {tm : NTM k} {f : ℕ → ℕ} {p : Polynomial ℕ} (hall : tm.AllPathsHaltIn f) (hle : ∀ (n : ℕ), f n ≤ Polynomial.eval n p) (hchar : ∀ (x : List Bool), x ∈ L ↔ 2 ^ f x.length < 2 * tm.acceptCount x (f x.length)) (x : List Bool) : x ∈ L ↔ tally (fun (v : ℕ) => !tm.acceptsAt x (Polynomial.eval x.length p) v) (2 ^ Polynomial.eval x.length p) < tally (fun (v : ℕ) => tm.acceptsAt x (Polynomial.eval x.length p) v) (2 ^ Polynomial.eval x.length p)

The complete machine specification for PP. Everything on the right is something a machine performs: iterate a counter to a polynomial bound it can evaluate, simulate one path per counter value, keep two tallies, and compare them. No probability, no rationals, no quantifier over the function space, and no reference to the protocol's own time function survive.

theorem Complexity.NTM.choiceTM_placed_keepsWindow {k : ℕ} (tm : NTM k) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (x : List Bool) (m : ℕ) (c₀ : Cfg (k + 1) tm.Q) {inputLength h₀ : ℕ} (hdrop : dropChoice c₀ = tm.initCfg x) (hinv : (c₀.work (Fin.last k)).StartInvariant) (hhead : 1 ≤ (c₀.work (Fin.last k)).head) (hheads : ∀ (i : Fin (k + 1)), (c₀.work i).head ≤ h₀) (hin : c₀.input.head ≤ inputLength + h₀ + 1) (hout : c₀.output.head ≤ h₀ + 1) (D : Cfg (k + 1 + m + 1) (tm.choiceTM.liftTM m).retargetOutput.Q) : (tm.choiceTM.liftTM m).retargetOutput.reaches ((tm.choiceTM.liftTM m).retargetCfg (tm.choiceTM.liftCfg m c₀)) D → D.WithinDecisionSpace inputLength (h₀ + (f x.length + 1) + 1)

The inner call, fully placed. The path simulator sits inside a machine with m extra tapes and writes its verdict onto a work tape rather than the real output. Lifting is free and the output redirection costs one cell, so the whole placed call keeps a window one wider than the simulation's own. This is the form in which the counting machine invokes it.

The loop invariant

The counting machine carries three numbers on its tapes: the counter, the accepting tally, and the rejecting tally. tallyStep is one iteration's effect on that triple, and tallyStep_iterate is the invariant relating the state after N iterations to tally — the fact the machine's correctness proof carries through the loop.

def Complexity.NTM.tallyStep (P : ℕ → Bool) (st : ℕ × ℕ × ℕ) : ℕ × ℕ × ℕ

One iteration of the counting loop, on the triple (counter, accepting tally, rejecting tally).

Equations

• Complexity.NTM.tallyStep P st = (st.1 + 1, st.2.1 + if P st.1 = true then 1 else 0, st.2.2 + if P st.1 = true then 0 else 1)

theorem Complexity.NTM.tallyStep_iterate (P : ℕ → Bool) (N : ℕ) : (tallyStep P)^[N] (0, 0, 0) = (N, tally P N, tally (fun (v : ℕ) => !P v) N)

The loop invariant. After N iterations from the zero state, the counter reads N and the two tallies read the counts of the values below N satisfying and failing P.

theorem Complexity.NTM.mem_iff_iterate_tallyStep {k : ℕ} {L : Language} {tm : NTM k} {f : ℕ → ℕ} {p : Polynomial ℕ} (hall : tm.AllPathsHaltIn f) (hle : ∀ (n : ℕ), f n ≤ Polynomial.eval n p) (hchar : ∀ (x : List Bool), x ∈ L ↔ 2 ^ f x.length < 2 * tm.acceptCount x (f x.length)) (x : List Bool) : x ∈ L ↔ ((tallyStep fun (v : ℕ) => tm.acceptsAt x (Polynomial.eval x.length p) v)^[2 ^ Polynomial.eval x.length p] (0, 0, 0)).2.2 < ((tallyStep fun (v : ℕ) => tm.acceptsAt x (Polynomial.eval x.length p) v)^[2 ^ Polynomial.eval x.length p] (0, 0, 0)).2.1

What the counting machine must compute, as a single iterated function. Running the loop 2 ^ T times from the zero state and comparing the two tallies decides membership. This is the form the machine's Hoare contract will take: an iteration count, one step function, and a comparison of two components of the final state.

theorem Complexity.NTM.tallyLoop_hoareTime {n : ℕ} (tmBody tmTest : TM n) (cIdx aIdx rIdx : Fin n) (I : Tape) (rest : Fin n → Tape) (P : ℕ → Bool) {post : TapePred n} (N b : ℕ) (hstep : ∀ j < N, ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), tallyState cIdx aIdx rIdx I rest ((tallyStep P)^[j] (0, 0, 0)) inp work out → ∃ (inp' : Tape) (work' : Fin n → Tape) (out' : Tape), ∃ t ≤ b, (tmBody.loopTM tmTest).reachesIn t { state := (tmBody.loopTM tmTest).qstart, input := inp, work := work, output := out } { state := (tmBody.loopTM tmTest).qstart, input := inp', work := work', output := out' } ∧ tallyState cIdx aIdx rIdx I rest ((tallyStep P)^[j + 1] (0, 0, 0)) inp' work' out') (hstop : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), tallyState cIdx aIdx rIdx I rest ((tallyStep P)^[N] (0, 0, 0)) inp work out → ∃ (c' : Cfg n (tmBody.loopTM tmTest).Q), ∃ t ≤ b, (tmBody.loopTM tmTest).reachesIn t { state := (tmBody.loopTM tmTest).qstart, input := inp, work := work, output := out } c' ∧ (tmBody.loopTM tmTest).halted c' ∧ post c'.input c'.work c'.output) : (tmBody.loopTM tmTest).HoareTime (tallyState cIdx aIdx rIdx I rest (0, 0, 0)) post ((N + 1) * b)

The counting loop, granted a body that realises one step. With the tape state of tallyState and the index read back by tallyIdx, the indexed loop rule reduces the whole run to two obligations: one iteration advances the state by tallyStep, and the loop halts at the final count. Everything about counting — the invariant, the variant, the fuel — is discharged here.

def Complexity.NTM.outSlot (s : Γw) : Tape

The output tape as the counting loop uses it: a single verdict cell, and blanks beyond it. TM.loopTM inspects exactly this cell after rewinding the output, so the loop's whole interaction with its output tape is the choice of one symbol.

Equations

• Complexity.NTM.outSlot s = { head := 1, cells := fun (j : ℕ) => if j = 0 then Complexity.Γ.start else if j = 1 then s.toΓ else Complexity.Γ.blank }

@[simp]

theorem Complexity.NTM.outSlot_head (s : Γw) : (outSlot s).head = 1

@[simp]

theorem Complexity.NTM.outSlot_cells_zero (s : Γw) : (outSlot s).cells 0 = Γ.start

@[simp]

theorem Complexity.NTM.outSlot_cells_one (s : Γw) : (outSlot s).cells 1 = s.toΓ

theorem Complexity.NTM.outSlot_parked (s : Γw) : TM.Parked (outSlot s)

A verdict slot never carries a stray left marker, so it is parked.

theorem Complexity.NTM.outSlot_cells_one_eq_one_iff (s : Γw) : (outSlot s).cells 1 = Γ.one ↔ s = Γw.one

The verdict cell holds 1 exactly when the slot was written with 1.

def Complexity.NTM.tallyPre {n : ℕ} (cIdx aIdx rIdx : Fin n) (I : Tape) (rest : Fin n → Tape) (P : ℕ → Bool) (v : ℕ) : TM.TapePred n

The tape state the counting loop sits in at its own start state. Every tape is named outright: the three numeric registers hold the count and the two tallies, every other work tape is back at its resting contents, and the output carries the previous check's verdict, which for a continuing iteration is 0.

Equations

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

def Complexity.NTM.tallyPost {n : ℕ} (cIdx aIdx rIdx : Fin n) (I : Tape) (rest : Fin n → Tape) (P : ℕ → Bool) (N v : ℕ) : TM.TapePred n

The tape state the loop's test leaves behind: the same registers, with the verdict slot holding 1 exactly when the count has reached its horizon.

Equations

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

theorem Complexity.NTM.tallyPre_loopParked {n : ℕ} (cIdx aIdx rIdx : Fin n) (I : Tape) (rest : Fin n → Tape) (P : ℕ → Bool) (hI : TM.Parked I) (hrest : ∀ (i : Fin n), TM.Parked (rest i)) (v : ℕ) {inp : Tape} {work : Fin n → Tape} {out : Tape} (h : tallyPre cIdx aIdx rIdx I rest P v inp work out) : TM.LoopParked inp work out

A pinned tally state is parked on every tape, given that the resting tapes are.

theorem Complexity.NTM.tallyPost_loopParked {n : ℕ} (cIdx aIdx rIdx : Fin n) (I : Tape) (rest : Fin n → Tape) (P : ℕ → Bool) (hI : TM.Parked I) (hrest : ∀ (i : Fin n), TM.Parked (rest i)) (N v : ℕ) {inp : Tape} {work : Fin n → Tape} {out : Tape} (h : tallyPost cIdx aIdx rIdx I rest P N v inp work out) : TM.LoopParked inp work out

The same, for the state the test leaves behind.

theorem Complexity.NTM.tallyIdx_tallyPre {n : ℕ} (cIdx aIdx rIdx : Fin n) (I : Tape) (rest : Fin n → Tape) (P : ℕ → Bool) (v : ℕ) {inp : Tape} {work : Fin n → Tape} {out : Tape} (h : tallyPre cIdx aIdx rIdx I rest P v inp work out) : tallyIdx cIdx inp work out = v

Reading the count back off a pinned tally state.

theorem Complexity.NTM.tallyLoop_hoareTime_of_hoare {n : ℕ} (tmBody tmTest : TM n) (cIdx aIdx rIdx : Fin n) (I : Tape) (rest : Fin n → Tape) (P : ℕ → Bool) (mid : ℕ → TM.TapePred n) (N bBody bTest : ℕ) (hN : 1 ≤ N) (hI : TM.Parked I) (hrest : ∀ (i : Fin n), TM.Parked (rest i)) (hbody : ∀ v < N, tmBody.HoareTime (tallyPre cIdx aIdx rIdx I rest P v) (mid v) bBody) (hmid : ∀ (v : ℕ) (inp : Tape) (work : Fin n → Tape) (out : Tape), mid v inp work out → TM.LoopParked inp work out) (htest : ∀ v < N, tmTest.HoareTime (mid v) (tallyPost cIdx aIdx rIdx I rest P N (v + 1)) bTest) : (tmBody.loopTM tmTest).HoareTime (tallyPre cIdx aIdx rIdx I rest P 0) (tallyPost cIdx aIdx rIdx I rest P N N) (N * (bBody + bTest + 5))

The counting loop from two Hoare contracts. This is the interface the machine construction actually meets: a contract saying the body advances the tally by one index, and a contract saying the test reports whether the horizon has been reached.

TM.loopTM is a do-while — its body runs before its first test — so a loop that halts after N tallies performs its N-th body pass on the terminating iteration, not on a continuing one. The indexed rule is therefore applied at N - 1, which is why the body is never asked to run at index N and why 1 ≤ N is needed.

theorem Complexity.NTM.tallyLoop_keepsWindow_of_hoare {n : ℕ} (tmBody tmTest : TM n) (cIdx aIdx rIdx : Fin n) (I : Tape) (rest : Fin n → Tape) (P : ℕ → Bool) (mid : ℕ → TM.TapePred n) (N bBody bTest inputLength : ℕ) (hN : 1 ≤ N) (hI : TM.Parked I) (hrest : ∀ (i : Fin n), TM.Parked (rest i)) (hIhead : I.head ≤ inputLength + 1) (hrestHead : ∀ (i : Fin n), (rest i).head ≤ 1) (hbody : ∀ v < N, tmBody.HoareTime (tallyPre cIdx aIdx rIdx I rest P v) (mid v) bBody) (hmid : ∀ (v : ℕ) (inp : Tape) (work : Fin n → Tape) (out : Tape), mid v inp work out → TM.LoopParked inp work out) (htest : ∀ v < N, tmTest.HoareTime (mid v) (tallyPost cIdx aIdx rIdx I rest P N (v + 1)) bTest) (inp : Tape) (work : Fin n → Tape) (out : Tape) : tallyPre cIdx aIdx rIdx I rest P 0 inp work out → ∀ (c : Cfg n (tmBody.loopTM tmTest).Q), (tmBody.loopTM tmTest).reaches { state := (tmBody.loopTM tmTest).qstart, input := inp, work := work, output := out } c → c.WithinDecisionSpace inputLength (1 + (bBody + bTest + 5))

The counting loop keeps a window one iteration wide. The loop runs exponentially many iterations, so no bound derived from its total running time can be polynomial; what is polynomial is a single iteration, and every state the loop returns to has all its heads at cell one.

theorem Complexity.NTM.choiceTM_choiceCells {k : ℕ} (tm : NTM k) {c : Cfg (k + 1) tm.Q} (hinv : (c.work (Fin.last k)).StartInvariant) (hhead : 1 ≤ (c.work (Fin.last k)).head) (c' : Cfg (k + 1) tm.choiceTM.Q) : tm.choiceTM.reaches c c' → (c'.work (Fin.last k)).cells = (c.work (Fin.last k)).cells ∧ (c'.work (Fin.last k)).StartInvariant ∧ 1 ≤ (c'.work (Fin.last k)).head

The path simulation leaves the counter's digits alone. choiceTM writes every choice bit back unchanged and only advances the head, so the counter tape's contents survive the run — the body has merely to rewind the head to restore the encoding for the next iteration.

theorem Complexity.NTM.choiceStream_eq_choicesOfNat {k : ℕ} {tm : NTM k} (c : Cfg (k + 1) tm.Q) (v T : ℕ) (h : (c.work (Fin.last k)).HasBinaryNat v) (j : Fin T) : choiceStream c ↑j = choicesOfNat T v j

A counter tape reads exactly as the choice sequence of its value. Combining the encoding bridge with the bit correspondence: if the choice tape carries the canonical representation of v, then the stream the path simulator consumes is choicesOfNat T v — no padding, no copy, and no fixed-width counter.

theorem Complexity.NTM.hasBinaryNat_startInvariant {t : Tape} {v : ℕ} (h : t.HasBinaryNat v) : t.StartInvariant

A canonical binary tape carries its left marker and nothing else does.

theorem Complexity.NTM.choiceTM_dropChoice_eq {k : ℕ} (tm : NTM k) (x : List Bool) (T v : ℕ) (c : Cfg (k + 1) tm.Q) (hdrop : dropChoice c = tm.initCfg x) (hv : (c.work (Fin.last k)).HasBinaryNat v) : ∃ (c' : Cfg (k + 1) tm.choiceTM.Q), ∃ t ≤ T, tm.choiceTM.reachesIn t c c' ∧ dropChoice c' = tm.trace T (choicesOfNat T v) (tm.initCfg x)

What the simulation computes from a counter value. Started with the counter tape carrying v and the machine's own tapes in their initial configuration, the path simulator produces exactly the trace of tm along the choice sequence choicesOfNat T v.

theorem Complexity.NTM.choiceTM_delay_dropChoice_eq {k : ℕ} (tm : NTM k) (x : List Bool) (hne : tm.qstart ≠ tm.qhalt) (T v : ℕ) (hT : 1 ≤ T) (c : Cfg (k + 1) tm.delayNTM.Q) (hdrop : dropChoice c = tm.delayNTM.trace 1 (fun (x : Fin 1) => false) (tm.delayNTM.initCfg x)) (hv : (c.work (Fin.last k)).HasBinaryNat v) : ∃ (c' : Cfg (k + 1) tm.delayNTM.choiceTM.Q), ∃ t ≤ T, tm.delayNTM.choiceTM.reachesIn t c c' ∧ dropChoice c' = tm.delayEmbed (tm.trace T (choicesOfNat T v) (tm.initCfg x))

What the loop body's simulation computes. Started from the delayed machine's post-sentinel configuration — every head at cell one, the counter carrying v, the machine's own tapes blank — the path simulator produces exactly the source machine's trace along the choice sequence v encodes.

Two corrections cancel here. Entering after the sentinel step costs one step of the delayed machine, and the delay itself costs one; together they are exactly the two steps NTM.delayNTM_trace_initCfg charges, so the horizon T on the counter is the source machine's own horizon, with no off-by-one left over.

theorem Complexity.NTM.choiceTM_delay_haltsIn {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) (c : Cfg (k + 1) tm.delayNTM.Q) (hdrop : dropChoice c = tm.delayNTM.trace 1 (fun (x : Fin 1) => false) (tm.delayNTM.initCfg x)) (hv : (c.work (Fin.last k)).HasBinaryNat v) : ∃ (c' : Cfg (k + 1) tm.delayNTM.choiceTM.Q), ∃ t ≤ T, tm.delayNTM.choiceTM.reachesIn t c c' ∧ tm.delayNTM.choiceTM.halted c' ∧ decide (c'.output.cells 1 = Γ.one) = tm.acceptsAt x T v

The loop body's simulation, run to a halt with its verdict. The counter's value selects a path, the simulation follows it to the end, and the halted configuration's verdict cell holds exactly the bit the tally is counting.

theorem Complexity.NTM.choiceTM_verdict {k : ℕ} (tm : NTM k) (x : List Bool) (T v : ℕ) {c' : Cfg (k + 1) tm.Q} (heq : dropChoice c' = tm.trace T (choicesOfNat T v) (tm.initCfg x)) : decide (c'.state = tm.qhalt ∧ c'.output.cells 1 = Γ.one) = tm.acceptsAt x T v

The verdict the loop body reads is the enumeration's acceptance test.

theorem Complexity.NTM.tallyLoop_hoareTime_of_body {n : ℕ} (tmBody tmTest : TM n) (cIdx aIdx rIdx : Fin n) (I : Tape) (rest : Fin n → Tape) (P : ℕ → Bool) {post : TapePred n} (N b : ℕ) (hbody : ∀ (v a r : ℕ), v < N → ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), tallyState cIdx aIdx rIdx I rest (v, a, r) inp work out → ∃ (inp' : Tape) (work' : Fin n → Tape) (out' : Tape), ∃ t ≤ b, (tmBody.loopTM tmTest).reachesIn t { state := (tmBody.loopTM tmTest).qstart, input := inp, work := work, output := out } { state := (tmBody.loopTM tmTest).qstart, input := inp', work := work', output := out' } ∧ tallyState cIdx aIdx rIdx I rest (v + 1, a + if P v = true then 1 else 0, r + if P v = true then 0 else 1) inp' work' out') (hstop : ∀ (inp : Tape) (work : Fin n → Tape) (out : Tape), tallyState cIdx aIdx rIdx I rest (N, tally P N, tally (fun (v : ℕ) => !P v) N) inp work out → ∃ (c' : Cfg n (tmBody.loopTM tmTest).Q), ∃ t ≤ b, (tmBody.loopTM tmTest).reachesIn t { state := (tmBody.loopTM tmTest).qstart, input := inp, work := work, output := out } c' ∧ (tmBody.loopTM tmTest).halted c' ∧ post c'.input c'.work c'.output) : (tmBody.loopTM tmTest).HoareTime (tallyState cIdx aIdx rIdx I rest (0, 0, 0)) post ((N + 1) * b)

The counting loop, granted only that the body advances the triple. The body's obligation no longer mentions iterates or tallies: from a state holding (v, a, r) it must reach the state holding (v + 1, a + [P v], r + [¬P v]). All the counting bookkeeping is discharged here.

theorem Complexity.NTM.choiceTM_lifted_keepsWindow {k : ℕ} (tm : NTM k) {f : ℕ → ℕ} (hall : tm.AllPathsHaltIn f) (x : List Bool) (m : ℕ) (c₀ : Cfg (k + 1) tm.Q) {inputLength h₀ : ℕ} (hdrop : dropChoice c₀ = tm.initCfg x) (hinv : (c₀.work (Fin.last k)).StartInvariant) (hhead : 1 ≤ (c₀.work (Fin.last k)).head) (hheads : ∀ (i : Fin (k + 1)), (c₀.work i).head ≤ h₀) (hin : c₀.input.head ≤ inputLength + h₀ + 1) (hout : c₀.output.head ≤ h₀ + 1) (D : Cfg (k + 1 + m) (tm.choiceTM.liftTM m).Q) : (tm.choiceTM.liftTM m).reaches (tm.choiceTM.liftCfg m c₀) D → D.WithinDecisionSpace inputLength (h₀ + (f x.length + 1))

The inner call as the loop's test, placed. TM.ifTM branches on the real output tape's verdict cell, and the path simulator already writes tm's verdict there — so the simulation can serve directly as the conditional's test, with no output retargeting. Only the lift into the larger tape space is needed, and that is free.