moat_width_unsat

formal source

 182
 183/-- **THEOREM (Moat Width for UNSAT).**
 184    For an UNSAT formula, every assignment has J-cost ≥ 1. -/
 185theorem moat_width_unsat {n : ℕ} (f : CNFFormula n) (h : f.isUNSAT) :
 186    ∀ a : Assignment n, satJCost f a ≥ 1 :=
 187  unsat_cost_lower_bound f h
 188
 189/-- **THEOREM (Moat Width for SAT).**
 190    For a SAT formula, there exists a zero-cost assignment. -/
 191theorem moat_zero_sat {n : ℕ} (f : CNFFormula n) (h : f.isSAT) :
 192    ∃ a : Assignment n, satJCost f a = 0 :=
 193  sat_reaches_zero f h
 194
 195/-- The moat value equals 0 iff the formula is satisfiable. -/
 196theorem defect_moat_zero_iff_sat {n : ℕ} (f : CNFFormula n) :
 197    DefectMoat f = 0 ↔ f.isSAT := by
 198  unfold DefectMoat
 199  haveI := Classical.propDecidable f.isSAT
 200  by_cases h : f.isSAT
 201  · simp [h]
 202  · simp [h]
 203
 204/-! ## Part 4: Circuit Cannot Sense the Moat -/
 205
 206/-- **THEOREM (Circuit Cannot Verify Satisfiability Without Full Input).**
 207    For any fixed-view decoder over a proper subset M of variables (|M| < n),
 208    there exists a pair (b, R) such that the decoder cannot distinguish the hidden bit.
 209
 210    This is the BalancedParityHidden adversarial lower bound applied to circuits:
 211    any fixed-view decoder over a proper subset of variables can be fooled.
 212
 213    Consequence: no poly-size circuit (querying < n variables) can correctly
 214    decide satisfiability for all n-variable formulas. -/
 215theorem circuit_cannot_sense_moat