Cook–Levin machines: polynomial-time evaluation of natural polynomials

Proved

CookLevin.polyTime_unary_polynomial

by Robertboy18 · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

arithmeticcook-levinpolynomial-timeturing-machines

For every fixed polynomial p with natural coefficients, if f(x) is polynomial-time computable in unary, then p(f(x)) is polynomial-time computable in unary. The proof constructs constants, sums, and fixed powers from accepted Turing-machine closure theorems and applies polynomial induction. Specializing f to input length gives an actual emitter for every natural polynomial in input length, not just an output-length bound.

Preamble

import Definitions.Def_CookLevin_Complexity
import Mathlib.Algebra.Polynomial.Eval.Defs
open CookLevin
set_option autoImplicit false

Formal statement

theorem CookLevin.polyTime_unary_polynomial (p : Polynomial Nat) (f : List Bool → Nat)
    (hf : IsPolyTimeComputable (fun x => List.replicate (f x) true)) :
    IsPolyTimeComputable (fun x => List.replicate (p.eval (f x)) true) := by sorry

Source

Composition of accepted CookLevin machine constructors: alphabet alignment, independent computations, head reset, unary work-bank multiplication, and sequence preservation.

View graph