unsat_positive_jcost

formal source

 136
 137/-- For an unsatisfiable formula, every assignment has J-cost > 0.
 138    This means the J-cost landscape has no zero-cost point = topological obstruction. -/
 139theorem unsat_positive_jcost {n : ℕ} (f : CNFFormula n) (h : f.isUNSAT) :
 140    ∀ a : Assignment n, satJCost f a > 0 := by
 141  intro a
 142  have := h a
 143  by_contra hle
 144  push_neg at hle
 145  have heq : satJCost f a = 0 := le_antisymm hle (satJCost_nonneg f a)
 146  rw [satJCost_zero_iff] at heq
 147  exact absurd heq (by simp [this])
 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))