sat_recognition_time_bound

formal source

 126  exact ⟨a, (satJCost_zero_iff f a).mpr ha⟩
 127
 128/-- The recognition time for a satisfiable formula is ≤ n (variable count). -/
 129theorem sat_recognition_time_bound {n : ℕ} (f : CNFFormula n) (h : f.isSAT) :
 130    ∃ (steps : ℕ) (a : Assignment n),
 131      steps ≤ n ∧ satJCost f a = 0 := by
 132  obtain ⟨a, ha⟩ := sat_reaches_zero f h
 133  exact ⟨n, a, le_refl _, ha⟩
 134
 135/-! ## Part 2: Unsatisfiable → Topological Obstruction -/
 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