Framed pair-builder phase

The output and inactive work tapes are ghost snapshots. Their heads must be positive for exact preservation; their start invariants supply the later seam. Space is charged on every ordinary work tape and the output, and includes only this pair-building phase's runtime.

def Complexity.TM.PairBuildFramePre {k : ℕ} (yIdx pIdx : Fin k) (x y : List Bool) (extras : Fin k → Tape) (out₀ : Tape) : TapePred k

Canonical active tapes together with an arbitrary inactive frame.

Equations

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

def Complexity.TM.PairBuildFramePost {k : ℕ} (yIdx pIdx : Fin k) (x y : List Bool) (extras : Fin k → Tape) (out₀ : Tape) : TapePred k

Pair encoding, exact frame, and marker invariants needed at the next seam.

Equations

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

theorem Complexity.TM.pairBuildTM_hoareTime_framed {k : ℕ} (yIdx pIdx : Fin k) (hne : yIdx ≠ pIdx) (x y : List Bool) (extras : Fin k → Tape) (out₀ : Tape) (hout : out₀.StartInvariant) (houtHead : 1 ≤ out₀.head) (hextras : ∀ (i : Fin k), i ≠ yIdx → i ≠ pIdx → (extras i).StartInvariant) (hextraHeads : ∀ (i : Fin k), i ≠ yIdx → i ≠ pIdx → 1 ≤ (extras i).head) : (pairBuildTM yIdx pIdx).HoareTime (PairBuildFramePre yIdx pIdx x y extras out₀) (PairBuildFramePost yIdx pIdx x y extras out₀) (pairBuildTime x.length y.length)

Ordinary deterministic pair building preserves a parked, well-formed frame.

theorem Complexity.TM.pairBuildFramePost_seam_heads {k : ℕ} {yIdx pIdx : Fin k} {x y : List Bool} {extras : Fin k → Tape} {out₀ inp out : Tape} {work : Fin k → Tape} (h : PairBuildFramePost yIdx pIdx x y extras out₀ inp work out) : 1 ≤ (transitionInput inp).head ∧ (∀ (i : Fin k), 1 ≤ (transitionTape (work i)).head) ∧ 1 ≤ (transitionTape out).head

Every head is positive after the next sequential handoff. No positivity claim about the active tapes before this handoff is needed.

theorem Complexity.TM.pairBuildTM_hoareSafety_framed {k : ℕ} (yIdx pIdx : Fin k) (hne : yIdx ≠ pIdx) (x y : List Bool) (extras : Fin k → Tape) (out₀ : Tape) (initialSpace : ℕ) (hspace : 1 ≤ initialSpace) (hextraHeads : ∀ (i : Fin k), i ≠ yIdx → i ≠ pIdx → (extras i).head ≤ initialSpace) (houtHead : out₀.head ≤ initialSpace + 1) : (pairBuildTM yIdx pIdx).HoareSafety (PairBuildFramePre yIdx pIdx x y extras out₀) fun (inp : Tape) (work : Fin k → Tape) (out : Tape) => { state := (), input := inp, work := work, output := out }.WithinDecisionSpace x.length (initialSpace + pairBuildTime x.length y.length)

Every reachable prefix of pair building stays within the entry space plus 4 * |x| + 2 * |y| + 10; output travel is charged. The frame's initial heads are bounded explicitly, and no downstream verifier runtime occurs in this bound.