One pass of the witness enumerator

⚠️ Unreviewed by Bolton

An iteration takes the count v, tests the witness it denotes, and leaves the loop one count further along. In order:

1. blank the verdict slot, so the pass starts from a known output;
2. emit pair x w onto the first pair tape;
3. rewind the input copy, the witness, and that tape, which the emitter left mid-scan;
4. copy the pair into virtual-input shape on the tape the matrix machine reads;
5. run the matrix machine, which writes its verdict to the verdict tape;
6. rewind the verdict tape, since the matrix machine left its head wherever it halted;
7. publish that verdict into the slot;
8. bump the tally the slot names and advance the counter;
9. advance the witness in step with the counter;
10. blank everything the pass dirtied.

Steps 8 and 10 are the counting machine's own — TM.tallyBumpTM and TM.wipeRewindTM — and step 9 is what makes the loop's resting bank depend on the count.

Main results

• PolyExists.copyPairTM — the copy into virtual-input shape
• PolyExists.bodyTM — one pass of the enumerator
• PolyExists.enumBank — the tapes an iteration starts from, and its values at the named indices
• PolyExists.blankSlot_hoareTime — the first stage's contract

def Complexity.PolyExists.copyPairTM (k : ℕ) : TM (enumTapes k)

Move the emitted pair onto the tape the matrix machine reads, in the shape it expects.

Equations

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

def Complexity.PolyExists.bodyTM {k : ℕ} (M : TM k) : TM (enumTapes k)

One pass of the witness enumerator.

Equations

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

The bank the loop rests in

def Complexity.PolyExists.enumBank (k : ℕ) (x : List Bool) (N H v a r : ℕ) : Fin (enumTapes k) → Tape

The tapes at count v with tallies a and r: the loop's three registers over the resting bank.

Equations

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

theorem Complexity.PolyExists.enumBank_of_ne (k : ℕ) (x : List Bool) (N H v a r : ℕ) (i : Fin (enumTapes k)) (hc : i ≠ cIdx k) (ha : i ≠ aIdx k) (hr : i ≠ rIdx k) : enumBank k x N H v a r i = enumRest k x N H (v + 1) i

A tape that is none of the loop's three registers rests where the bank puts it.

theorem Complexity.PolyExists.ne_tallyRegs {k : ℕ} (i : Fin (enumTapes k)) (h2 : ↑i ≠ 3 + k + 2) (h5 : ↑i ≠ 3 + k + 5) (h8 : ↑i ≠ 3 + k + 8) : i ≠ cIdx k ∧ i ≠ aIdx k ∧ i ≠ rIdx k

theorem Complexity.PolyExists.x_ne_regs (k : ℕ) : xIdx k ≠ cIdx k ∧ xIdx k ≠ aIdx k ∧ xIdx k ≠ rIdx k

theorem Complexity.PolyExists.w_ne_regs (k : ℕ) : wIdx k ≠ cIdx k ∧ wIdx k ≠ aIdx k ∧ wIdx k ≠ rIdx k

theorem Complexity.PolyExists.y1_ne_regs (k : ℕ) : y1Idx k ≠ cIdx k ∧ y1Idx k ≠ aIdx k ∧ y1Idx k ≠ rIdx k

theorem Complexity.PolyExists.y_ne_regs (k : ℕ) : yIdx k ≠ cIdx k ∧ yIdx k ≠ aIdx k ∧ yIdx k ≠ rIdx k

theorem Complexity.PolyExists.v_ne_regs (k : ℕ) : vIdx k ≠ cIdx k ∧ vIdx k ≠ aIdx k ∧ vIdx k ≠ rIdx k

theorem Complexity.PolyExists.n_ne_regs (k : ℕ) : nIdx k ≠ cIdx k ∧ nIdx k ≠ aIdx k ∧ nIdx k ≠ rIdx k

theorem Complexity.PolyExists.res_ne_regs (k : ℕ) : resIdx k ≠ cIdx k ∧ resIdx k ≠ aIdx k ∧ resIdx k ≠ rIdx k

theorem Complexity.PolyExists.z_ne_regs (k : ℕ) : zIdx k ≠ cIdx k ∧ zIdx k ≠ aIdx k ∧ zIdx k ≠ rIdx k

theorem Complexity.PolyExists.reg_ne_regs (k : ℕ) : regIdx k ≠ cIdx k ∧ regIdx k ≠ aIdx k ∧ regIdx k ≠ rIdx k

@[simp]

theorem Complexity.PolyExists.enumBank_x (k : ℕ) (x : List Bool) (N H v a r : ℕ) : enumBank k x N H v a r (xIdx k) = strTape x

@[simp]

theorem Complexity.PolyExists.enumBank_w (k : ℕ) (x : List Bool) (N H v a r : ℕ) : enumBank k x N H v a r (wIdx k) = strTape (dropTop (v + 1))

theorem Complexity.PolyExists.enumRest_blank (k : ℕ) (x : List Bool) (N H v : ℕ) (i : Fin (enumTapes k)) (hx : i ≠ xIdx k) (hw : i ≠ wIdx k) (hn : i ≠ nIdx k) (hreg : i ≠ regIdx k) : enumRest k x N H v i = TM.blankTape

Every scratch tape rests blank.

theorem Complexity.PolyExists.enumBank_blank (k : ℕ) (x : List Bool) (N H v a r : ℕ) (i : Fin (enumTapes k)) (hc : i ≠ cIdx k) (ha : i ≠ aIdx k) (hr : i ≠ rIdx k) (hx : i ≠ xIdx k) (hw : i ≠ wIdx k) (hn : i ≠ nIdx k) (hreg : i ≠ regIdx k) : enumBank k x N H v a r i = TM.blankTape

@[simp]

theorem Complexity.PolyExists.enumBank_y1 (k : ℕ) (x : List Bool) (N H v a r : ℕ) : enumBank k x N H v a r (y1Idx k) = TM.blankTape

@[simp]

theorem Complexity.PolyExists.enumBank_z (k : ℕ) (x : List Bool) (N H v a r : ℕ) : enumBank k x N H v a r (zIdx k) = TM.blankTape

theorem Complexity.PolyExists.enumBank_parked (k : ℕ) (x : List Bool) (N H v a r : ℕ) (i : Fin (enumTapes k)) : TM.Parked (enumBank k x N H v a r i)

The bank is parked on every tape.

theorem Complexity.PolyExists.natTape_startInvariant (v : ℕ) : (natTape v).StartInvariant

theorem Complexity.PolyExists.strTape_cells_zero (l : List Bool) : (strTape l).cells 0 = Γ.start

theorem Complexity.PolyExists.enumBank_startInvariant (k : ℕ) (x : List Bool) (N H v a r : ℕ) (i : Fin (enumTapes k)) : (enumBank k x N H v a r i).StartInvariant

The bank satisfies the left-marker invariant on every tape, which every rewind, park and wipe downstream asks of the tapes it carries.

theorem Complexity.PolyExists.enumBank_head (k : ℕ) (x : List Bool) (N H v a r : ℕ) (i : Fin (enumTapes k)) : (enumBank k x N H v a r i).head = 1

Every tape of the bank is parked at cell one.

theorem Complexity.PolyExists.natTape_head_one (v : ℕ) : (natTape v).head = 1

theorem Complexity.PolyExists.blankSlot_hoareTime (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) : (TM.writeOutputBitTM (zIdx k)).HoareTime (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ work = enumBank k x N H v a r ∧ ∃ (s : Γw), s ≠ Γw.one ∧ out = NTM.outSlot s) (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ work = enumBank k x N H v a r ∧ out = TM.blankTape) 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; everything downstream — the emitter, the matrix machine, the wipe — needs the real output tape blank.

theorem Complexity.PolyExists.blankTape_eq_parkedBlank : TM.blankTape = TM.parkedBlank

def Complexity.PolyExists.afterPair (k : ℕ) (x : List Bool) (N H v a r : ℕ) : Fin (enumTapes k) → Tape

The tapes after the pair has been emitted and everything the emitter scanned rewound: the bank, with the pair now on its tape.

Equations

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

def Complexity.PolyExists.midEmit (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (B : ℕ) : TM.TapePred (enumTapes k)

What the emitter leaves behind: the pair on its tape, both sources with their cells intact, every other tape untouched, and no head further out than the stage is long.

Equations

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

theorem Complexity.PolyExists.emit_hoareTime (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) (hISI : I.StartInvariant) (B : ℕ) (hB : 1 + TM.pairInputWorkTime x (dropTop (v + 1)) ≤ B) : (emitTM k).HoareTime (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ work = enumBank k x N H v a r ∧ out = TM.blankTape) (midEmit k x N H v a r I B) (TM.pairInputWorkTime x (dropTop (v + 1)))

The emitting stage's contract.

theorem Complexity.PolyExists.pairTargets_nodup (k : ℕ) : [xIdx k, wIdx k, y1Idx k].Nodup

theorem Complexity.PolyExists.mem_pairTargets_iff (k : ℕ) (j : Fin (enumTapes k)) : j ∈ [xIdx k, wIdx k, y1Idx k] ↔ TM.placeWorkInMiddle 0 3 j

A tape of the layout is one of the three the emitter touches exactly when it is inside the emitter's block.

theorem Complexity.PolyExists.parkPair_hoareTime (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hISI : I.StartInvariant) (hIhead : I.head = 1) (B : ℕ) (hB : 1 ≤ B) : (TM.parkRewindTM [xIdx k, wIdx k, y1Idx k]).HoareTime (midEmit k x N H v a r I B) (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ work = afterPair k x N H v a r ∧ out = TM.blankTape) (1 + 1 + (2 * (max (B + 2) (3 * (B + 3) + 1) + 1) + 1))

The rewinding stage's contract. The emitter left three heads mid-scan; this puts them back at cell one, which pins every tape again.

theorem Complexity.PolyExists.enumBank_blank_of_val (k : ℕ) (x : List Bool) (N H v a r : ℕ) (i : Fin (enumTapes k)) (h2 : 2 ≤ ↑i) (hlt : ↑i < 3 + k + 2) : enumBank k x N H v a r i = TM.blankTape

Every tape of the scratch block rests blank: the emitter's target, the matrix machine's own tapes, the tape it reads and the one it writes.

@[simp]

theorem Complexity.PolyExists.enumBank_y (k : ℕ) (x : List Bool) (N H v a r : ℕ) : enumBank k x N H v a r (yIdx k) = TM.blankTape

@[simp]

theorem Complexity.PolyExists.enumBank_v (k : ℕ) (x : List Bool) (N H v a r : ℕ) : enumBank k x N H v a r (vIdx k) = TM.blankTape

def Complexity.PolyExists.afterCopy (k : ℕ) (x : List Bool) (N H v a r : ℕ) : Fin (enumTapes k) → Tape

The tapes after the pair has been moved into the shape the matrix machine reads: the emitter's target keeps its contents with its head left past them, and the matrix machine's input tape now holds the pair.

Equations

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

theorem Complexity.PolyExists.copyPair_hoareTime (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) : (copyPairTM k).HoareTime (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ work = afterPair k x N H v a r ∧ out = TM.blankTape) (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ work = afterCopy k x N H v a r ∧ out = TM.blankTape) (2 * (pair x (dropTop (v + 1))).length + 5)

The copying stage's contract.

theorem Complexity.PolyExists.matrixEntry_afterCopy {k : ℕ} (M : TM k) (x : List Bool) (N H v a r : ℕ) (I : Tape) : matrixEntry M (afterCopy k x N H v a r) (pair x (dropTop (v + 1))) I = afterCopy k x N H v a r

The layout and the placement agree. The tapes the copy stage leaves behind are exactly the ones the placed matrix machine expects to be entered with: its own scratch blank, the pair on the tape it reads, the verdict tape blank, and the enumerator's registers on either side.

theorem Complexity.PolyExists.afterCopy_startInvariant (k : ℕ) (x : List Bool) (N H v a r : ℕ) (i : Fin (enumTapes k)) : (afterCopy k x N H v a r i).StartInvariant

theorem Complexity.PolyExists.afterCopy_head_pos (k : ℕ) (x : List Bool) (N H v a r : ℕ) (i : Fin (enumTapes k)) : 1 ≤ (afterCopy k x N H v a r i).head

theorem Complexity.PolyExists.matrix_hoareTime {k : ℕ} (M : TM k) {L : Language} {T S : ℕ → ℕ} (hdec : M.DecidesInTime L T) (hdecS : M.DecidesInSpace L S) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) (hISI : I.StartInvariant) (Hb : ℕ) (hHS : (pair x (dropTop (v + 1))).length + S (pair x (dropTop (v + 1))).length + 2 ≤ Hb) : (matrixTM M).HoareTime (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ work = afterCopy k x N H v a r ∧ out = TM.blankTape) (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ out = TM.blankTape ∧ (pair x (dropTop (v + 1)) ∈ L → (work (vIdx k)).cells 1 = Γ.one) ∧ (pair x (dropTop (v + 1)) ∉ L → (work (vIdx k)).cells 1 = Γ.zero) ∧ (∀ (i : Fin (3 + (k + 2) + 7)), ¬TM.placeWorkInMiddle 3 (k + 2) i → work i = afterCopy k x N H v a r i) ∧ ∀ (i : Fin (3 + (k + 2) + 7)), TM.placeWorkInMiddle 3 (k + 2) i → (work i).StartInvariant ∧ (work i).head ≤ Hb ∧ ∀ (j : ℕ), Hb < j → (work i).cells j = Γ.blank) (T (pair x (dropTop (v + 1))).length)

The evaluating stage's contract, in the enumerator's own terms.

def Complexity.PolyExists.midMatrix (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (Hb : ℕ) (b : Bool) : TM.TapePred (enumTapes k)

What the matrix machine leaves behind: its verdict on the verdict tape, the enumerator's own tapes untouched, and its block dirty but bounded.

Equations

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

theorem Complexity.PolyExists.matrix_hoareTime_bool {k : ℕ} (M : TM k) {L : Language} {T S : ℕ → ℕ} (hdec : M.DecidesInTime L T) (hdecS : M.DecidesInSpace L S) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) (hISI : I.StartInvariant) (Hb : ℕ) (hHS : (pair x (dropTop (v + 1))).length + S (pair x (dropTop (v + 1))).length + 2 ≤ Hb) (b : Bool) (hb : b = true ↔ pair x (dropTop (v + 1)) ∈ L) : (matrixTM M).HoareTime (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ work = afterCopy k x N H v a r ∧ out = TM.blankTape) (midMatrix k x N H v a r I Hb b) (T (pair x (dropTop (v + 1))).length)

The evaluating stage, with its verdict read as a Boolean.

def Complexity.PolyExists.midParked (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (Hb : ℕ) (b : Bool) : TM.TapePred (enumTapes k)

The verdict tape rewound: the pass can read the bit it published.

Equations

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

theorem Complexity.PolyExists.parkVerdict_hoareTime (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hISI : I.StartInvariant) (hIhead : I.head = 1) (Hb : ℕ) (hHb : 1 ≤ Hb) (b : Bool) : (TM.parkRewindTM [vIdx k]).HoareTime (midMatrix k x N H v a r I Hb b) (midParked k x N H v a r I Hb b) (1 + 1 + (2 * (max (Hb + 2) (1 * (Hb + 3) + 1) + 1) + 1))

Rewinding the verdict tape. The matrix machine halts wherever it likes; the bit it wrote is at cell one, so the head has to go back there before the pass can publish it.

theorem Complexity.PolyExists.readBackWrite_one_iff (s : Γ) : TM.readBackWrite s = Γw.one ↔ s = Γ.one

Reading a cell back as a writable symbol turns it into 1 exactly when it was 1.

def Complexity.PolyExists.midPublish (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (Hb : ℕ) (b : Bool) : TM.TapePred (enumTapes k)

The verdict published into the slot, where the tally bump can branch on it.

Equations

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

theorem Complexity.PolyExists.publishVerdict_hoareTime (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) (Hb : ℕ) (b : Bool) : (TM.writeOutputBitTM (vIdx k)).HoareTime (midParked k x N H v a r I Hb b) (midPublish k x N H v a r I Hb b) 1

Publishing the verdict. The bit under the verdict tape's head is copied into the output slot, which is the only channel between a work tape and the real output.

@[simp]

theorem Complexity.PolyExists.enumBank_c (k : ℕ) (x : List Bool) (N H v a r : ℕ) : enumBank k x N H v a r (cIdx k) = natTape v

@[simp]

theorem Complexity.PolyExists.enumBank_a (k : ℕ) (x : List Bool) (N H v a r : ℕ) : enumBank k x N H v a r (aIdx k) = natTape a

@[simp]

theorem Complexity.PolyExists.enumBank_r (k : ℕ) (x : List Bool) (N H v a r : ℕ) : enumBank k x N H v a r (rIdx k) = natTape r

theorem Complexity.PolyExists.afterCopy_of_ne (k : ℕ) (x : List Bool) (N H v a r : ℕ) (i : Fin (enumTapes k)) (h1 : i ≠ y1Idx k) (h2 : i ≠ yIdx k) : afterCopy k x N H v a r i = enumBank k x N H v a r i

theorem Complexity.PolyExists.afterCopy_outside (k : ℕ) (x : List Bool) (N H v a r : ℕ) (i : Fin (enumTapes k)) (hm : ¬TM.placeWorkInMiddle 3 (k + 2) i) (h1 : i ≠ y1Idx k) : afterCopy k x N H v a r i = enumBank k x N H v a r i

A tape outside the matrix machine's block is neither of the two the copy stage disturbed.

def Complexity.PolyExists.midBump (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (Hb : ℕ) (b : Bool) : TM.TapePred (enumTapes k)

What the tally bump leaves: the counter advanced, one tally bumped, and the slot blank again.

Equations

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

theorem Complexity.PolyExists.tallyBump_hoareTime (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) (hIz : I.cells 0 = Γ.start) (Hb : ℕ) (b : Bool) : (TM.tallyBumpTM (cIdx k) (aIdx k) (rIdx k) (zIdx k)).HoareTime (midPublish k x N H v a r I Hb b) (midBump k x N H v a r I Hb b) (3 * (max (1 + 1 + max (TM.binarySuccTime a) (TM.binarySuccTime r) + 5) (TM.binarySuccTime v) + 1) + 1)

The tally bump. The slot the previous stage published names which tally to advance; the counter advances with it, and the slot is blanked so that the wipe can run.

def Complexity.PolyExists.midBumped (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (Hb : ℕ) (b : Bool) : TM.TapePred (enumTapes k)

The witness advanced in step with the counter.

Equations

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

theorem Complexity.PolyExists.witnessBump_hoareTime (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) (Hb : ℕ) (b : Bool) : (TM.binaryBumpTM (wIdx k)).HoareTime (midBump k x N H v a r I Hb b) (midBumped k x N H v a r I Hb b) (TM.binaryBumpTime (dropTop (v + 1)))

Advancing the witness. The counter has just moved on, and TM.binaryBumpTM moves the witness with it: PolyExists.dropTop_succ says the string the next count denotes is exactly the zero-extending increment of this one.

theorem Complexity.PolyExists.enumRest_eq_of_ne_w (k : ℕ) (x : List Bool) (N H v v' : ℕ) (i : Fin (enumTapes k)) (hw : i ≠ wIdx k) : enumRest k x N H v i = enumRest k x N H v' i

The resting bank depends on the count only through the witness.

theorem Complexity.PolyExists.wipe_hoareTime (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) (hISI : I.StartInvariant) (Hb : ℕ) (b : Bool) (hHb : Hb + 1 ≤ H) (hpairH : (pair x (dropTop (v + 1))).length + 1 ≤ H) : (TM.wipeRewindTM (scratchTargets k) (regIdx k)).HoareTime (midBumped k x N H v a r I Hb b) (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ work = enumBank k x N H (v + 1) (a + if b = true then 1 else 0) (r + if b = true then 0 else 1) ∧ out = TM.blankTape) ((scratchTargets k).length * (H + 4) + H * 4 + 8 + 1 + ((scratchTargets k).length * (H + 4) + 1))

The wipe, and the bridge back to the loop invariant. Blanking everything the pass dirtied turns the bank into the one the loop's state names at the next count.

Chaining the pass

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

A phase boundary parks every tape it crosses.

theorem Complexity.PolyExists.trans_id_of_parked {k : ℕ} {inp : Tape} {work : Fin (enumTapes k) → Tape} {out : Tape} (hi : TM.Parked inp) (hw : ∀ (i : Fin (enumTapes k)), TM.Parked (work i)) (ho : TM.Parked out) : TM.transitionInput inp = inp ∧ (fun (i : Fin (enumTapes k)) => TM.transitionTape (work i)) = work ∧ TM.transitionTape out = out

A phase boundary is the identity on parked tapes.

theorem Complexity.PolyExists.afterPair_parked (k : ℕ) (x : List Bool) (N H v a r : ℕ) (i : Fin (enumTapes k)) : TM.Parked (afterPair k x N H v a r i)

theorem Complexity.PolyExists.afterCopy_parked (k : ℕ) (x : List Bool) (N H v a r : ℕ) (i : Fin (enumTapes k)) : TM.Parked (afterCopy k x N H v a r i)

theorem Complexity.PolyExists.midEmit_trans (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) (B : ℕ) (hB : 1 ≤ B) (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) (h : midEmit k x N H v a r I B inp work out) : midEmit k x N H v a r I B (TM.transitionInput inp) (fun (i : Fin (enumTapes k)) => TM.transitionTape (work i)) (TM.transitionTape out)

The seam after the emitter. The emitter can leave a head on the marker; the boundary step moves it off, and everything the next stage needs survives.

theorem Complexity.PolyExists.midMatrix_trans (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) (Hb : ℕ) (hHb : 1 ≤ Hb) (b : Bool) (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) (h : midMatrix k x N H v a r I Hb b inp work out) : midMatrix k x N H v a r I Hb b (TM.transitionInput inp) (fun (i : Fin (enumTapes k)) => TM.transitionTape (work i)) (TM.transitionTape out)

The seam after the matrix machine. Same story: the machine may halt with a head on the marker, and the boundary moves it off.

theorem Complexity.PolyExists.trans_of_parked_pred {k : ℕ} {P : TM.TapePred (enumTapes k)} {inp : Tape} {work : Fin (enumTapes k) → Tape} {out : Tape} (hi : TM.Parked inp) (hw : ∀ (i : Fin (enumTapes k)), TM.Parked (work i)) (ho : TM.Parked out) (h : P inp work out) : P (TM.transitionInput inp) (fun (i : Fin (enumTapes k)) => TM.transitionTape (work i)) (TM.transitionTape out)

A predicate about parked tapes survives a phase boundary, since the boundary does not move them.

def Complexity.PolyExists.bodyTime (k : ℕ) (x : List Bool) (T : ℕ → ℕ) (H Hb B v a r : ℕ) : ℕ

The pass's running time: its ten stages and the nine boundaries between them.

Equations

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

theorem Complexity.PolyExists.bodyTM_hoareTime {k : ℕ} (M : TM k) {L : Language} {T S : ℕ → ℕ} (hdec : M.DecidesInTime L T) (hdecS : M.DecidesInSpace L S) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) (hISI : I.StartInvariant) (hIhead : I.head = 1) (hIz : I.cells 0 = Γ.start) (B Hb : ℕ) (hB : 1 + TM.pairInputWorkTime x (dropTop (v + 1)) ≤ B) (hB1 : 1 ≤ B) (hHb1 : 1 ≤ Hb) (hHS : (pair x (dropTop (v + 1))).length + S (pair x (dropTop (v + 1))).length + 2 ≤ Hb) (hHbH : Hb + 1 ≤ H) (hpairH : (pair x (dropTop (v + 1))).length + 1 ≤ H) (b : Bool) (hb : b = true ↔ pair x (dropTop (v + 1)) ∈ L) : (bodyTM M).HoareTime (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ work = enumBank k x N H v a r ∧ ∃ (s : Γw), s ≠ Γw.one ∧ out = NTM.outSlot s) (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ work = enumBank k x N H (v + 1) (a + if b = true then 1 else 0) (r + if b = true then 0 else 1) ∧ out = TM.blankTape) (bodyTime k x T H Hb B v a r)

One pass of the enumerator, contracted. From the loop's state at count v the pass tests the witness that count denotes, advances the counter and the witness, bumps the tally the verdict names, and leaves the loop's state at count v + 1.