Mathlib's stack-to-tape compiler has polynomial overhead

Mathlib already compiles TM2 → TM1 → TM0. This module proves that its compiler is efficient: a fixed finitely supported stack program has one finite-state tape simulator running in C * (input.length + sourceTime + 1)^2 transitions. The constant depends only on the program. The stack-track alphabet is finite whenever there are finitely many stacks and each stack alphabet is finite.

exists_tm0_computer applies directly to Mathlib's bundled FinTM2 and TM2OutputsInTime. Both the input and the complete output tape are exactly TM2to1.trInit of the corresponding stack word, including its bottom marker. This format stores stacks bottom first. The separate Complexitylib.Interop.Mathlib.TM2.FP interface supplies the binary input/output adapters and canonical FP transfer for finite working alphabets.

The timing proofs are reused from the rational hitting-list development and remain in their original modules and namespaces.

theorem Complexity.MathlibTM2.exists_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

Every output stack has length at most the initial input length plus a fixed multiple of the source transition count.

theorem Complexity.MathlibTM2.exists_tm0_simulator {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

Mathlib's existing stack compiler simulates every terminating source run with quadratic transition overhead, retaining the entire represented stack state.

theorem Complexity.MathlibTM2.exists_tm0_computer (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)

A bundled Mathlib TM2 has a fixed finite-state tape computer with quadratic overhead and exact input/output stack-track tapes, including empty words.

theorem Complexity.MathlibTM2.exists_tm0_polynomial_computer {α β Γ Δ : Type} {input : α → List Γ} {output : β → List Δ} {f : α → β} (computer : Turing.TM2ComputableInPolyTime input output f) : ∃ (m : ℕ) (G : Turing.TM0.Machine (Turing.TM2to1.Γ' computer.tm.K computer.tm.Γ) (Fin (m + 1))) (p : Polynomial ℕ), ∀ (a : α), ∃ u ≤ Polynomial.eval (input a).length p, ∃ (c : Turing.TM0.Cfg (Turing.TM2to1.Γ' computer.tm.K computer.tm.Γ) (Fin (m + 1))), exec (Turing.TM0.step G) u (Turing.TM0.init (Turing.TM2to1.trInit computer.tm.k₀ (List.map (⇑computer.inputAlphabet.symm) (input a)))) = some c ∧ Turing.TM0.step G c = none ∧ c.Tape = Turing.Tape.mk₁ (Turing.TM2to1.trInit computer.tm.k₁ (List.map (⇑computer.outputAlphabet.symm) (output (f a))))

A Mathlib polynomial-time certificate yields one finite-state TM0 and a polynomial time bound, with its encoded input and complete output tapes explicit.