Chapter 34 — NP-Completeness

Chapter 34 of CLRS covers NP-completeness: the complexity classes P and NP, polynomial-time reducibility, and NP-completeness.

This chapter formalizes the polynomial-time framework and the represented NP-completeness reductions through Section 34.4. It is built on Mathlib's Turing.TM2ComputableInPolyTime (machine-level polynomial-time computability with Polynomial ℕ time bounds).

Sections

34.1 Polynomial Time

• CLRS.Chapter34.Language — a set of strings over an alphabet

• CLRS.Chapter34.PolyTimeComputable — a function computed by a TM2 machine in time bounded by a polynomial in the input length

• CLRS.Chapter34.PolyTimeDecidable — a language decided by a polynomial-time decision function

• CLRS.Chapter34.ClassP — the class of polynomial-time decidable languages

34.2 Polynomial-Time Verification

• CLRS.Chapter34.pairEncoding — encode a certificate/input pair as one string

• CLRS.Chapter34.PolyTimeVerifiable — a language verifiable by a polynomial-time verifier with polynomial-size certificates

• CLRS.Chapter34.ClassNP — the class of polynomially verifiable languages

34.3 NP-Completeness and Reducibility

• CLRS.Chapter34.PolyTimeReducible — L₁ ≤_P L₂, polynomial-time reducibility

• CLRS.Chapter34.NPHard / NPComplete — the NP-hard / NP-complete classes

• CLRS.Chapter34.ClassNPC — the class of NP-complete languages

Status: partial — the complete framework (languages, polytime, class P, class NP, reducibility, NP-hard/NP-complete) is defined, and the theorem layer is complete: composition, P ⊆ NP, transitivity of ≤_P, and the closure of ClassP under complement, union, and intersection. Section 34.4 includes the concrete CIRCUIT-SAT → SAT and SAT → at-most-three-literal 3-CNF-SAT reductions, plus a reduction from 3-CNF-SAT to its specialized occurrence-graph clique language. The concrete Turing.TM3CNF.sat_reducible_to_threeCNFSat machine theorem is sealed by the Chapter 34 public interface. The bounded-builder kernel now includes verified scan/copy, symbol-local bounded-loop, and row-major nested-loop macros, each with canonical exact independent and compiled runs; their costs are respectively 3n + 3, 2n + L + 3, and 2n² + 5n + L + 4. The Cook--Levin foundation now also extracts finite reachable alphabets for fixed bundled machines, encodes canonical bounded configurations without assuming the full work alphabets are finite, proves exact-horizon stuttering equivalence, and establishes a uniform stack-height bound that counts every push along a bundled statement path. Canonical row validity is now circuitized with exact decoding semantics and an exact gate cost affine in the height bound. Verified one-step workspace bridges now widen and narrow row bundles with exact gate costs, overflow-fit semantics, and successful-decoding preservation. Widening now exposes its exact two-gate Boolean constant pool for downstream reuse. The circuit kernel also provides finite-family mux and streaming equality with exact respective costs 3n + 1 and 6n + 1; canonical row flattening lifts these operations to whole configuration bundles with exact costs 3w + 1 and 6w + 1, where the row width w denotes cfgBitCount tm H; typed stack views meanwhile support zero-gate functional replacement. Pure fixed-width stack push, peek, and pop on raw Boolean bundles now have exact coordinate laws, supported-head codec round trips, raw one-hot preservation under an explicit capacity premise, and a full-stack overflow theorem. These primitives do not yet prove wire-level transition correctness by themselves. Canonical Boolean stack encodings now carry exact list semantics: push is cons under capacity, peek is head, pop is tail plus the old head, and every successful whole-row evaluation projects to the corresponding represented machine stack. Wire-level wrappers reuse a shared Boolean pool, keep push/peek zero-gate, give positive-width pop exact one-OR cost, and compute capacity with one NOT, while preserving complete-row frames. The structural compiler compileStmt covers all seven TM2.Stmt constructors—halt, goto, load, push, peek, pop, and branch—using fixed finite truth tables. Its complete-row evaluation theorem is exactly TM2.stepAux under explicit prefix capacity, and it publishes both an exact structural gate delta and a fixed-machine/statement affine emitted-gate bound. Finite program-label dispatch now selects statements compiled against the same source row, preserves the reserved-none stuttering case, and publishes exact complete-row semantics and gate cost. The local transitionCircuit widens into the one-step workspace, dispatches, narrows under its internally checked fit bit, compares the complete public target row, and accepts exactly stutterStep tm c; its result records the exact total gate delta and a fixed-machine affine emitted-gate bound. Canonical row validity, finite-label dispatch, and local transition construction now publish height-independent coefficients, while finished validity and transition wrappers are proved well formed and evaluation preserving. The fresh-layout layer now allocates consecutive nonaliasing rows at any external input offset. freshTransitionCircuitAt_complete_nat preserves an arbitrary base assignment outside the two row intervals, while freshTransitionCircuit_complete constructs the finite assignment used by general-circuit satisfiability. Exact boundary constraints now compare the complete first/last row against canonical initList/haltList targets, reject oversized or unsupported concrete targets with a real false wire, and expose a symbolic-input-stack initial form for certificate-linked assembly. Whole-tableau circuitization now allocates every verifier row, checks canonical validity and all adjacent stuttering steps, enforces bounded certificate/input shape and exact endpoint rows, and closes a well-formed general circuit. Its satisfiability is equivalent to language membership and its gate count, input count, and complete unary encoding length are controlled by explicit fixed-verifier polynomials. The exported function-level cookLevinMap preserves language membership exactly and has a proved output- length bound. GeneralCircuitSAT also has an executable finite Boolean- certificate checker whose bounded-certificate semantics is exact. A concrete TM2 computes that checker Boolean on every input; every successful, rejecting, and malformed route is covered by one explicit quartic step polynomial. Consequently GeneralCircuitSAT is now proved polynomially verifiable and a member of ClassNP. The concrete polynomial-time Cook--Levin generator TM2 and the resulting hardness/NP-completeness wrappers remain downstream. A general graph-plus-k CLIQUE target and Section 34.5 remain unrepresented.

Theorem layer:

• Turing.TM2ComputableInPolyTime.comp (via Turing.TM2Comp.comp_scratch): composition of polynomial-time machines is polynomial-time (Mathlib leaves this as proof_wanted; closed here). Unlocks P ⊆ NP and the transitivity of PolyTimeReducible.

• PolyTimeDecidable.compl / ClassP_compl: P is closed under complement.

• PolyTimeDecidable.union / ClassP_union and PolyTimeDecidable.inter / ClassP_inter: P is closed under union and intersection, via the AND/OR machine Turing.TM2AndOr.andOrMachine (which duplicates the input, runs both deciders, and combines with AND/OR).

• ClassP_subset_ClassNP: P ⊆ NP (Theorem 34.2).

Open problems (whether P = NP) and the Section 34.5 reductions such as VERTEX-COVER, HAM-CYCLE, and SUBSET-SUM are intentionally out of scope for now.