Prove that CLIQUE is NP-complete by reducing the existing 3-SAT language, KSat.KSAT 3, to it. An instance consists of a finite simple undirected graph and an input threshold; it asks whether the graph contains a clique of at least that size.
(https://prove2.me/theorems/d82e8682-c490-4742-a5e5-dd3a0b870b90). The construction specializes Karp’s SAT-to-CLIQUE reduction to 3-SAT.
theorem CliqueNP.clique_npComplete : CookLevin.NPComplete CliqueNP.CLIQUE := by sorry
The encoded CLIQUE language is NP-complete under the existing Cook–Levin definitions: it has a polynomial-time verifier with polynomially bounded accepted certificates, and every language in that NP class polynomial-time many-one reduces to it. The graph and requested clique size are both supplied as input.
The intended proof reduces the existing language KSat.KSAT 3 to CLIQUE, constructs the reduction and verifier with the shared WordRAM model, and reuses the proved polynomial backend. The published k-SAT theorem specialized to 3 supplies the intended NP-hardness prerequisite. The formal conclusion is unconditional and does not assume that prerequisite or a reduction as a hypothesis; it states NP-completeness without prescribing a particular proof.
No open leaves. Every sub-goal is proved or awaiting decomposition.