Canonical FP membership from a Mathlib TM2 string certificate

Compile the source once and supply its exact stack-track input through the marked copier. The target computes reversal composed with the source function and reversal. Closure of FP under composition removes those representation conventions. A source stack-growth bound supplies the required output length.

theorem Complexity.MathlibTM2.marked_run_eq_exec (M : MathlibTM0.MarkedMachine) (t : ℕ) (c : M.Config) : M.run t c = exec (Turing.TM0.step M.code) t c

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