Safety of witness-independent phases

Appending the distinguished witness tape to an ordinary phase preserves every safety property of its visible tapes. In particular, decision-space bounds keep charging output while ignoring the external stream's unbounded cursor.

theorem Complexity.TM.liftLast_reaches_project {k : ℕ} (D : TM k) {c c' : Cfg (k + 1) D.Q} (h : D.liftLast.reaches c c') : D.reaches (NTM.dropChoice c) (NTM.dropChoice c')

Every reachable configuration of a lifted phase projects to one of the original phase, independently of the contents or position of the added tape.

theorem Complexity.TM.liftLast_hoareSafety {k : ℕ} (D : TM k) {pre safe : TapePred k} (h : D.HoareSafety pre safe) : D.liftLast.HoareSafety (fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => pre inp (fun (i : Fin k) => work i.castSucc) out) fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => safe inp (fun (i : Fin k) => work i.castSucc) out

Lift ordinary phase safety without charging the added external tape.

theorem Complexity.TM.HoareTime.projectedSafety {k : ℕ} {M : TM (k + 1)} {pre post : TapePred (k + 1)} {time inputLength initialSpace : ℕ} (h : M.HoareTime pre post time) (hinit : ∀ (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape), pre inp work out → { state := (), input := inp, work := fun (i : Fin k) => work i.castSucc, output := out }.WithinDecisionSpace inputLength initialSpace) : M.HoareSafety pre fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => { state := (), input := inp, work := fun (i : Fin k) => work i.castSucc, output := out }.WithinDecisionSpace inputLength (initialSpace + time)

A terminating phase has a conservative projected decision-space bound. Only the ordinary tapes contribute; the final external tape may travel freely.