196theorem defect_moat_zero_iff_sat {n : ℕ} (f : CNFFormula n) : 197 DefectMoat f = 0 ↔ f.isSAT := by
proof body
Term-mode proof.
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. -/
depends on (21)
Lean names referenced from this declaration's body.