Cook–Levin machines: polynomial-time unary maximum closure

Proved

CookLevin.polyTime_unary_maximum

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

arithmeticcook-levinpolynomial-timeturing-machines

If f(x) and g(x) are polynomial-time computable in unary, then max(f(x),g(x)) is polynomial-time computable in unary. A single loop advances each source head only while it reads one, writes one while either source remains, and halts at both terminators. It preserves both source tapes and supports arbitrary symbols beyond their terminators. Composed with independent computations and head reset, the time bound is 5T1+3T2+5, and the resulting polynomial degree is max(d1,d2). This supplies the maximum operation in the actual Cook-Levin tableau width.

Preamble

import Definitions.Def_CookLevin_Complexity
open CookLevin
set_option autoImplicit false

Formal statement

theorem CookLevin.polyTime_unary_maximum (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 (max (f x) (g x)) true) := by sorry

Source

Direct maximum-loop simulation, spectator padding and tape permutation, followed by accepted independent-computation, reset, sequence, and alphabet-alignment constructors.

View graph