Exact-run decomposition — proof internals

These small deterministic-run lemmas expose configurations at chosen time indices. They support the finite reduced-configuration argument without adding execution choices to the machine model.

theorem Complexity.TM.reachesIn_split_internal {n : ℕ} {tm : TM n} {a b : ℕ} {c c' : Cfg n tm.Q} (hreach : tm.reachesIn (a + b) c c') : ∃ (d : Cfg n tm.Q), tm.reachesIn a c d ∧ tm.reachesIn b d c'

Split an exact run at a prescribed prefix length.

theorem Complexity.TM.reachesIn_prefix_internal {n : ℕ} {tm : TM n} {t i : ℕ} {c c' : Cfg n tm.Q} (hreach : tm.reachesIn t c c') (hi : i ≤ t) : ∃ (d : Cfg n tm.Q), tm.reachesIn i c d ∧ tm.reachesIn (t - i) d c'

Expose the configuration at time i of an exact t-step run.