SAT: Boolean satisfiability

This module formalizes the language SAT and the semantic/encoding infrastructure used by the polynomial-time verifier.

Submodules

• Semantics — Lit, Clause, CNF, Assignment, and the pure-recursive CNF.eval. This is the audit surface: whatever the verifier actually computes will be proved equal to CNF.eval α φ.
• Encoding — CNF.encode : CNF → List Bool, the bit-level format the verifier parses.
• Language — language, the witness relation Witness, and the proofs mem_language_iff_witness / polyBalanced_witness.
• Verifier — executable decoding and checking for pair(z, α).
• VerifierTM — deterministic TM components for the machine-level verifier.
• GuessVerify — the proved SAT-specialized NTM composition for counter setup, bounded guessing, pair construction, and verifier simulation.
• Headline / CookLevin.Assembly — SAT ∈ NP and the final NP-completeness theorem.