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.computableInPolyTime_encList: transfer a typed Mathlib polynomial-time certificate to CSLib.

This is the forward bridge. TM2.Reverse.Transfer supplies a direct reverse compiler and polynomial-time equivalence, including explicit conversions for these word encodings.

References

The source model and runtime convention are Mathlib's Mathlib.Computability.TuringMachine.Computable and Mathlib.Computability.TuringMachine.StackTuringMachine. This is a direct proof, 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.ComputableInPolyTime (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.ComputableInPolyTime (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.computableInPolyTime_encList {α β αΓ βΓ : Type} [Finite αΓ] {encA : αΓ ↪ List Bool} {encB : βΓ ↪ List Bool} {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.ComputableInPolyTime f ({ toFun := ea, inj' := ha }.trans (MultiTapeTM.encList encA)) ({ toFun := eb, inj' := hb }.trans (MultiTapeTM.encList encB))

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