139theorem unsat_positive_jcost {n : ℕ} (f : CNFFormula n) (h : f.isUNSAT) : 140 ∀ a : Assignment n, satJCost f a > 0 := by
proof body
Term-mode proof.
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). -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.