The enumerator's prologue

⚠️ Unreviewed by Bolton

Before the loop can start, three tapes have to be filled: a copy of the real input, for the pair emitter to read; the horizon the counter is compared against; and the unary register that drives each pass's wipe.

TM.copyInputToWorkTM's own contract says nothing about the tapes it does not write, and it is used here beside a dozen that must survive. It does not disturb them: every tape but its target is written blank and moved by TM.idleDir, so a blank tape comes back blank — which is what the frame below records, by induction along the run.

Main results

• PolyExists.blankTape_idle — an idled blank tape is unchanged
• PolyExists.copyInputToWorkTM_blank_frame — the copier leaves every other blank tape blank
• PolyExists.copyX_hoareTime — the copy stage's contract, frame included

theorem Complexity.PolyExists.blankTape_idle : TM.blankTape.writeAndMove Γw.blank.toΓ (TM.idleDir TM.blankTape.read) = TM.blankTape

An idled blank tape is unchanged. Writing a blank under the head of a blank tape changes nothing, and TM.idleDir does not move a head that is off the marker.

theorem Complexity.PolyExists.copyStep_blank {n : ℕ} (idx : Fin n) {c c' : Cfg n (TM.copyInputToWorkTM idx).Q} (hstep : (TM.copyInputToWorkTM idx).step c = some c') (i : Fin n) (hi : i ≠ idx) (h : c.work i = TM.blankTape) : c'.work i = TM.blankTape

One step of the copier leaves a blank tape blank.

theorem Complexity.PolyExists.copyInputToWorkTM_blank_frame {n : ℕ} (idx : Fin n) {t : ℕ} {c c' : Cfg n (TM.copyInputToWorkTM idx).Q} : (TM.copyInputToWorkTM idx).reachesIn t c c' → ∀ (i : Fin n), i ≠ idx → c.work i = TM.blankTape → c'.work i = TM.blankTape

The copier leaves every other blank tape blank, which is the frame its own contract does not record.

theorem Complexity.PolyExists.copyStep_blank_out {n : ℕ} (idx : Fin n) {c c' : Cfg n (TM.copyInputToWorkTM idx).Q} (hstep : (TM.copyInputToWorkTM idx).step c = some c') (h : c.output = TM.blankTape) : c'.output = TM.blankTape

One step of the copier leaves the real output blank, for the same reason.

theorem Complexity.PolyExists.copyInputToWorkTM_blank_frame_out {n : ℕ} (idx : Fin n) {t : ℕ} {c c' : Cfg n (TM.copyInputToWorkTM idx).Q} : (TM.copyInputToWorkTM idx).reachesIn t c c' → c.output = TM.blankTape → c'.output = TM.blankTape

theorem Complexity.PolyExists.blankTape_hasBinaryPrefix_nil : TM.blankTape.HasBinaryPrefix []

The blank tape carries the empty binary prefix.

theorem Complexity.PolyExists.copyX_hoareTime (k : ℕ) (x : List Bool) : (TM.copyInputToWorkTM (xIdx k)).HoareTime (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = strTape x ∧ (work = fun (x : Fin (enumTapes k)) => TM.blankTape) ∧ out = TM.blankTape) (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp.cells = (strTape x).cells ∧ inp.head = x.length + 1 ∧ (∀ (i : Fin (enumTapes k)), i ≠ xIdx k → work i = TM.blankTape) ∧ (work (xIdx k)).HasBinaryPrefix x ∧ (work (xIdx k)).cells 0 = Γ.start ∧ out = TM.blankTape) (x.length + 1)

The input copy, contracted with its frame.

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

The register subroutines state their contracts with an output accumulator; with nothing emitted that is just the blank tape.

theorem Complexity.PolyExists.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 emit contract with nothing emitted.

theorem Complexity.PolyExists.bits_two_pow_sub_one' (T : ℕ) : (2 ^ T - 1).bits = List.replicate T true

A unary register of T ones is the binary numeral 2 ^ T - 1. The two encodings agree cell for cell, which is what lets the prologue produce the horizon without a doubling loop.

theorem Complexity.PolyExists.regTape_eq_natTape' (T : ℕ) : TM.regTape T = natTape (2 ^ T - 1)

theorem Complexity.PolyExists.regTape_zero' : TM.regTape 0 = TM.blankTape

A unary register holding zero is the blank tape.

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

And so is a counter tape holding zero.

def Complexity.PolyExists.prologueTM (k : ℕ) (p q : Polynomial ℕ) : TM (enumTapes k)

The enumerator's prologue. Measure the input, evaluate the horizon's exponent and the wipe height on unary registers, bump the exponent — a register of m + 1 ones is the binary numeral 2 ^ (m + 1) - 1 — and clear the scratch.

Equations

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

def Complexity.PolyExists.copiedBank (k : ℕ) (x : List Bool) : Fin (enumTapes k) → Tape

The bank the copy stage leaves: the input on its tape, everything else blank.

Equations

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

theorem Complexity.PolyExists.copiedBank_parked (k : ℕ) (x : List Bool) (j : Fin (enumTapes k)) : TM.Parked (copiedBank k x j)

theorem Complexity.PolyExists.copiedBank_of_ne (k : ℕ) (x : List Bool) (j : Fin (enumTapes k)) (h : j ≠ xIdx k) : copiedBank k x j = TM.blankTape

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

The cap the Horner evaluation stays under.

Equations

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

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

def Complexity.PolyExists.prologueBnd (p q : Polynomial ℕ) (lx : ℕ) : ℕ

The prologue's per-stage budget.

Equations

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

def Complexity.PolyExists.prologueTime (p q : Polynomial ℕ) (lx : ℕ) : ℕ

The prologue's running time.

Equations

• Complexity.PolyExists.prologueTime p q lx = 7 * (Complexity.PolyExists.prologueBnd p q lx + 1) + 1

theorem Complexity.PolyExists.prologueTM_hoareTime (k : ℕ) (p q : Polynomial ℕ) (x : List Bool) : (prologueTM k p q).HoareTime (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = strTape x ∧ work = copiedBank k x ∧ out = TM.blankTape) (fun (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => inp = strTape x ∧ work = enumBank k x (2 ^ (Polynomial.eval x.length p + 1) - 1) (Polynomial.eval x.length q) 0 0 0 ∧ out = TM.blankTape) (prologueTime p q x.length)

The prologue's contract. From the bank the copy stage leaves it lands on the loop's starting bank: the horizon on PolyExists.nIdx, the wipe height on PolyExists.regIdx, the input copy where the emitter reads it, and everything else blank.