def NPCompleteness.IsCoNPHard {Γ : Type} (B : Set (List Γ)) : Prop

A language B is coNP-hard if every language A ∈ coNP polynomial-time reduces to B. Analogous to the NP-hardness definition ∀ A ∈ NP, A ≤_P B from the textbook, but for the class coNP.

noncomputable def NPCompleteness.BoolFormula.maxVarSucc (φ : BoolFormula) : ℕ

One plus the largest variable index appearing in φ. This gives an upper bound m such that every variable of φ has index < m.

theorem NPCompleteness.BoolFormula.eval_eq_of_agree_on_vars {σ₁ σ₂ : BoolAssignment} (φ : BoolFormula) (h : ∀ i ∈ φ.vars, σ₁ i = σ₂ i) : eval σ₁ φ = eval σ₂ φ

The truth value φ.eval σ depends only on the values of σ on the variables that actually occur in φ. If two assignments agree on φ.vars they yield the same evaluation.

theorem NPCompleteness.BoolFormula.countSat_eq_zero_of_not_satisfiable {φ : BoolFormula} (hunsat : ¬φ.Satisfiable) : φ.countSat = 0

If φ is unsatisfiable then its #SAT count is zero. One direction of the equivalence between satisfiability and positive #SAT count.

theorem NPCompleteness.BoolFormula.not_satisfiable_of_countSat_eq_zero {φ : BoolFormula} (hcount : φ.countSat = 0) : ¬φ.Satisfiable

Converse of countSat_eq_zero_of_not_satisfiable: if φ has zero satisfying assignments then φ is unsatisfiable.

def NPCompleteness.BoolFormula.IsTautology (φ : BoolFormula) : Prop

A Boolean formula φ is a tautology iff φ.eval σ = true for every assignment σ.

def NPCompleteness.TAUTOLOGY : Set BoolFormula

The language TAUTOLOGY = {⟨φ⟩ | φ is a tautology}, the canonical coNP-complete language.

structure NPCompleteness.SharpSATEncoding : Type

A simple encoding of #SAT instances ⟨φ, k⟩ as lists of Boolean formulas, specifically tailored for the coNP-hardness reduction. Only one round-trip law is required: decode (encode p) = some p.

• encode : BoolFormula × ℕ → List BoolFormula
• decode : List BoolFormula → Option (BoolFormula × ℕ)
• decode_encode (p : BoolFormula × ℕ) : self.decode (self.encode p) = some p

def NPCompleteness.SharpSATLang (enc : SharpSATEncoding) : Set (List BoolFormula)

The #SAT language as a set of encoded instances over the alphabet BoolFormula: w is accepted iff it decodes to a pair ⟨φ, k⟩ with k = countSat φ.

theorem NPCompleteness.PolyReducible.compl_left {Γ : Type} {A B : Set (List Γ)} (h : TuringMachine.PolyReducible Aᶜ B) : TuringMachine.PolyReducible A Bᶜ

If Aᶜ ≤_P B then A ≤_P Bᶜ (the same reduction function works in both directions, since w ∈ Aᶜ ↔ f(w) ∈ B is equivalent to w ∈ A ↔ f(w) ∈ Bᶜ).

noncomputable def NPCompleteness.unsatToSharpSAT (enc : SharpSATEncoding) (w : List BoolFormula) : List BoolFormula

The reduction UNSAT ≤_P #SAT: given an input encoding a single Boolean formula φ (the natural input format for UNSAT), output the #SAT encoding of ⟨φ, 0⟩. Malformed inputs are mapped to the encoding of ⟨false, 0⟩ (which is trivially a true #SAT instance, but the original input is also not in UNSAT under this convention).

theorem NPCompleteness.BoolFormula.not_satisfiable_falseConst : ¬falseConst.Satisfiable

The constant false formula is unsatisfiable.

theorem NPCompleteness.BoolFormula.countSat_falseConst : falseConst.countSat = 0

The constant false formula has zero satisfying assignments.

theorem NPCompleteness.unsatToSharpSAT_correct (enc : SharpSATEncoding) (w : List BoolFormula) : w ∈ SATLangᶜ ↔ unsatToSharpSAT enc w ∈ SharpSATLang enc

Correctness of the unsatToSharpSAT reduction: w ∈ SATᶜ iff unsatToSharpSAT w ∈ #SAT. Concretely, for a single-formula input [φ], this says φ is unsatisfiable iff countSat φ = 0.

theorem NPCompleteness.unsatToSharpSAT_polyTime (enc : SharpSATEncoding) : TuringMachine.IsPolyTimeComputableFunction (unsatToSharpSAT enc)

The reduction function unsatToSharpSAT is computable in polynomial time: encoding ⟨φ, 0⟩ from φ takes polynomial work in |φ|.

theorem NPCompleteness.unsatLang_polyReducible_sharpSATLang (enc : SharpSATEncoding) : TuringMachine.PolyReducible SATLangᶜ (SharpSATLang enc)

UNSAT ≤_P #SAT: the language SATᶜ (the complement of SAT) polynomial-time reduces to #SAT via unsatToSharpSAT.

theorem NPCompleteness.sharpSATLang_coNP_hard (enc : SharpSATEncoding) : IsCoNPHard (SharpSATLang enc)

#SAT is coNP-hard. For every A ∈ coNP, A ≤_P #SAT. The proof chains together: A ∈ coNP ⇒ Aᶜ ∈ NP ⇒ Aᶜ ≤_P SAT (Cook–Levin) ⇒ A ≤_P SATᶜ (PolyReducible.compl_left) ⇒ A ≤_P #SAT (via the UNSAT ≤_P #SAT reduction).