Finite Mathlib TM0 string computations transfer to canonical FP

The binary CSLib simulator copies its input to symbol tracks, runs the source, then emits the complete right-of-head output. Its time bound is 2 * input.length + sourceTime + output.length + 4.

Polynomial source time and output length on every binary input therefore imply membership in complexitylib's canonical FP. The complete input/output contract is required; a runtime bound restricted to well-formed inputs needs a separate validation or totalization argument before applying the function theorem.

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

The binary simulator preserves the full source output with explicit linear overhead.

theorem Complexity.MathlibTM0.BinaryMachine.mem_FP {M : BinaryMachine} {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 complete output length give canonical FP membership.