Execution correspondence for the reverse TM2 compiler

Each native transition compiles to one fixed Mathlib stack-machine statement. The finite control holds the current work cells; raw stacks retain blank cells and preserve the two-sided geometry.

Main results

• Turing.MultiTapeTM.ToTM2.stepAux_action: a compiled action realizes the raw tape update.

theorem Turing.MultiTapeTM.ToTM2.stepAux_action {k : ℕ} {State : Type} (d : Data k State) (a : Action k Bool State) (symbol : Option Bool) (busy : Bool) : TM2.stepAux (action a) (control d symbol busy) (store d) = encode (d.step a)

One complete compiled action realizes the native update on finite tape data.

theorem Turing.MultiTapeTM.ToTM2.step_encode {k : ℕ} {State : Type} [Fintype State] (tm : MultiTapeTM k Bool State) (d : Data k State) {q : State} (hq : d.state = some q) : TM2.step (program tm.q₀ tm.tr) (encode d) = some (encode (Data.totalStep tm d))

One live source transition is exactly one Mathlib stack-machine transition.

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

A halted source starts cleanup on the following target step.

theorem Turing.MultiTapeTM.ToTM2.encode_init {k : ℕ} {State : Type} [Fintype State] (tm : MultiTapeTM k Bool State) (input : List Bool) : encode (Data.init tm.q₀ input) = initList (machine tm.q₀ tm.tr) input

Native initialization already has the stack layout required by the compiler.