Log-space transducers run in polynomial time — proof internals

This module turns the finite reduced-configuration bound for deterministic transducers into a polynomial bound when the auxiliary space is logarithmic. The public results are in Complexitylib.Classes.L.PolynomialTime.

theorem Complexity.TM.transducerConfigBound_bigO_polynomial_internal {k : ℕ} (tm : TM k) {S : ℕ → ℕ} (hS : BigO S fun (n : ℕ) => Nat.log 2 n) : ∃ (c : ℕ), BigO (fun (n : ℕ) => tm.transducerConfigBound n (S n)) fun (x : ℕ) => x ^ (1 + (2 * c + 1) * k)

Internal polynomial bound for the reduced configurations of a logarithmic-space transducer.

theorem Complexity.L_subset_P_internal : L ⊆ P

Internal containment of deterministic logarithmic-space transducer languages in polynomial time.

theorem Complexity.FL_subset_FP_internal : FL ⊆ FP

Internal containment of deterministic logarithmic-space transducer functions in polynomial-time transducer functions.