Hoare contracts through work-tape lifting

A lifted machine keeps its source's time bound and preserves arbitrary non-marker extra tapes exactly. These frame rules need no universal-machine or clock infrastructure.

theorem Complexity.TM.liftTM_hoareTime_frame {n m : ℕ} (tm : TM n) {pre post : TapePred n} {b : ℕ} (extras : Fin m → Tape) (hex : ∀ (j : Fin m), 1 ≤ (extras j).head ∧ (extras j).read ≠ Γ.start) (h : tm.HoareTime pre post b) : (tm.liftTM m).HoareTime (fun (inp : Tape) (work : Fin (n + m) → Tape) (out : Tape) => pre inp (fun (i : Fin n) => work (Fin.castAdd m i)) out ∧ ∀ (j : Fin m), work (Fin.natAdd n j) = extras j) (fun (inp : Tape) (work : Fin (n + m) → Tape) (out : Tape) => post inp (fun (i : Fin n) => work (Fin.castAdd m i)) out ∧ ∀ (j : Fin m), work (Fin.natAdd n j) = extras j) b

Frame rule for liftTM Hoare specs (ghost-pinned extras). If tm : TM n satisfies {pre} tm {post} [≤ b], then tm.liftTM m satisfies the same triple on its first n work tapes while the m extra tapes — holding arbitrary parked content extras (head ≥ 1, reading a non-▷ symbol) — are preserved exactly, with the same time bound. This is what lets lifted 6-tape UTM phases run while tape 6 holds the clock.

theorem Complexity.TM.liftTM_hoareTime {n m : ℕ} (tm : TM n) {pre post : TapePred n} {b : ℕ} (h : tm.HoareTime pre post b) : (tm.liftTM m).HoareTime (fun (inp : Tape) (work : Fin (n + m) → Tape) (out : Tape) => pre inp (fun (i : Fin n) => work (Fin.castAdd m i)) out ∧ ∀ (j : Fin m), work (Fin.natAdd n j) = (Tape.init []).move Dir3.right) (fun (inp : Tape) (work : Fin (n + m) → Tape) (out : Tape) => post inp (fun (i : Fin n) => work (Fin.castAdd m i)) out ∧ ∀ (j : Fin m), work (Fin.natAdd n j) = (Tape.init []).move Dir3.right) b

liftTM preserves Hoare specs (blank extras). Special case of liftTM_hoareTime_frame: the extra tapes start and end as the canonical parked blank tape (Tape.init []).move Dir3.right.