Cook–Levin machines: polynomial-time unary multiplication closure

Proved

CookLevin.polyTime_unary_product

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

arithmeticcook-levinpolynomial-timeturing-machines

If the unary encodings of f(x) and g(x) are polynomial-time computable, then so is the unary encoding of f(x)g(x). The proof constructs a machine from the two source computations, aligns their alphabets, executes them in separate work banks, resets their heads, and multiplies their terminated unary prefixes. Its bound is 6T1 + 2T2 + 2T1*T2 + 5. For source polynomial degrees d1 and d2, degree d1+d2 suffices. This is a closure theorem for actual Turing-machine computation, not merely an output-length estimate.

Preamble

import Definitions.Def_CookLevin_Complexity
open CookLevin
set_option autoImplicit false

Formal statement

theorem CookLevin.polyTime_unary_product (f g : List Bool → Nat)
    (hf : IsPolyTimeComputable (fun x => List.replicate (f x) true))
    (hg : IsPolyTimeComputable (fun x => List.replicate (g x) true)) :
    IsPolyTimeComputable (fun x => List.replicate (f x * g 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