Work-tape placement

This public surface exposes exact simulation theorems for TM.placeWorkTM. The source machine occupies a contiguous middle block of physical work tapes; prefix and suffix tapes form an arbitrary preserved frame whenever their heads are parked away from the left-end marker.

Main results

• TM.placeWorkTM_step_placeWorkCfg — exact step with an evolving frame
• TM.placeWorkTM_reachesIn_placeWorkCfg_stable — exact stable-frame simulation
• TM.placeWorkTM_reachesIn_placeWorkParkedCfg — canonical parked simulation
• TM.placeWorkTM_computesInTime — same-time preservation of computation

theorem Complexity.TM.placeWorkTM_step_placeWorkCfg {n : ℕ} (tm : TM n) (pre post : ℕ) (extras : Fin (pre + n + post) → Tape) (c : Cfg n tm.Q) : (placeWorkTM pre post tm).step (tm.placeWorkCfg pre post extras c) = Option.map (tm.placeWorkCfg pre post (placeWorkFrameStep extras)) (tm.step c)

A placed step simulates one source step while applying the prescribed idle action to the arbitrary physical extra-tape frame.

theorem Complexity.TM.placeWorkTM_step_placeWorkCfg_stable {n : ℕ} (tm : TM n) (pre post : ℕ) (extras : Fin (pre + n + post) → Tape) (c : Cfg n tm.Q) (hextra : ∀ (i : Fin (pre + n + post)), ¬placeWorkInMiddle pre n i → (extras i).read ≠ Γ.start) : (placeWorkTM pre post tm).step (tm.placeWorkCfg pre post extras c) = Option.map (tm.placeWorkCfg pre post extras) (tm.step c)

If every extra tape reads a non-left-end symbol, its idle action is a no-op and a placed step commutes through the unchanged frame.

theorem Complexity.TM.placeWorkTM_step_placeWorkCfg_of_startInvariant {n : ℕ} (tm : TM n) (pre post : ℕ) (extras : Fin (pre + n + post) → Tape) (c : Cfg n tm.Q) (hinv : ∀ (i : Fin (pre + n + post)), ¬placeWorkInMiddle pre n i → (extras i).StartInvariant) (hhead : ∀ (i : Fin (pre + n + post)), ¬placeWorkInMiddle pre n i → 1 ≤ (extras i).head) : (placeWorkTM pre post tm).step (tm.placeWorkCfg pre post extras c) = Option.map (tm.placeWorkCfg pre post extras) (tm.step c)

Start-invariant extra tapes whose heads are at positive positions form a stable frame for one placed step.

theorem Complexity.TM.placeWorkTM_reachesIn_placeWorkCfg_stable {n : ℕ} (tm : TM n) (pre post : ℕ) (extras : Fin (pre + n + post) → Tape) {t : ℕ} {c c' : Cfg n tm.Q} (hreach : tm.reachesIn t c c') (hextra : ∀ (i : Fin (pre + n + post)), ¬placeWorkInMiddle pre n i → (extras i).read ≠ Γ.start) : (placeWorkTM pre post tm).reachesIn t (tm.placeWorkCfg pre post extras c) (tm.placeWorkCfg pre post extras c')

A stable arbitrary frame is preserved exactly throughout a bounded source run, with no time overhead.

theorem Complexity.TM.placeWorkTM_reachesIn_placeWorkCfg_of_startInvariant {n : ℕ} (tm : TM n) (pre post : ℕ) (extras : Fin (pre + n + post) → Tape) {t : ℕ} {c c' : Cfg n tm.Q} (hreach : tm.reachesIn t c c') (hinv : ∀ (i : Fin (pre + n + post)), ¬placeWorkInMiddle pre n i → (extras i).StartInvariant) (hhead : ∀ (i : Fin (pre + n + post)), ¬placeWorkInMiddle pre n i → 1 ≤ (extras i).head) : (placeWorkTM pre post tm).reachesIn t (tm.placeWorkCfg pre post extras c) (tm.placeWorkCfg pre post extras c')

Start-invariant positive-head extras remain an exact frame throughout a bounded source run.

theorem Complexity.TM.placeWorkTM_step_placeWorkParkedCfg {n : ℕ} (tm : TM n) (pre post : ℕ) (c : Cfg n tm.Q) : (placeWorkTM pre post tm).step (tm.placeWorkParkedCfg pre post c) = Option.map (tm.placeWorkParkedCfg pre post) (tm.step c)

The canonical parked embedding commutes with one source step.

theorem Complexity.TM.placeWorkTM_reachesIn_placeWorkParkedCfg {n : ℕ} (tm : TM n) (pre post : ℕ) {t : ℕ} {c c' : Cfg n tm.Q} (hreach : tm.reachesIn t c c') : (placeWorkTM pre post tm).reachesIn t (tm.placeWorkParkedCfg pre post c) (tm.placeWorkParkedCfg pre post c')

The canonical parked embedding simulates a bounded source run exactly.

@[simp]

theorem Complexity.TM.placeWorkCfg_halted_iff {n : ℕ} (tm : TM n) (pre post : ℕ) (extras : Fin (pre + n + post) → Tape) (c : Cfg n tm.Q) : (placeWorkTM pre post tm).halted (tm.placeWorkCfg pre post extras c) ↔ tm.halted c

A placed embedded configuration is halted exactly when its source configuration is halted.

theorem Complexity.TM.placeWorkTM_reachesIn_init {n : ℕ} (tm : TM n) (pre post : ℕ) (x : List Bool) {t : ℕ} {c' : Cfg n tm.Q} (hreach : tm.reachesIn t (tm.initCfg x) c') : ∃ (C' : Cfg (pre + n + post) (placeWorkTM pre post tm).Q), (placeWorkTM pre post tm).reachesIn t ((placeWorkTM pre post tm).initCfg x) C' ∧ C'.state = c'.state ∧ C'.input = c'.input ∧ C'.output = c'.output ∧ (t = 0 ∨ C' = tm.placeWorkParkedCfg pre post c')

A bounded run from the source's ordinary initial configuration lifts with the same duration. A positive run ends in the canonical parked embedding; at time zero the placed machine remains at its own ordinary initial configuration.

theorem Complexity.TM.placeWorkTM_computesInTime {n : ℕ} (tm : TM n) (pre post : ℕ) {f : List Bool → List Bool} {T : ℕ → ℕ} (hcomp : tm.ComputesInTime f T) : (placeWorkTM pre post tm).ComputesInTime f T

Work-tape placement preserves deterministic function computation with exactly the same time bound. The surrounding blank tapes bounce off ▷ during the source machine's own first step and then remain parked.