theorem
proved
tactic proof
satJCost_zero_iff
show as:
view Lean formalization →
formal statement (Lean)
90theorem satJCost_zero_iff {n : ℕ} (f : CNFFormula n) (a : Assignment n) :
91 satJCost f a = 0 ↔ f.satisfiedBy a = true := by
proof body
Tactic-mode proof.
92 unfold satJCost CNFFormula.satisfiedBy
93 constructor
94 · intro h
95 have hlen : (f.clauses.filter (fun c => !c.satisfiedBy a)).length = 0 := by exact_mod_cast h
96 have hfilt : (f.clauses.filter (fun c => !c.satisfiedBy a)) = [] :=
97 List.eq_nil_iff_length_eq_zero.mpr hlen
98 rw [List.all_eq_true]
99 intro c hc
100 by_contra hc2
101 push_neg at hc2
102 have hmem : c ∈ f.clauses.filter (fun c => !c.satisfiedBy a) := by
103 simp only [List.mem_filter]
104 exact ⟨hc, by simp [hc2]⟩
105 rw [hfilt] at hmem
106 simp at hmem
107 · intro h
108 rw [List.all_eq_true] at h
109 have hfilt : (f.clauses.filter (fun c => !c.satisfiedBy a)) = [] := by
110 rw [List.filter_eq_nil_iff]
111 intro c hc
112 have hsat := h c hc
113 simp [hsat]
114 simp [hfilt]
115
116/-! ## Part 1: Satisfiable → Zero Cost (O(n) recognition steps) -/
117
118/-- **THEOREM**: For a satisfiable formula, R̂ finds zero-cost assignment in O(n) steps.
119 The constructive proof: if f.isSAT, then there exists a in 2^n candidates
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). -/