SAT: Language and Witness Relation

This file defines the formal SAT language language and the NP witness relation Witness, and proves the two core bridge theorems:

• mem_language_iff_witness — z ∈ language ↔ ∃ α, Witness z α (a CNF is satisfiable iff it admits a short satisfying assignment)
• polyBalanced_witness — witness length is bounded by |z| + 1 (satisfying assignments can always be truncated to length φ.maxVar + 1, and φ.maxVar ≤ |φ.encode| from the unary encoding)

These are the semantic and witness-length ingredients used by both routes to SAT ∈ NP. The executable verifier is specified in SAT/Verifier.lean, its polynomial-time TM implementation is proved in SAT/VerifierTM.lean, and the SAT-specialized guess-and-verify construction is assembled into the unconditional headline theorem in SAT/Headline.lean.

def Complexity.SAT.language : Language

The SAT language. A bitstring z is in language iff it encodes some satisfiable CNF formula.

Note: encode is injective on well-formed CNFs, but we don't need injectivity for any of the downstream theorems — we only need "there exists some φ …".

Equations

• Complexity.SAT.language = {z : List Bool | ∃ (φ : Complexity.SAT.CNF), z = φ.encode ∧ φ.Satisfiable}

def Complexity.SAT.Witness (z α : List Bool) : Prop

The SAT witness relation. Witness z α holds when z encodes some CNF φ, α is a bit-string of length at most |z| + 1, and α satisfies φ.

The |z| + 1 length bound is what gives PolyBalanced Witness. It's always achievable because any satisfying assignment can be truncated to length φ.maxVar + 1 ≤ |φ.encode| + 1 = |z| + 1 (satisfiable_iff_short_witness + CNF.maxVar_le_encode_length).

Equations

• Complexity.SAT.Witness z α = ∃ (φ : Complexity.SAT.CNF), z = φ.encode ∧ α.length ≤ z.length + 1 ∧ Complexity.SAT.CNF.eval α φ = true

theorem Complexity.SAT.mem_language_iff_witness (z : List Bool) : z ∈ language ↔ ∃ (α : List Bool), Witness z α

Witness characterization of language. A string z is in language iff there exists a witness α with Witness z α.

The forward direction uses CNF.satisfiable_iff_short_witness to produce a truncated witness, then applies CNF.maxVar_le_encode_length to bound its length by |z| + 1.

The reverse direction is immediate: any α satisfying φ proves φ.Satisfiable.

theorem Complexity.SAT.polyBalanced_witness : PolyBalanced Witness

Short-witness property for SAT. The witness relation Witness is polynomially balanced: every valid witness has length at most |z| + 1, which is bounded by the degree-1 polynomial X + 1.

This is the key structural fact that makes SAT a candidate for NP: we never need to guess more than linearly many bits.

theorem Complexity.SAT.witness_mem_FNP_of_verifier (h : pairLang Witness ∈ P) : Witness ∈ FNP

SAT is in FNP modulo the verifier. If the verifier's pair language is in P, then Witness is an FNP relation — and hence a candidate NP witness relation for language. The only nontrivial content is polyBalanced_witness.

theorem Complexity.SAT.language_mem_NP_of_verifier (hwitness : NP.WitnessNTMConstruction) (h : pairLang Witness ∈ P) : language ∈ NP

SAT is in NP modulo the verifier and generic guess-and-verify construction. If the verifier's pair language is in P and the generic FNP-witness to NP construction has been built, then language ∈ NP.

Combines witness_mem_FNP_of_verifier (SAT's FNP witness relation) with the generic NP witness theorem mem_NP_of_FNP_witness. This theorem deliberately retains the generic construction as an explicit hypothesis; the SAT-specific unconditional route is provided by SAT/Headline.lean.