Building the pair the matrix machine reads

⚠️ Unreviewed by Bolton

TM.pairInputWorkTM emits pair first second, reading the first component off a work tape and the second off its input tape. The enumerator needs pair x w with the witness second, so the witness has to be what the emitter reads as an input — which TM.retargetInput arranges, since it runs a machine with its input supplied on the last work tape. TM.retargetOutput then sends the emitted pair to a work tape rather than the real output, which a loop body cannot write to.

The emitter's own contract says only that the pair appears; it says nothing about the tapes it read. PolyExists.pairFrame_hoareTime restates its exact-execution theorem as the contract that does: both sources come back with their cells intact and their heads left past the content, which the rewind that follows the stage puts back.

Main results

• PolyExists.pairFrame_hoareTime — the emitter's contract, framed
• PolyExists.emitCore, PolyExists.emitTM — the emitter as a stage of the enumerator
• PolyExists.emitCore_hoareTime — the stage's contract, on the three tapes it uses
• PolyExists.emitTM, PolyExists.emitTM_hoareTime — the same, placed in the layout

theorem Complexity.PolyExists.pairFrame_hoareTime {n : ℕ} (firstIdx : Fin n) (first second : List Bool) (inp₀ : Tape) (work₀ : Fin n → Tape) (out₀ : Tape) (hinput : inp₀ = (Tape.init (List.map Γ.ofBool second)).move Dir3.right) (hsourceHead : (work₀ firstIdx).head = 1) (hsourceOutput : (work₀ firstIdx).HasOutput first) (hwork : ∀ (i : Fin n), (work₀ i).StartInvariant ∧ 1 ≤ (work₀ i).head) (houtput : out₀ = (Tape.init []).move Dir3.right) : (TM.pairInputWorkTM firstIdx).HoareTime (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp = inp₀ ∧ work = work₀ ∧ out = out₀) (fun (inp : Tape) (work : Fin n → Tape) (out : Tape) => inp.cells = inp₀.cells ∧ (work firstIdx).cells = (work₀ firstIdx).cells ∧ (work firstIdx).HasOutput first ∧ (∀ (i : Fin n), i ≠ firstIdx → work i = work₀ i) ∧ out.HasBinaryPrefix (pair first second)) (TM.pairInputWorkTime first second)

The pair emitter, framed. Beyond the pair, this records what the sources look like when the stage ends: their cells are untouched and the first component is still readable, its head having been left past the content.

def Complexity.PolyExists.emitCore : TM 3

The emitter as a three-tape machine: the input copy, the witness it reads as an input, and the tape the pair is written to.

Equations

• Complexity.PolyExists.emitCore = (Complexity.TM.pairInputWorkTM 0).retargetInput.retargetOutput

theorem Complexity.PolyExists.emitCore_hoareTime (x w : List Bool) (X : Tape) (hXhead : X.head = 1) (hXout : X.HasOutput x) (hXSI : X.StartInvariant) : emitCore.HoareTime (fun (_inp : Tape) (work : Fin 3 → Tape) (out : Tape) => work 0 = X ∧ work 1 = (Tape.init (List.map Γ.ofBool w)).move Dir3.right ∧ work 2 = TM.parkedBlank ∧ out = TM.parkedBlank) (fun (_inp : Tape) (work : Fin 3 → Tape) (out : Tape) => (work 0).cells = X.cells ∧ (work 0).HasOutput x ∧ (work 1).cells = ((Tape.init (List.map Γ.ofBool w)).move Dir3.right).cells ∧ (work 2).HasBinaryPrefix (pair x w) ∧ out = TM.parkedBlank) (TM.pairInputWorkTime x w)

The emitter stage's contract. Started with the input copy rewound, the witness in virtual-input shape, and the target tape blank, it leaves the pair on the target tape and both sources with their cells intact.

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

The emitter placed in the enumerator's layout: it uses the first three tapes, which is where the input copy, the witness, and the pair sit.

Equations

• Complexity.PolyExists.emitTM k = Complexity.TM.placeWorkTM 0 (k + 9) Complexity.PolyExists.emitCore

theorem Complexity.PolyExists.placeWorkIdx_zero (k : ℕ) : TM.placeWorkIdx 0 (k + 9) 0 = xIdx k

theorem Complexity.PolyExists.placeWorkIdx_one (k : ℕ) : TM.placeWorkIdx 0 (k + 9) 1 = wIdx k

theorem Complexity.PolyExists.placeWorkIdx_two (k : ℕ) : TM.placeWorkIdx 0 (k + 9) 2 = y1Idx k

theorem Complexity.PolyExists.not_inMiddle_iff (k : ℕ) (i : Fin (enumTapes k)) : ¬TM.placeWorkInMiddle 0 3 i ↔ 3 ≤ ↑i

A tape of the layout is outside the emitter's block exactly when its index is at least three.

theorem Complexity.PolyExists.emitTM_hoareTime (k : ℕ) (x w : List Bool) (X : Tape) (hXhead : X.head = 1) (hXout : X.HasOutput x) (hXSI : X.StartInvariant) (extras : Fin (enumTapes k) → Tape) (hinv : ∀ (i : Fin (0 + 3 + (k + 9))), ¬TM.placeWorkInMiddle 0 3 i → (extras i).StartInvariant) (hhead : ∀ (i : Fin (0 + 3 + (k + 9))), ¬TM.placeWorkInMiddle 0 3 i → 1 ≤ (extras i).head) : (emitTM k).HoareTime (fun (_inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => (∀ (i : Fin (0 + 3 + (k + 9))), ¬TM.placeWorkInMiddle 0 3 i → work i = extras i) ∧ work (xIdx k) = X ∧ work (wIdx k) = (Tape.init (List.map Γ.ofBool w)).move Dir3.right ∧ work (y1Idx k) = TM.parkedBlank ∧ out = TM.parkedBlank) (fun (_inp : Tape) (work : Fin (enumTapes k) → Tape) (out : Tape) => (∀ (i : Fin (0 + 3 + (k + 9))), ¬TM.placeWorkInMiddle 0 3 i → work i = extras i) ∧ (work (xIdx k)).cells = X.cells ∧ (work (xIdx k)).HasOutput x ∧ (work (wIdx k)).cells = ((Tape.init (List.map Γ.ofBool w)).move Dir3.right).cells ∧ (work (y1Idx k)).HasBinaryPrefix (pair x w) ∧ out = TM.parkedBlank) (TM.pairInputWorkTime x w)

The placed emitter's contract. The three tapes it uses come back as PolyExists.emitCore_hoareTime describes them; every other tape of the layout is untouched.