Exact configuration transport

Successful-step preservation transports exact runs without changing their duration. The stronger equality of optional steps also reflects every reachable configuration from an embedded start. The distinction matters: a controller may continue after a child halts, whereas a tape-layout embedding reflects the child's halt as well.

No injectivity, halting-time bound, or tape invariant is assumed implicitly.

theorem Complexity.TM.reachesIn_transport {n n' : ℕ} {tm : TM n} {tm' : TM n'} (R : Cfg n tm.Q → Cfg n' tm'.Q → Prop) (h_step : ∀ {c c' : Cfg n tm.Q} {d : Cfg n' tm'.Q}, R c d → tm.step c = some c' → ∃ (d' : Cfg n' tm'.Q), tm'.step d = some d' ∧ R c' d') {t : ℕ} {c c' : Cfg n tm.Q} (hreach : tm.reachesIn t c c') {d : Cfg n' tm'.Q} (hR : R c d) : ∃ (d' : Cfg n' tm'.Q), tm'.reachesIn t d d' ∧ R c' d'

A relation preserved by one successful step transports an exact run. The relation may carry a source invariant and an evolving extra-tape frame; both remain explicit in the caller's one-step obligation. No halt reflection or injectivity is required.

theorem Complexity.TM.reachesIn_map' {n n' : ℕ} {tm : TM n} {tm' : TM n'} (wrap : Cfg n tm.Q → Cfg n' tm'.Q) (h_step : ∀ (c c' : Cfg n tm.Q), tm.step c = some c' → tm'.step (wrap c) = some (wrap c')) {t : ℕ} {c c' : Cfg n tm.Q} (hreach : tm.reachesIn t c c') : tm'.reachesIn t (wrap c) (wrap c')

Cross-arity generalization of reachesIn_map: the simulating machine may have a different number of work tapes. If wrap commutes with step, then reachesIn lifts through the embedding.

theorem Complexity.TM.reaches_map_reflect {n n' : ℕ} {tm : TM n} {tm' : TM n'} (wrap : Cfg n tm.Q → Cfg n' tm'.Q) (h_step : ∀ (c : Cfg n tm.Q), tm'.step (wrap c) = Option.map wrap (tm.step c)) (c₀ : Cfg n tm.Q) (D : Cfg n' tm'.Q) : tm'.reaches (wrap c₀) D → ∃ (c : Cfg n tm.Q), tm.reaches c₀ c ∧ D = wrap c

If optional steps commute with an embedding, every target configuration reachable from an embedded start is the image of a reachable source configuration. This includes all prefixes, not just successful endpoints; no injectivity assumption is needed.