sat_reaches_zero

formal source

 120    with satJCost f a = 0. R̂ evaluates this assignment directly.
 121
 122    Recognition time = n (one variable at a time, each step costs at most 1 tick). -/
 123theorem sat_reaches_zero {n : ℕ} (f : CNFFormula n) (h : f.isSAT) :
 124    ∃ a : Assignment n, satJCost f a = 0 := by
 125  obtain ⟨a, ha⟩ := h
 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