Stack-growth bounds using the existing simulation tools

The rational hitting-list development already proves timing bounds for Mathlib's TM2-to-TM1 and TM1-to-TM0 compilers, together with finite-state restriction. Those proofs remain in their original modules and namespaces. This module reuses them and adds a bound on the length of each stack.

theorem Complexity.MathlibTM2.StackToOne.execution_length {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} [DecidableEq K] (M : Λ → Turing.TM2.Stmt Γ Λ σ) [Inhabited Λ] (F : Finset Λ) (hF : Turing.TM2.Supports M F) (C : ℕ) (hC : ∀ l ∈ F, stackWeight (M l) + 1 ≤ C) (t : ℕ) (a b : Turing.TM2.Cfg Γ Λ σ) (L : ℕ) (ha : a.l ∈ Finset.insertNone F) (hS : ∀ (k : K), (a.stk k).length ≤ L) (hr : exec (Turing.TM2.step M) t a = some b) (k : K) : (b.stk k).length ≤ L + C * t

Each stack grows at most linearly in the number of source transitions.