unsat_cost_lower_bound

formal source

 148
 149/-- The topological obstruction: for UNSAT formulas, the minimum J-cost over
 150    all assignments is positive (bounded away from zero). -/
 151theorem unsat_cost_lower_bound {n : ℕ} (f : CNFFormula n) (h : f.isUNSAT) :
 152    ∀ a : Assignment n, satJCost f a ≥ 1 := by
 153  intro a
 154  have hpos := unsat_positive_jcost f h a
 155  -- satJCost is a natural-number length cast to ℝ; > 0 implies ≥ 1
 156  have hnat : 1 ≤ (f.clauses.filter (fun c => !c.satisfiedBy a)).length := by
 157    have : 0 < (f.clauses.filter (fun c => !c.satisfiedBy a)).length := by
 158      unfold satJCost at hpos; exact_mod_cast hpos
 159    omega
 160  unfold satJCost
 161  exact_mod_cast hnat
 162
 163/-! ## Part 3: Separation via BalancedParityHidden -/
 164
 165/-- The adversarial failure theorem (from BalancedParityHidden):
 166    any fixed-view decoder on a proper subset of variables can be fooled.
 167    This is the RS version of the natural proof barrier: no local property
 168    of the formula can certify unsatisfiability. -/
 169theorem rs_adversarial_lower_bound (n : ℕ) (M : Finset (Fin n))
 170    (g : ({i // i ∈ M} → Bool) → Bool) :
 171    ∃ (b : Bool) (R : Fin n → Bool),
 172      g (BalancedParityHidden.restrict (BalancedParityHidden.enc b R) M) ≠ b :=
 173  BalancedParityHidden.adversarial_failure M g
 174
 175/-- The R̂ certifier is "non-natural" in the sense that it uses the entire
 176    assignment at once (global, not local). The adversarial failure shows
 177    that any LOCAL certifier fails, while R̂'s global evaluation succeeds. -/
 178theorem rhat_is_non_natural (n : ℕ) :
 179    ¬ ∃ (M : Finset (Fin n)),
 180      (M.card < n) ∧
 181      ∀ (f : CNFFormula n) (_ : f.isSAT),