Every fixed clause-width bound has a polynomial-time WordRAM certificate verifier

Proved

KSat.ksat_ram_verifier

by wurtle · Oct 5, 2026 · Mathlib 0df444a (Lean v4.33.1)

complexity-theorynp-completenesswordram

For every fixed natural number $k$ , there are a restricted WordRAM algorithm $A$ , a Boolean verifier $V$ on pairs of bit strings, and natural constants $a,b$ , such that $A$ decides $V$ in polynomially many WordRAM steps on every input pair and

V(x,y)=1 \Longrightarrow |y|\le a(|x|+1)^b,

x\in k\text{-SAT}\quad\Longleftrightarrow\quad\exists y,\ V(x,y)=1.

Here $k$ -SAT is the mission's language of encodings of satisfiable CNF formulas with at most $k$ literal occurrences per clause. All bit strings are in the verifier's input domain; malformed encodings, over-width formulas, and overlong certificates must be rejected. Empty formulas, empty clauses, repeated literals, and $k=0$ retain the published definitions' meanings. The algorithm and bounds may depend on the fixed $k$ .

This is the certificate-verification component of the NP-membership argument, with a concrete WordRAM implementation obligation. The published polynomial simulation backend can translate it to the mission's Turing-machine definition of NP.

Formalization Note This specializes the standard assignment-verification argument to the mission's existing unary, self-delimiting formula encoding and its restricted WordRAM model; it does not assert an instruction listing or a particular polynomial exponent.

Preamble

import Definitions.Def_WordRAM_Complexity_BitIO
import Definitions.Def_KSat_Languages

set_option autoImplicit false

Formal statement

theorem KSat.ksat_ram_verifier (k : Nat) :
    ∃ (A : WordRAM.Complexity.Algorithm .restricted)
      (V : List Bool → List Bool → Bool) (a b : Nat),
      WordRAM.Complexity.RAMPolyTimeDecidable A V ∧
      (∀ x y, V x y = true → y.length ≤ CookLevin.polyBound a b x.length) ∧
      (∀ x, KSat.KSAT k x ↔ ∃ y, V x y = true) := by sorry

Source

Karp (1972), Reducibility Among Combinatorial Problems, Main Theorem, pp. 94–95, problem 11; https://doi.org/10.1007/978-1-4684-2001-2_9 . Assignment-verifier argument: Madhu Sudan, CS121 Lecture 19 (2020), slides 16–17, https://people.seas.harvard.edu/~madhusudan/courses/Fall2020/Lectures/L19-after.pdf . Fixed-k extension and WordRAM implementation are the explicit formalization obligations here.

View graph