Ordinary verifier phase resource contracts

Relocated inputs are charged work storage. The original verifier's time and independent decision-space bounds transfer through a disjoint tape placement, while its real output stays the final verdict rather than another work tape.

theorem Complexity.TM.retargetInputStarted_keepsWindow_of_decidesInTimeSpace {k : ℕ} (M : TM k) {L : Language} {T S : ℕ → ℕ} (hdec : M.DecidesInTimeSpace L T S) (z : List Bool) (r : Tape) (hrsi : r.StartInvariant) {inputLength H : ℕ} (hspace : z.length + S z.length + 1 ≤ H) (hr : max r.head 1 ≤ inputLength + H + 1) (c : Cfg (k + 1) M.retargetInputStarted.Q) : M.retargetInputStarted.reaches (M.retargetInputStartedCfg z r) c → c.WithinDecisionSpace inputLength H

Relocating the virtual input charges its whole source input-head window. The actual output remains output, so no extra output-work-tape cell is charged.

theorem Complexity.TM.retargetInputStarted_hoareTimeSafety_decide {k : ℕ} (M : TM k) {L : Language} {T S : ℕ → ℕ} (hdec : M.DecidesInTimeSpace L T S) (z : List Bool) (r : Tape) (hrsi : r.StartInvariant) {inputLength H : ℕ} (hspace : z.length + S z.length + 1 ≤ H) (hr : max r.head 1 ≤ inputLength + H + 1) : M.retargetInputStarted.HoareTime (fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => inp = r ∧ work = (M.retargetInputStartedCfg z r).work ∧ out = parkedBlank) (fun (x : Tape) (x_1 : Fin (k + 1) → Tape) (out : Tape) => (z ∈ L → out.cells 1 = Γ.one) ∧ (z ∉ L → out.cells 1 = Γ.zero)) (T z.length) ∧ M.retargetInputStarted.HoareSafety (fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => inp = r ∧ work = (M.retargetInputStartedCfg z r).work ∧ out = parkedBlank) fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => { state := (), input := inp, work := work, output := out }.WithinDecisionSpace inputLength H

The virtual-input verifier phase has the original time budget and exact verdict, with honest decision-space safety at every reachable prefix, including time zero.

theorem Complexity.TM.placeWorkTM_retargetInputStarted_hoareTimeSafety_decide {k : ℕ} (M : TM k) {L : Language} {T S : ℕ → ℕ} (hdec : M.DecidesInTimeSpace L T S) (z : List Bool) (r : Tape) (hrsi : r.StartInvariant) (pre post : ℕ) (extras : Fin (pre + (k + 1) + post) → Tape) (hextraSI : ∀ (i : Fin (pre + (k + 1) + post)), ¬placeWorkInMiddle pre (k + 1) i → (extras i).StartInvariant) (hextraPos : ∀ (i : Fin (pre + (k + 1) + post)), ¬placeWorkInMiddle pre (k + 1) i → 1 ≤ (extras i).head) {inputLength H : ℕ} (hspace : z.length + S z.length + 1 ≤ H) (hr : max r.head 1 ≤ inputLength + H + 1) (hextraH : ∀ (i : Fin (pre + (k + 1) + post)), ¬placeWorkInMiddle pre (k + 1) i → (extras i).head ≤ H) : (placeWorkTM pre post M.retargetInputStarted).HoareTime (fun (inp : Tape) (work : Fin (pre + (k + 1) + post) → Tape) (out : Tape) => inp = r ∧ work = (M.retargetInputStarted.placeWorkCfg pre post extras (M.retargetInputStartedCfg z r)).work ∧ out = parkedBlank) (fun (x : Tape) (work : Fin (pre + (k + 1) + post) → Tape) (out : Tape) => ((z ∈ L → out.cells 1 = Γ.one) ∧ (z ∉ L → out.cells 1 = Γ.zero)) ∧ ∀ (i : Fin (pre + (k + 1) + post)), ¬placeWorkInMiddle pre (k + 1) i → work i = extras i) (T z.length) ∧ (placeWorkTM pre post M.retargetInputStarted).HoareSafety (fun (inp : Tape) (work : Fin (pre + (k + 1) + post) → Tape) (out : Tape) => inp = r ∧ work = (M.retargetInputStarted.placeWorkCfg pre post extras (M.retargetInputStartedCfg z r)).work ∧ out = parkedBlank) fun (inp : Tape) (work : Fin (pre + (k + 1) + post) → Tape) (out : Tape) => { state := (), input := inp, work := work, output := out }.WithinDecisionSpace inputLength H

The same verifier phase in a genuinely separate work-tape block. Extras outside the block retain their tapes exactly and are charged against H.