Whole-run correspondence before cleanup

The compiler executes exactly one source transition per TM2 transition until the first halting source configuration. Its next transition enters cleanup. These statements include the final source action, which may write, move heads and emit a bit while halting.

Main results

• Turing.MultiTapeTM.ToTM2.iterate_encode: correspondence of every source execution prefix.
• Turing.MultiTapeTM.ToTM2.prefixEvals: the same correspondence with Mathlib's partial clock.

theorem Turing.MultiTapeTM.ToTM2.stepTotal_encode_halt {k : ℕ} {State : Type} [Fintype State] (tm : MultiTapeTM k Bool State) (d : Data k State) (hq : d.state = none) : TM2.stepTotal (program tm.q₀ tm.tr) (encode d) = { l := some Label.clean, var := control d d.input.right.head?, stk := store d }

theorem Turing.MultiTapeTM.ToTM2.iterate_encode {k : ℕ} {State : Type} [Fintype State] (tm : MultiTapeTM k Bool State) (input : List Bool) {t : ℕ} (ht : tm.HaltsAt (tm.initCfg input) t) {i : ℕ} (hi : i ≤ t) : (TM2.stepTotal (program tm.q₀ tm.tr))^[i] (initList (machine tm.q₀ tm.tr) input) = encode (Data.run tm input i)

Every source prefix through the first halted configuration is reproduced exactly.

def Turing.MultiTapeTM.ToTM2.prefixEvals {k : ℕ} {State : Type} [Fintype State] (tm : MultiTapeTM k Bool State) (input : List Bool) {t : ℕ} (ht : tm.HaltsAt (tm.initCfg input) t) {i : ℕ} (hi : i ≤ t) : StateTransition.EvalsToInTime (machine tm.q₀ tm.tr).step (initList (machine tm.q₀ tm.tr) input) (some (encode (Data.run tm input i))) i

Mathlib's partial execution reaches each source prefix in exactly that many transitions.