From Mathlib TM2 computations to CSLib polynomial time

Mathlib counts one fixed stack-machine statement per transition. The simulation certifies each statement using CSLib's list and finite-table calculus, then iterates it for the source polynomial clock. Encoded configurations have linear growth in source time. The resulting certificate is for an actual tidy binary multi-tape Turing machine, with polynomial time and space.

Input and output words use encList (encFinite _). Their alphabets may differ or be empty. Typed encoders must be injective, as required by CSLib. Every working alphabet must be finite; Mathlib's FinTM2 alone only guarantees finiteness of the input alphabet.

Main results

• Turing.TM2ComputableInPolyTime.computableTidilyInPolyTime: transfer a typed Mathlib polynomial-time certificate to CSLib.

This is a polynomial-time bridge, not a space-preserving simulation or a converse equivalence.

References

The source model and runtime convention are Mathlib's Mathlib.Computability.TuringMachine.Computable and Mathlib.Computability.TuringMachine.StackTuringMachine. This is a direct proof through the tidy calculus, independent of the TM2-to-TM0 compiler in Complexitylib PR #72.

theorem Turing.TM2.stepTotal_of_step {K : Type} [DecidableEq K] {Γ : K → Type} {Λ σ : Type} (M : Λ → Stmt Γ Λ σ) (cfg : Cfg Γ Λ σ) : stepTotal M cfg = (step M cfg).getD cfg

A source clock may continue after halting without changing the result.

theorem Turing.TM2.iterate_stepTotal_of_evals (tm : FinTM2) (input : List (tm.Γ tm.k₀)) (output : List (tm.Γ tm.k₁)) (time : ℕ) (h : TM2OutputsInTime tm input (some output) time) : (stepTotal tm.m)^[time] (initList tm input) = haltList tm output

Bounded partial execution to a halted configuration agrees with the padded total clock.

theorem Turing.TM2.initList_polyTime (tm : FinTM2) [∀ (k : tm.K), Finite (tm.Γ k)] : MultiTapeTM.ComputableTidilyInPolyTime (initList tm) (MultiTapeTM.encList (MultiTapeTM.encFinite (tm.Γ tm.k₀))) encCfg

Initialization copies the source input and supplies empty auxiliary stacks.

theorem Turing.TM2.run_polyTime (tm : FinTM2) [∀ (k : tm.K), Finite (tm.Γ k)] (p : Polynomial ℕ) : MultiTapeTM.ComputableTidilyInPolyTime (fun (input : List (tm.Γ tm.k₀)) => (stepTotal tm.m)^[Polynomial.eval input.length p] (initList tm input)) (MultiTapeTM.encList (MultiTapeTM.encFinite (tm.Γ tm.k₀))) encCfg

Polynomially many source steps have polynomially bounded encoded intermediate states.

theorem Turing.TM2ComputableInPolyTime.computableTidilyInPolyTime {α β αΓ βΓ : Type} [Finite αΓ] [Finite βΓ] {ea : α → List αΓ} {eb : β → List βΓ} {f : α → β} (h : TM2ComputableInPolyTime ea eb f) [∀ (k : h.tm.K), Finite (h.tm.Γ k)] (ha : Function.Injective ea) (hb : Function.Injective eb) : MultiTapeTM.ComputableTidilyInPolyTime f ({ toFun := ea, inj' := ha }.trans (MultiTapeTM.encList (MultiTapeTM.encFinite αΓ))) ({ toFun := eb, inj' := hb }.trans (MultiTapeTM.encList (MultiTapeTM.encFinite βΓ)))

A finite-alphabet Mathlib certificate gives tidy CSLib polynomial-time computation under the standard binary encodings of its input and output words.