 176/-! ## Part 3: The Defect Moat -/
 177
 178/-- The **Defect Moat** for a formula f: 0 if SAT, 1 if UNSAT. -/
 179noncomputable def DefectMoat {n : ℕ} (f : CNFFormula n) : ℕ :=
 180  haveI := Classical.propDecidable f.isSAT
 181  if f.isSAT then 0 else 1
 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

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.