One pass of the enumerator, in space

⚠️ Unreviewed by Bolton

Nine of the pass's ten stages are short, and their windows come straight from their running times. The tenth — the matrix machine — is not short at all: it may run for exponentially many steps, and its window has to come from its space bound instead (PolyExists.matrixTM_keepsWindowOn). Composing the ten is what TM.seqTM_keepsWindowOn is for.

Main results

• PolyExists.afterCopy_head_le, PolyExists.mid*_heads — how far each intermediate state's heads can be

theorem Complexity.PolyExists.afterCopy_head_le (k : ℕ) (x : List Bool) (N H v a r G : ℕ) (hG : (pair x (dropTop (v + 1))).length + 1 ≤ G) (i : Fin (enumTapes k)) : (afterCopy k x N H v a r i).head ≤ G

Every tape the copy stage leaves has its head inside the pair's width.

theorem Complexity.PolyExists.enumBank_head_le (k : ℕ) (x : List Bool) (N H v a r G : ℕ) (hG : 1 ≤ G) (i : Fin (enumTapes k)) : (enumBank k x N H v a r i).head ≤ G

Every tape of the loop's own state has its head at cell one.

theorem Complexity.PolyExists.midMatrix_heads (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (Hb G : ℕ) (b : Bool) (hHb : Hb ≤ G) (hpair : (pair x (dropTop (v + 1))).length + 1 ≤ G) (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) (h : midMatrix k x N H v a r I Hb b inp work out) (i : Fin (enumTapes k)) : (work i).head ≤ G

theorem Complexity.PolyExists.midParked_heads (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (Hb G : ℕ) (b : Bool) (hHb : Hb + 1 ≤ G) (hpair : (pair x (dropTop (v + 1))).length + 1 ≤ G) (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) (h : midParked k x N H v a r I Hb b inp work out) (i : Fin (enumTapes k)) : (work i).head ≤ G

theorem Complexity.PolyExists.midPublish_heads (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (Hb G : ℕ) (b : Bool) (hHb : Hb + 1 ≤ G) (hpair : (pair x (dropTop (v + 1))).length + 1 ≤ G) (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) (h : midPublish k x N H v a r I Hb b inp work out) (i : Fin (enumTapes k)) : (work i).head ≤ G

theorem Complexity.PolyExists.midBump_heads (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (Hb G : ℕ) (b : Bool) (hHb : Hb + 1 ≤ G) (hpair : (pair x (dropTop (v + 1))).length + 1 ≤ G) (hG1 : 1 ≤ G) (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) (h : midBump k x N H v a r I Hb b inp work out) (i : Fin (enumTapes k)) : (work i).head ≤ G

theorem Complexity.PolyExists.midBumped_heads (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (Hb G : ℕ) (b : Bool) (hHb : Hb + 1 ≤ G) (hpair : (pair x (dropTop (v + 1))).length + 1 ≤ G) (hG1 : 1 ≤ G) (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) (h : midBumped k x N H v a r I Hb b inp work out) (i : Fin (enumTapes k)) : (work i).head ≤ G

theorem Complexity.PolyExists.wipe_keepsWindowOn (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) (hIsi : I.StartInvariant) (hIhead : I.head = 1) (Hb G : ℕ) (b : Bool) (hHbH : Hb + 1 ≤ H) (hpairH : (pair x (dropTop (v + 1))).length + 1 ≤ H) (hG1 : 1 ≤ G) (hGHb : Hb + 1 ≤ G) (hGpair : (pair x (dropTop (v + 1))).length + 1 ≤ G) : (TM.wipeRewindTM (scratchTargets k) (regIdx k)).KeepsWindowOn (fun (c : Cfg (enumTapes k) (TM.wipeRewindTM (scratchTargets k) (regIdx k)).Q) => c.state = (TM.wipeRewindTM (scratchTargets k) (regIdx k)).qstart ∧ midBumped k x N H v a r I Hb b c.input c.work c.output) x.length (G + ((scratchTargets k).length * (H + 4) + H * 4 + 8 + 1 + ((scratchTargets k).length * (H + 4) + 1)))

The wipe's window.

theorem Complexity.PolyExists.witnessBump_keepsWindowOn (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) (hIhead : I.head = 1) (Hb G : ℕ) (b : Bool) (hG1 : 1 ≤ G) (hGHb : Hb + 1 ≤ G) (hGpair : (pair x (dropTop (v + 1))).length + 1 ≤ G) : (TM.binaryBumpTM (wIdx k)).KeepsWindowOn (fun (c : Cfg (enumTapes k) (TM.binaryBumpTM (wIdx k)).Q) => c.state = (TM.binaryBumpTM (wIdx k)).qstart ∧ midBump k x N H v a r I Hb b c.input c.work c.output) x.length (G + TM.binaryBumpTime (dropTop (v + 1)))

The witness bump's window.

theorem Complexity.PolyExists.tallyBump_keepsWindowOn (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) (hIz : I.cells 0 = Γ.start) (hIhead : I.head = 1) (Hb G : ℕ) (b : Bool) (hG1 : 1 ≤ G) (hGHb : Hb + 1 ≤ G) (hGpair : (pair x (dropTop (v + 1))).length + 1 ≤ G) : (TM.tallyBumpTM (cIdx k) (aIdx k) (rIdx k) (zIdx k)).KeepsWindowOn (fun (c : Cfg (enumTapes k) (TM.tallyBumpTM (cIdx k) (aIdx k) (rIdx k) (zIdx k)).Q) => c.state = (TM.tallyBumpTM (cIdx k) (aIdx k) (rIdx k) (zIdx k)).qstart ∧ midPublish k x N H v a r I Hb b c.input c.work c.output) x.length (G + (3 * (max (1 + 1 + max (TM.binarySuccTime a) (TM.binarySuccTime r) + 5) (TM.binarySuccTime v) + 1) + 1))

The tally bump's window.

theorem Complexity.PolyExists.publishVerdict_keepsWindowOn (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) (hIhead : I.head = 1) (Hb G : ℕ) (b : Bool) (hG1 : 1 ≤ G) (hGHb : Hb + 1 ≤ G) (hGpair : (pair x (dropTop (v + 1))).length + 1 ≤ G) : (TM.writeOutputBitTM (vIdx k)).KeepsWindowOn (fun (c : Cfg (enumTapes k) (TM.writeOutputBitTM (vIdx k)).Q) => c.state = (TM.writeOutputBitTM (vIdx k)).qstart ∧ midParked k x N H v a r I Hb b c.input c.work c.output) x.length (G + 1)

The publication's window.

theorem Complexity.PolyExists.parkVerdict_keepsWindowOn (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hIsi : I.StartInvariant) (hIhead : I.head = 1) (Hb G : ℕ) (hHb1 : 1 ≤ Hb) (b : Bool) (hG1 : 1 ≤ G) (hGHb : Hb ≤ G) (hGpair : (pair x (dropTop (v + 1))).length + 1 ≤ G) : (TM.parkRewindTM [vIdx k]).KeepsWindowOn (fun (c : Cfg (enumTapes k) (TM.parkRewindTM [vIdx k]).Q) => c.state = (TM.parkRewindTM [vIdx k]).qstart ∧ midMatrix k x N H v a r I Hb b c.input c.work c.output) x.length (G + (1 + 1 + (2 * (max (Hb + 2) (1 * (Hb + 3) + 1) + 1) + 1)))

The verdict rewind's window.

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

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

theorem Complexity.PolyExists.blankSlot_keepsWindowOn (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) (hIhead : I.head = 1) (G : ℕ) (hG1 : 1 ≤ G) : (TM.writeOutputBitTM (zIdx k)).KeepsWindowOn (fun (c : Cfg (enumTapes k) (TM.writeOutputBitTM (zIdx k)).Q) => c.state = (TM.writeOutputBitTM (zIdx k)).qstart ∧ c.input = I ∧ c.work = enumBank k x N H v a r ∧ ∃ (s : Γw), s ≠ Γw.one ∧ c.output = NTM.outSlot s) x.length (G + 1)

The blanking stage's window.

theorem Complexity.PolyExists.emit_keepsWindowOn (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) (hIsi : I.StartInvariant) (hIhead : I.head = 1) (B G : ℕ) (hB : 1 + TM.pairInputWorkTime x (dropTop (v + 1)) ≤ B) (hG1 : 1 ≤ G) : (emitTM k).KeepsWindowOn (fun (c : Cfg (enumTapes k) (emitTM k).Q) => c.state = (emitTM k).qstart ∧ c.input = I ∧ c.work = enumBank k x N H v a r ∧ c.output = TM.blankTape) x.length (G + TM.pairInputWorkTime x (dropTop (v + 1)))

The emitter's window.

theorem Complexity.PolyExists.parkPair_keepsWindowOn (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hIsi : I.StartInvariant) (hIhead : I.head = 1) (B G : ℕ) (hB1 : 1 ≤ B) (hGB : B ≤ G) : (TM.parkRewindTM [xIdx k, wIdx k, y1Idx k]).KeepsWindowOn (fun (c : Cfg (enumTapes k) (TM.parkRewindTM [xIdx k, wIdx k, y1Idx k]).Q) => c.state = (TM.parkRewindTM [xIdx k, wIdx k, y1Idx k]).qstart ∧ midEmit k x N H v a r I B c.input c.work c.output) x.length (G + (1 + 1 + (2 * (max (B + 2) (3 * (B + 3) + 1) + 1) + 1)))

The rewinding stage's window.

theorem Complexity.PolyExists.copyPair_keepsWindowOn (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hI : TM.Parked I) (hIhead : I.head = 1) (G : ℕ) (hG1 : 1 ≤ G) : (copyPairTM k).KeepsWindowOn (fun (c : Cfg (enumTapes k) (copyPairTM k).Q) => c.state = (copyPairTM k).qstart ∧ c.input = I ∧ c.work = afterPair k x N H v a r ∧ c.output = TM.blankTape) x.length (G + (2 * (pair x (dropTop (v + 1))).length + 5))

The copy stage's window.

theorem Complexity.PolyExists.matrix_keepsWindowOn {k : ℕ} (M : TM k) {L' : Language} {S : ℕ → ℕ} (hdecS : M.DecidesInSpace L' S) (hne : M.qstart ≠ M.qhalt) (x : List Bool) (N H v a r : ℕ) (I : Tape) (hIsi : I.StartInvariant) (hIhead : I.head = 1) (W : ℕ) (hW : (pair x (dropTop (v + 1))).length + S (pair x (dropTop (v + 1))).length + 2 ≤ W) (hWpair : (pair x (dropTop (v + 1))).length + 1 ≤ W) : (matrixTM M).KeepsWindowOn (fun (c : Cfg (enumTapes k) (matrixTM M).Q) => c.state = (matrixTM M).qstart ∧ c.input = I ∧ c.work = afterCopy k x N H v a r ∧ c.output = TM.blankTape) x.length W

The evaluating stage's window, at the tapes the copy stage leaves.

theorem Complexity.PolyExists.midMatrix_si (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (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) (i : Fin (enumTapes k)) : (work i).StartInvariant

theorem Complexity.PolyExists.midParked_si (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (Hb : ℕ) (b : Bool) (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) (h : midParked k x N H v a r I Hb b inp work out) (i : Fin (enumTapes k)) : (work i).StartInvariant

theorem Complexity.PolyExists.midPublish_si (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (Hb : ℕ) (b : Bool) (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) (h : midPublish k x N H v a r I Hb b inp work out) (i : Fin (enumTapes k)) : (work i).StartInvariant

theorem Complexity.PolyExists.midBump_si (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (Hb : ℕ) (b : Bool) (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) (h : midBump k x N H v a r I Hb b inp work out) (i : Fin (enumTapes k)) : (work i).StartInvariant

theorem Complexity.PolyExists.midBumped_si (k : ℕ) (x : List Bool) (N H v a r : ℕ) (I : Tape) (Hb : ℕ) (b : Bool) (inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) (h : midBumped k x N H v a r I Hb b inp work out) (i : Fin (enumTapes k)) : (work i).StartInvariant

theorem Complexity.PolyExists.hoare_post_of {m : ℕ} {tm : TM m} {pre post : TM.TapePred m} {bnd : ℕ} (h : tm.HoareTime pre post bnd) (c : Cfg m tm.Q) (hst : c.state = tm.qstart) (hpre : pre c.input c.work c.output) : ∃ (e : Cfg m tm.Q), tm.reaches c e ∧ tm.halted e ∧ post e.input e.work e.output

A contract yields the halting witness the window composition asks for.

theorem Complexity.PolyExists.windowed_of_heads {k : ℕ} {Q : Type} (c : Cfg (enumTapes k) Q) (lx G W : ℕ) (hGW : G ≤ W) (hw : ∀ (i : Fin (enumTapes k)), (c.work i).head ≤ G) (hi : c.input.head ≤ 1) (ho : c.output.head ≤ 1) (h1 : 1 ≤ W) : c.WithinDecisionSpace lx W

A configuration whose heads are inside G is inside any wider window.

theorem Complexity.PolyExists.cfgStartInvariant_of {k : ℕ} {Q : Type} (c : Cfg (enumTapes k) Q) (hi : c.input.StartInvariant) (hw : ∀ (i : Fin (enumTapes k)), (c.work i).StartInvariant) (ho : c.output.StartInvariant) : TM.CfgStartInvariant c

And it satisfies the left-marker invariant if each of its tapes does.

theorem Complexity.PolyExists.bodyTM_keepsWindowOn {k : ℕ} (M : TM k) {L' : Language} {T S : ℕ → ℕ} (hdec : M.DecidesInTime L' T) (hdecS : M.DecidesInSpace L' S) (hne : M.qstart ≠ M.qhalt) (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 G W : ℕ) (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') (hG1 : 1 ≤ G) (hGB : B ≤ G) (hGHb : Hb + 1 ≤ G) (hGpair : (pair x (dropTop (v + 1))).length + 1 ≤ G) (hW1 : G + 1 ≤ W) (hW2 : G + TM.pairInputWorkTime x (dropTop (v + 1)) ≤ W) (hW3 : G + (1 + 1 + (2 * (max (B + 2) (3 * (B + 3) + 1) + 1) + 1)) ≤ W) (hW4 : G + (2 * (pair x (dropTop (v + 1))).length + 5) ≤ W) (hW6 : G + (1 + 1 + (2 * (max (Hb + 2) (1 * (Hb + 3) + 1) + 1) + 1)) ≤ W) (hW8 : G + (3 * (max (1 + 1 + max (TM.binarySuccTime a) (TM.binarySuccTime r) + 5) (TM.binarySuccTime v) + 1) + 1) ≤ W) (hW9 : G + TM.binaryBumpTime (dropTop (v + 1)) ≤ W) (hW10 : G + ((scratchTargets k).length * (H + 4) + H * 4 + 8 + 1 + ((scratchTargets k).length * (H + 4) + 1)) ≤ W) : (bodyTM M).KeepsWindowOn (fun (c : Cfg (enumTapes k) (bodyTM M).Q) => c.state = (bodyTM M).qstart ∧ c.input = I ∧ c.work = enumBank k x N H v a r ∧ ∃ (s : Γw), s ≠ Γw.one ∧ c.output = NTM.outSlot s) x.length W

One pass of the enumerator keeps a window. Nine stages are bounded by their running times; the matrix machine is bounded by its space, which is the only bound of the ten that is polynomial in the input length.