Retargeted-input computation seam internals

This file proves that TM.retargetInputStarted resumes an ordinary source run after its compulsory sentinel transition. The already-halted case is handled separately: such a machine can compute only the empty output, and the wrapper therefore halts immediately on its parked blank output tape.

theorem Complexity.TM.retargetInputStarted_step_eq_internal {k : ℕ} (M : TM k) (c : Cfg (k + 1) M.Q) : M.retargetInputStarted.step c = M.retargetInput.step c

The started wrapper has exactly the same transition behavior as the ordinary retargeted-input machine.

theorem Complexity.TM.retargetInputStarted_reachesIn_of_retargetInput_internal {k : ℕ} (M : TM k) {t : ℕ} {c c' : Cfg (k + 1) M.Q} (hreach : M.retargetInput.reachesIn t c c') : M.retargetInputStarted.reachesIn t c c'

Any bounded run of the ordinary retargeted-input machine is also a run of the started wrapper.

theorem Complexity.TM.retargetInputStarted_qstart_eq_startedCfg_state_internal {k : ℕ} (M : TM k) (y : List Bool) (hne : M.qstart ≠ M.qhalt) : M.retargetInputStarted.qstart = (M.startedCfg y hne).state

In the nondegenerate case, the wrapper start state is exactly the source state after its first transition from the all-sentinel configuration.

theorem Complexity.TM.retargetInputStartedCfg_eq_retargetWrap_internal {k : ℕ} (M : TM k) (y : List Bool) (realInput : Tape) (hne : M.qstart ≠ M.qhalt) : M.retargetInputStartedCfg y realInput = M.retargetWrap realInput (M.startedCfg y hne)

In the nondegenerate case, the canonical wrapper entry is the ordinary retargetWrap of the source's exact post-sentinel configuration.

theorem Complexity.TM.retargetInputStarted_computesVirtual_exact_internal {k : ℕ} (M : TM k) {f : List Bool → List Bool} {T : ℕ → ℕ} (hcomp : M.ComputesInTime f T) (y : List Bool) (realInput : Tape) : ∃ (c' : Cfg (k + 1) M.Q) (t : ℕ), (t + if M.qstart = M.qhalt then 0 else 1) ≤ T y.length ∧ M.retargetInputStarted.reachesIn t (M.retargetInputStartedCfg y realInput) c' ∧ M.retargetInputStarted.halted c' ∧ c'.output.HasOutput (f y)

Exact virtual-input computation seam. The result time omits the source's first transition when that transition exists; an initially halted source uses zero steps.

theorem Complexity.TM.retargetInputStarted_computesVirtual_internal {k : ℕ} (M : TM k) {f : List Bool → List Bool} {T : ℕ → ℕ} (hcomp : M.ComputesInTime f T) (y : List Bool) (realInput : Tape) : ∃ (c' : Cfg (k + 1) M.Q), ∃ t ≤ T y.length, M.retargetInputStarted.reachesIn t (M.retargetInputStartedCfg y realInput) c' ∧ M.retargetInputStarted.halted c' ∧ c'.output.HasOutput (f y)

Same-time form of the virtual-input computation seam.

theorem Complexity.TM.retargetInputStarted_decidesVirtual_internal {k : ℕ} (M : TM k) {L : Language} {T : ℕ → ℕ} (hdec : M.DecidesInTime L T) (y : List Bool) (realInput : Tape) : ∃ (c' : Cfg (k + 1) M.Q), ∃ t ≤ T y.length, M.retargetInputStarted.reachesIn t (M.retargetInputStartedCfg y realInput) c' ∧ M.retargetInputStarted.halted c' ∧ (y ∈ L → c'.output.cells 1 = Γ.one) ∧ (y ∉ L → c'.output.cells 1 = Γ.zero)

A decider run can be resumed on a virtual input with the same advertised time bound while retaining both verdict implications.

theorem Complexity.TM.retargetInputStarted_hoareTime_internal {k : ℕ} (M : TM k) {f : List Bool → List Bool} {T : ℕ → ℕ} (hcomp : M.ComputesInTime f T) (y : List Bool) : M.retargetInputStarted.HoareTime (fun (inp : Tape) (work : Fin (k + 1) → Tape) (out : Tape) => work = (M.retargetInputStartedCfg y inp).work ∧ out = (Tape.init []).move Dir3.right) (fun (_inp : Tape) (_work : Fin (k + 1) → Tape) (out : Tape) => out.HasOutput (f y)) (T y.length)

Hoare form of the same-time virtual-input seam.

theorem Complexity.TM.placeWorkTM_retargetInputStarted_computesVirtual_internal {k : ℕ} (M : TM k) (pre post : ℕ) (extras : Fin (pre + (k + 1) + post) → Tape) {f : List Bool → List Bool} {T : ℕ → ℕ} (hcomp : M.ComputesInTime f T) (y : List Bool) (realInput : Tape) (hinv : ∀ (i : Fin (pre + (k + 1) + post)), ¬placeWorkInMiddle pre (k + 1) i → (extras i).StartInvariant) (hhead : ∀ (i : Fin (pre + (k + 1) + post)), ¬placeWorkInMiddle pre (k + 1) i → 1 ≤ (extras i).head) : ∃ (c' : Cfg (k + 1) M.Q) (C' : Cfg (pre + (k + 1) + post) (placeWorkTM pre post M.retargetInputStarted).Q), ∃ t ≤ T y.length, (placeWorkTM pre post M.retargetInputStarted).reachesIn t (M.retargetInputStarted.placeWorkCfg pre post extras (M.retargetInputStartedCfg y realInput)) C' ∧ C' = M.retargetInputStarted.placeWorkCfg pre post extras c' ∧ (placeWorkTM pre post M.retargetInputStarted).halted C' ∧ C'.output.HasOutput (f y)

Combined placement seam with an exact preserved physical frame. The source work tapes and virtual input occupy the placed middle block; all prefix and suffix tapes are returned unchanged.

theorem Complexity.TM.placeWorkTM_retargetInputStarted_decidesVirtual_internal {k : ℕ} (M : TM k) (pre post : ℕ) (extras : Fin (pre + (k + 1) + post) → Tape) {L : Language} {T : ℕ → ℕ} (hdec : M.DecidesInTime L T) (y : List Bool) (realInput : Tape) (hinv : ∀ (i : Fin (pre + (k + 1) + post)), ¬placeWorkInMiddle pre (k + 1) i → (extras i).StartInvariant) (hhead : ∀ (i : Fin (pre + (k + 1) + post)), ¬placeWorkInMiddle pre (k + 1) i → 1 ≤ (extras i).head) : ∃ (c' : Cfg (k + 1) M.Q) (C' : Cfg (pre + (k + 1) + post) (placeWorkTM pre post M.retargetInputStarted).Q), ∃ t ≤ T y.length, (placeWorkTM pre post M.retargetInputStarted).reachesIn t (M.retargetInputStarted.placeWorkCfg pre post extras (M.retargetInputStartedCfg y realInput)) C' ∧ C' = M.retargetInputStarted.placeWorkCfg pre post extras c' ∧ (placeWorkTM pre post M.retargetInputStarted).halted C' ∧ (y ∈ L → C'.output.cells 1 = Γ.one) ∧ (y ∉ L → C'.output.cells 1 = Γ.zero)

Placed virtual-input decision with an exact preserved physical frame.