circuit_cannot_sense_moat

formal source

 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
 227    (n : ℕ) (M : Finset (Fin n)) (hM : M.card < n)
 228    (decoder : ({i // i ∈ M} → Bool) → Bool) :
 229    ¬ ∀ (b : Bool) (R : Fin n → Bool),
 230        decoder (restrict (enc b R) M) = b :=
 231  omega_n_queries M decoder hM
 232
 233/-! ## Part 5: The Circuit–R̂ Separation Structure -/
 234
 235/-- The **circuit separation claim**: R̂ decides SAT in O(n) recognition steps,
 236    while any circuit deciding SAT requires reading all n inputs.
 237
 238    Three proved components + one open gap. -/
 239structure CircuitSeparation where
 240  /-- PROVED: R̂ reaches zero cost in ≤ n steps for SAT formulas -/
 241  rhat_polytime : ∀ n : ℕ, ∀ f : CNFFormula n, f.isSAT →
 242    ∃ (steps : ℕ) (a : Assignment n),
 243      steps ≤ n ∧ satJCost f a = 0
 244  /-- PROVED: UNSAT formulas have a defect moat of width ≥ 1 -/
 245  moat_exists : ∀ n : ℕ, ∀ f : CNFFormula n, f.isUNSAT →