Retargeted-input computation seams

TM.retargetInputStarted runs a source machine on a virtual input held by its last work tape when every participating head is already parked at cell 1. It absorbs the source machine's compulsory first transition from ▷, making the wrapper suitable as a later phase of TM.seqTM.

The degenerate qstart = qhalt case is included: such a source computes only the empty string, and the wrapper halts immediately without requiring a positive advertised time bound.

Main results

• TM.retargetInputStarted_computesVirtual_exact — exact saved-start time
• TM.retargetInputStarted_computesVirtual — same-time virtual computation
• TM.retargetInputStarted_decidesVirtual — same-time virtual decision
• TM.retargetInputStarted_hoareTime — Hoare form for phase composition
• TM.placeWorkTM_retargetInputStarted_computesVirtual — placed stable-frame seam
• TM.placeWorkTM_retargetInputStarted_decidesVirtual — placed decision seam

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

The started wrapper and ordinary retargeted-input machine have identical step functions.

theorem Complexity.TM.retargetInputStarted_reachesIn_of_retargetInput {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'

A run of retargetInput M is also a run of its started wrapper.

theorem Complexity.TM.retargetInputStartedCfg_eq_retargetWrap {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)

For a non-halted source start state, the wrapper entry configuration is exactly the retargeted embedding of the source's post-sentinel configuration.

theorem Complexity.TM.retargetInputStarted_computesVirtual_exact {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. A nondegenerate source run saves its first transition; an initially halted source uses zero transitions.

theorem Complexity.TM.retargetInputStarted_computesVirtual {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)

The started virtual-input wrapper computes within the source's advertised time bound.

theorem Complexity.TM.retargetInputStarted_decidesVirtual {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)

The started virtual-input wrapper retains a source decider's two verdict implications within the source's advertised time bound.

theorem Complexity.TM.retargetInputStarted_hoareTime {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. The real input is ignored; the work and output tapes have the canonical already-started shapes.

theorem Complexity.TM.placeWorkTM_retargetInputStarted_computesVirtual {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)

Placed virtual-input computation with an exact preserved prefix/suffix frame. The middle block contains the source scratch tapes and virtual input. Every extra tape satisfying the standard start invariant at a positive head position is unchanged in the final placeWorkCfg endpoint.

theorem Complexity.TM.placeWorkTM_retargetInputStarted_decidesVirtual {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 prefix/suffix frame.