Polynomial-time normal forms — proof internals

The definitions of P and FP permit arbitrary time functions with Big-O power bounds. This module replaces either witness by the evaluation of one polynomial over the naturals, giving everywhere-valid monotone time bounds.

The public theorem is in Complexitylib.Classes.P.NormalForm.

theorem Complexity.mem_P_iff_decidesInTime_polynomial_internal {L : Language} : L ∈ P ↔ ∃ (k : ℕ) (tm : TM k) (p : Polynomial ℕ), tm.DecidesInTime L fun (x : ℕ) => Polynomial.eval x p

Internal proof that P membership is equivalent to decision within the evaluation of a natural-coefficient polynomial.

theorem Complexity.mem_FP_iff_computesInTime_polynomial_internal {f : List Bool → List Bool} : f ∈ FP ↔ ∃ (k : ℕ) (tm : TM k) (p : Polynomial ℕ), tm.ComputesInTime f fun (x : ℕ) => Polynomial.eval x p

Internal proof that FP membership is equivalent to computation within the evaluation of a natural-coefficient polynomial.