Mathlib TM2 string computations belong to canonical FP

A polynomial-time Mathlib certificate for a total binary-string function yields membership in Complexitylib's canonical machine-based FP. All working stack alphabets are explicitly required to be finite; Mathlib's FinTM2 bundle itself only includes input-alphabet finiteness. Marked input copying, complete output decoding, and string reversal account for the stack representation.

The total-function theorem uses the identity encoding on all binary strings. For a regular domain, mem_FP_on_dfa checks the input format and returns empty output outside the domain; the source time bound is required only inside it. mem_FP_encoded supports independent finite input and output alphabets through explicit binary symbol codes, including empty alphabets. Invalid symbol codes return empty output before the source starts. mem_FP_encoded_on_dfa additionally validates a regular binary input domain. Typed problem encodings still need their own validity and encoding-correspondence arguments.

theorem Complexity.MathlibTM2.mem_FP {f : List Bool → List Bool} (computer : Turing.TM2ComputableInPolyTime id id f) [(k : computer.tm.K) → Fintype (computer.tm.Γ k)] : f ∈ FP

Total Mathlib TM2 binary-string computations with finite working alphabets transfer to the canonical FP class, with no separate output-length assumption.

theorem Complexity.MathlibTM2.mem_FP_on_dfa {f : List Bool → List Bool} (computer : Turing.TM2ComputableAux Bool Bool) [(k : computer.tm.K) → Fintype (computer.tm.Γ k)] {σ : Type} [Fintype σ] (D : DFA Bool σ) [DecidablePred fun (x : List Bool) => x ∈ D.accepts] {p : Polynomial ℕ} (h : (w : List Bool) → w ∈ D.accepts → Turing.TM2OutputsInTime computer.tm (List.map (⇑computer.inputAlphabet.symm) w) (some (List.map (⇑computer.outputAlphabet.symm) (f w))) (Polynomial.eval w.length p)) : (fun (w : List Bool) => if w ∈ D.accepts then f w else []) ∈ FP

Validate a regular input domain and return empty output on malformed strings. Only valid inputs need a source time bound; output length is bounded automatically.

theorem Complexity.MathlibTM2.mem_FP_encoded {α β : Type} {f : List α → List β} (ci : FiniteAlphabetCode α) (co : FiniteAlphabetCode β) (computer : Turing.TM2ComputableInPolyTime id id f) [(k : computer.tm.K) → Fintype (computer.tm.Γ k)] : ci.map co f ∈ FP

Polynomial-time word functions over independent finite alphabets give canonical FP functions under explicit binary codes. Invalid codewords return empty output; no output-size bound is needed.

theorem Complexity.MathlibTM2.mem_FP_encoded_on_dfa {α β : Type} {f : List α → List β} (ci : FiniteAlphabetCode α) (co : FiniteAlphabetCode β) (computer : Turing.TM2ComputableAux α β) [(k : computer.tm.K) → Fintype (computer.tm.Γ k)] {σ : Type} [Fintype σ] (D : DFA Bool σ) [DecidablePred fun (x : List Bool) => x ∈ D.accepts] {p : Polynomial ℕ} (h : (xs : List α) → ci.encode xs ∈ D.accepts → Turing.TM2OutputsInTime computer.tm (List.map (⇑computer.inputAlphabet.symm) xs) (some (List.map (⇑computer.outputAlphabet.symm) (f xs))) (Polynomial.eval xs.length p)) : (fun (bits : List Bool) => if bits ∈ D.accepts then ci.map co f bits else []) ∈ FP

Validate a regular binary domain as well as finite-alphabet symbol codes. Source bounds are required only for source words whose binary encodings lie in the domain.