moat_zero_sat

formal source

 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
 216    (n : ℕ) (_hn : 0 < n)
 217    (M : Finset (Fin n)) (hM : M.card < n)
 218    (decoder : ({i // i ∈ M} → Bool) → Bool) :
 219    ∃ (b : Bool) (R : Fin n → Bool),
 220      decoder (restrict (enc b R) M) ≠ b :=
 221  adversarial_failure M decoder