Chapter 34 — NP-Completeness

Chapter 34 formalizes the textbook complexity framework and the advertised NP-completeness chain through Sections 34.1--34.5. Machine-level polynomial time is expressed with Mathlib's Turing.TM2ComputableInPolyTime and explicit Polynomial ℕ bounds.

Coverage status

Status: main-proof-complete. The selected textbook theorem boundary is kernel-checked end to end. This status is about the public mathematical claims and their honest serialized decision problems; it does not claim that every exercise or every possible low-level implementation refinement has been formalized.

34.1 Polynomial time

The chapter defines languages, polynomial-time computable functions and deciders, and ClassP. It proves composition of polynomial-time TM2 machines and closure of P under complement, union, and intersection.

34.2 Polynomial-time verification

Certificate/input pairing, polynomial-size certificates, PolyTimeVerifiable, and ClassNP provide the verifier model. The formalized Theorem 34.2 is ClassP_subset_ClassNP.

34.3 NP-completeness and reducibility

PolyTimeReducible, NPHard, and NPComplete supply the public reduction interface. Polynomial-time reducibility is transitive, so hardness can be transported along the concrete reduction chain.

34.4 Cook--Levin and the first NP-complete problems

The Cook--Levin development constructs the complete bounded computation tableau as a general circuit, proves its exact satisfiability semantics, and establishes polynomial bounds for gates, inputs, complete encoding length, and generator runtime. A fixed TM2 computes the exact map from the original raw input. The public results include:

• Turing.CookLevin.cookLevin_theorem for every language in NP;

• Turing.CookLevin.generalCircuitSAT_npComplete;

• the total direct bridge generalCircuitSAT_reducible_to_SAT;

• the concrete SAT-to-3-CNF-SAT and 3-CNF-SAT-to-CLIQUE reductions; and

• CLIQUE_npComplete for the honest serialized graph-plus-k language.

The standalone SAT and 3-CNF-SAT layers additionally provide total serialized assignment checkers, exact malformed-input semantics, and linear bounded- certificate characterizations. Lowering those two checkers to fixed TM2s and packaging their direct NP-completeness wrappers remains an optional refinement.

The supporting compiler modules are proof-level constructions: they turn a fixed verifier and raw input into the circuit encoding required by the reduction. They are part of the concrete polynomial-time proof, not a compiler chapter or an external implementation detour.

34.5 Selected NP-complete problems

The selected textbook chain is closed at both typed semantic and strict raw serialization layers:

• CLIQUE reduces to VERTEX-COVER;

• VERTEX-COVER reduces to HAM-CYCLE;

• HAM-CYCLE reduces to decision-TSP; and

• 3-CNF-SAT reduces to SUBSET-SUM by carry-free column packing.

Each public target has an honest raw language, bounded certificate semantics, a fixed polynomial-time verifier, a total fixed polynomial-time reduction machine, and an exact all-input semantic bridge. The final wrappers are VERTEXCOVER_npComplete, HAMCYCLE_npComplete, TSP_npComplete, and SUBSETSUM_npComplete.

Deliberate boundary

The P-versus-NP question is out of scope. Fixed-machine realizations of the standalone SAT/3-CNF-SAT checkers and direct concrete deciders for the empty and universal languages remain optional refinements, not Chapter 34 closure gaps. The canonical fourth-edition summary is CLRSLean.FourthEdition.Chapter_34.