Work-tape placement correctness internals

This file proves exact step and bounded-reachability commutation for TM.placeWorkTM. The strongest one-step theorem evolves an arbitrary physical extra-tape frame by its prescribed idle action. Stable frames and the canonical parked frame are fixed points of that action.

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

Exact one-step commutation with an arbitrary extra-tape frame. The source machine takes one step while every physical extra tape takes its idle action.

theorem Complexity.TM.placeWorkTM_step_placeWorkCfg_stable_internal {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 observable extra tape is off the left-end marker, the extra frame is fixed and one placed step commutes through the same embedding.

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

Bounded reachability commutes exactly while a stable arbitrary frame is preserved around the source work tapes.

theorem Complexity.TM.placeWorkTM_step_placeWorkParkedCfg_internal {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 frame is fixed by a placed source step.

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

Bounded reachability commutes through the canonical parked embedding.

theorem Complexity.TM.placeWorkTM_step_initCfg_internal {n : ℕ} (tm : TM n) (pre post : ℕ) (x : List Bool) : (placeWorkTM pre post tm).step ((placeWorkTM pre post tm).initCfg x) = Option.map (tm.placeWorkParkedCfg pre post) (tm.step (tm.initCfg x))

The first placed step from the ordinary initial configuration performs the source machine's first step and parks every surrounding blank tape.

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

Simulation from an ordinary initial configuration. At time zero the placed configuration is its ordinary initial configuration; every positive run ends in the canonical parked embedding of the source configuration.

theorem Complexity.TM.placeWorkTM_computesInTime_internal {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 the same time bound.