The enumerator's epilogue

⚠️ Unreviewed by Bolton

The loop leaves the accepting tally on PolyExists.aIdx, and the answer is whether it is positive. A machine has no >; it has subtraction and a test against zero. So the epilogue makes a one on the permanently blank tape, subtracts the tally from it — the difference is zero exactly when the tally is positive — and tests that difference against zero, publishing the answer.

The two tapes it borrows for the test are the emitter's target and the matrix machine's input: both are blank once the loop's last wipe has run, and nothing reads them again.

Main results

• PolyExists.epilogueTM — the epilogue, and PolyExists.epilogueTime its running time
• PolyExists.epilogueTM_hoareTime — its contract: the slot ends holding decide (0 < a)

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

The epilogue's arithmetic: make a one, subtract the accepting tally from it.

Equations

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

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

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

Equations

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

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

The enumerator's epilogue.

Equations

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

def Complexity.PolyExists.epilogueBank (k : ℕ) (x : List Bool) (N H A R : ℕ) : Fin (enumTapes 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.PolyExists.epilogueBank_parked (k : ℕ) (x : List Bool) (N H A R : ℕ) (j : Fin (enumTapes k)) : TM.Parked (epilogueBank k x N H A R j)

theorem Complexity.PolyExists.epilogueBank_cells_zero (k : ℕ) (x : List Bool) (N H A R : ℕ) (j : Fin (enumTapes k)) : (epilogueBank k x N H A R j).cells 0 = Γ.start

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

The state the epilogue's test leaves: every tape parked, and the answer bit sitting at cell one of the register the test wrote to.

Equations

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

theorem Complexity.PolyExists.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 (enumTapes k) → Tape) (out : Tape) => out = NTM.outSlot (TM.readBackWrite (Γ.ofBool b))) (1 * (B + 3) + 1 + 1 + 1)

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

theorem Complexity.PolyExists.natTape_zero_eq : natTape 0 = TM.blankTape

A counter tape holding zero is the blank tape.

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

Strict order as a truncated subtraction, which is what a machine can test.

theorem Complexity.PolyExists.epilogueBank_res (k : ℕ) (x : List Bool) (N H A R : ℕ) : epilogueBank k x N H A R (resIdx k) = natTape (1 - A)

theorem Complexity.PolyExists.epilogueBank_y1 (k : ℕ) (x : List Bool) (N H A R : ℕ) : epilogueBank k x N H A R (y1Idx k) = TM.blankTape

theorem Complexity.PolyExists.epilogueBank_y (k : ℕ) (x : List Bool) (N H A R : ℕ) : epilogueBank k x N H A R (yIdx k) = TM.blankTape

theorem Complexity.PolyExists.epilogueEq_hoareTime (k : ℕ) (x : List Bool) (N H A R : ℕ) (I : Tape) (hI : TM.Parked I) (hIsi : I.StartInvariant) : (TM.binaryEqTM (resIdx k) (y1Idx k) (yIdx k)).HoareTime (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ work = epilogueBank k x N H A R ∧ out = NTM.outSlot Γw.one) (afterEq k (decide (0 < A)) I 2) (TM.binaryEqTime (1 - A).bits (Nat.bits 0))

The epilogue's test. The difference is zero exactly when the accepting tally is positive, so comparing it with zero decides the bounded existential.

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

theorem Complexity.PolyExists.epiloguePreTM_hoareTime (k : ℕ) (x : List Bool) (N H A R : ℕ) (I : Tape) (hI : TM.Parked I) : (epiloguePreTM k).HoareTime (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ work = enumBank k x N H N A R ∧ out = NTM.outSlot Γw.one) (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ work = epilogueBank k x N H A R ∧ out = NTM.outSlot Γw.one) (2 * (max (TM.binarySuccTime 0) (TM.binaryRippleSubTime 1 A) + 1) + 1)

The epilogue's arithmetic. Make a one on the blank tape, then subtract the accepting tally from it; the difference is zero exactly when that tally is positive.

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

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

def Complexity.PolyExists.epilogueTime (A : ℕ) : ℕ

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

Equations

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

theorem Complexity.PolyExists.epilogueTM_hoareTime (k : ℕ) (x : List Bool) (N H A R : ℕ) (I : Tape) (hI : TM.Parked I) (hIsi : I.StartInvariant) : (epilogueTM k).HoareTime (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = I ∧ work = enumBank k x N H N A R ∧ out = NTM.outSlot Γw.one) (fun (_inp : Tape) (_work : Fin (enumTapes k) → Tape) (out : Tape) => out = NTM.outSlot (TM.readBackWrite (Γ.ofBool (decide (0 < A))))) (epilogueTime A)

The epilogue's contract. From the bank the loop leaves, the machine writes 1 into the verdict slot exactly when some witness was accepted.