Canonical FP transfer with finite input and output alphabets

The compiler's stack tracks are unchanged. Explicit symbol codes add linear parsing and emission cost. Palindromic codewords let ordinary binary reversal restore the stack order, even when input and output alphabets differ.

theorem Complexity.MathlibTM2.alphabetAdapter_input {α β : Type} (tm : Turing.FinTM2) [(k : tm.K) → Fintype (tm.Γ k)] (input : tm.Γ tm.k₀ ≃ α) (output : tm.Γ tm.k₁ ≃ β) {Q : Type} [Fintype Q] [Inhabited Q] (G : Turing.TM0.Machine (Turing.TM2to1.Γ' tm.K tm.Γ) Q) (w : List α) : (alphabetAdapter tm input output G).inputCells true w = Turing.TM2to1.trInit tm.k₀ (List.map (⇑input.symm) w.reverse)

theorem Complexity.MathlibTM2.coded_reversal {α β : Type} (ci : FiniteAlphabetCode α) (co : FiniteAlphabetCode β) (f : List α → List β) : List.reverse ∘ (ci.map co fun (xs : List α) => (f xs.reverse).reverse) ∘ List.reverse = ci.map co f

theorem Complexity.MathlibTM2.mem_FP_encoded_proof {α β : 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

theorem Complexity.MathlibTM2.mem_FP_encoded_on_dfa_proof {α β : 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