Finite-state compilation of arbitrary supported TM2 programs

This packages the existing Mathlib compiler and its timing lemmas for any finitely supported stack program with finite auxiliary state. The target's alphabet is exactly Mathlib's stack-track alphabet; no external recoding is hidden in the input or output contract. The timing lemmas remain in the rational hitting-list development; compile_source generalizes the assembly used in its FiniteCompiler module.

theorem Complexity.MathlibTM2.compile_source {K : Type} {Γ : K → Type} {Λ σ : Type} [DecidableEq K] [Inhabited Λ] [Inhabited σ] [Fintype σ] (M : Λ → Turing.TM2.Stmt Γ Λ σ) (F : Finset Λ) (hF : Turing.TM2.Supports M F) : ∃ (m : ℕ) (G : Turing.TM0.Machine (Turing.TM2to1.Γ' K Γ) (Fin (m + 1))) (C : ℕ), 0 < C ∧ ∀ (k : K) (w : List (Γ k)) (b : Turing.TM2.Cfg Γ Λ σ) (t : ℕ), exec (Turing.TM2.step M) t (Turing.TM2.init k w) = some b → Turing.TM2.step M b = none → ∃ u ≤ C * (w.length + t + 1) ^ 2, ∃ (a : Turing.TM0.Cfg (Turing.TM2to1.Γ' K Γ) (Fin (m + 1))), exec (Turing.TM0.step G) u (Turing.TM0.init (Turing.TM2to1.trInit k w)) = some a ∧ Turing.TM0.step G a = none ∧ ∃ (c : Turing.TM1.Cfg (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ), Turing.TM2to1.TrCfg b c ∧ a.Tape = c.Tape

theorem Complexity.MathlibTM2.tape_unique {K : Type} {Γ : K → Type} {Λ σ : Type} {a b : Turing.TM2.Cfg Γ Λ σ} {c d : Turing.TM1.Cfg (Turing.TM2to1.Γ' K Γ) (Turing.TM2to1.Λ' K Γ Λ σ) σ} (h : Turing.TM2to1.TrCfg a c) (h' : Turing.TM2to1.TrCfg b d) (hs : a.stk = b.stk) : c.Tape = d.Tape

theorem Complexity.MathlibTM2.exec_eq_iterate {α : Type u_1} (step : α → Option α) (t : ℕ) (a : α) : exec step t a = (fun (s : Option α) => s.bind step)^[t] (some a)

theorem Complexity.MathlibTM2.output_length_bound (tm : Turing.FinTM2) : ∃ (C : ℕ), 0 < C ∧ ∀ (input : List (tm.Γ tm.k₀)) (output : List (tm.Γ tm.k₁)) (time : ℕ) (a : Turing.TM2OutputsInTime tm input (some output) time), output.length ≤ input.length + C * time

theorem Complexity.MathlibTM2.compile_bundled (tm : Turing.FinTM2) : ∃ (m : ℕ) (G : Turing.TM0.Machine (Turing.TM2to1.Γ' tm.K tm.Γ) (Fin (m + 1))) (C : ℕ), 0 < C ∧ ∀ (input : List (tm.Γ tm.k₀)) (output : List (tm.Γ tm.k₁)) (time : ℕ) (a : Turing.TM2OutputsInTime tm input (some output) time), ∃ u ≤ C * (input.length + time + 1) ^ 2, ∃ (a : Turing.TM0.Cfg (Turing.TM2to1.Γ' tm.K tm.Γ) (Fin (m + 1))), exec (Turing.TM0.step G) u (Turing.TM0.init (Turing.TM2to1.trInit tm.k₀ input)) = some a ∧ Turing.TM0.step G a = none ∧ a.Tape = Turing.Tape.mk₁ (Turing.TM2to1.trInit tm.k₁ output)