Marked finite-tape computations transfer to canonical FP

The source input may distinguish its first symbol and use a marker for the empty word. Output is read through a separate decoder. The existing binary-track simulator handles these formats with linear initialization and emission cost.

theorem Complexity.MathlibTM0.MarkedMachine.computes_cslib (M : MarkedMachine) {input output : List Bool} {time : ℕ} (h : M.OutputsWithin input output time) : M.machine.ComputesInTimeAndSpace input output (2 * input.length + time + output.length + 4) (Turing.MultiTapeTM.spaceUsed (Turing.MultiTapeTM.initCfg input) (2 * input.length + time + output.length + 4))

Marked input and a separate output decoder add only linear simulation overhead.

theorem Complexity.MathlibTM0.MarkedMachine.mem_FP {M : MarkedMachine} {f : List Bool → List Bool} {p q : Polynomial ℕ} (h : ∀ (input : List Bool), M.OutputsWithin input (f input) (Polynomial.eval input.length p)) (hlen : ∀ (input : List Bool), (f input).length ≤ Polynomial.eval input.length q) : f ∈ FP

Polynomial source time and decoded output length imply canonical FP membership.

theorem Complexity.MathlibTM0.MarkedMachine.mem_FP_on_dfa {M : MarkedMachine} {σ : Type} [Fintype σ] (D : DFA Bool σ) [DecidablePred fun (x : List Bool) => x ∈ D.accepts] {f : List Bool → List Bool} {p q : Polynomial ℕ} (h : ∀ w ∈ D.accepts, M.OutputsWithin w (f w) (Polynomial.eval w.length p)) (hlen : ∀ w ∈ D.accepts, (f w).length ≤ Polynomial.eval w.length q) : (fun (w : List Bool) => if w ∈ D.accepts then f w else []) ∈ FP

Source bounds only on a regular domain suffice after rejecting malformed inputs.