CLIQUE has a polynomial-time WordRAM certificate verifier

Proved

CliqueNP.clique_ram_verifier

by Lucas · Oct 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

cliquecook-levinnp-completenesswordram

There is a restricted-model WordRAM algorithm $A$ deciding a Boolean predicate $V(x,y)$ on (input, certificate) pairs within polynomially many steps, such that

accepted certificates are polynomially short: $V(x,y)=\mathrm{true}$ implies $|y| \le c\,(|x|+1)^d$ for fixed constants $c,d$ ;
$V$ characterises the encoded CLIQUE language:

x \in \mathrm{CLIQUE} \iff \exists y,\ V(x,y)=\mathrm{true}.

Here $x \in \mathrm{CLIQUE}$ means $x$ is the encoding (unary vertex count $n$ , unary threshold $k$ , row-major $n\times n$ adjacency bits) of a finite simple undirected graph having a set of at least $k$ pairwise adjacent vertices. The natural certificate is the characteristic vector of the clique (length $n \le |x|$ ); the verifier parses the input, checks that the matrix is square, symmetric and loop-free, counts the selected vertices against $k$ , and checks every selected pair for adjacency. This is the NP-membership half of CLIQUE's NP-completeness, in the same format as KSat.ksat_ram_verifier.

Preamble

import Definitions.Def_WordRAM_Complexity_BitIO
import Definitions.Def_Clique_Language

set_option autoImplicit false

Formal statement

theorem CliqueNP.clique_ram_verifier :
    ∃ (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, CliqueNP.CLIQUE x ↔ ∃ y, V x y = true) := by sorry

Source

Richard M. Karp, Reducibility Among Combinatorial Problems, Complexity of Computer Computations, Plenum Press, pp. 85–103, 1972. https://doi.org/10.1007/978-1-4684-2001-2_9 . Main Theorem, problem 3 (CLIQUE), p. 94: membership in NP.

View graph