defect_moat_zero_iff_sat

formal source

 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
 222
 223/-- **THEOREM (Sublinear Circuit Cannot Universally Decode).**
 224    No circuit querying fewer than n inputs can universally decode
 225    the balanced-parity encoding. -/
 226theorem no_sublinear_universal_decoder