theorem
proved
tactic proof
laplacian_form_zero_imp
show as:
view Lean formalization →
formal statement (Lean)
166theorem laplacian_form_zero_imp {n : ℕ} (f : CNFFormula n) (x : (Fin n → Bool) → ℝ)
167 (hzero : JCostLaplacianForm f x = 0) :
168 ∀ (a : Fin n → Bool) (k : Fin n),
169 0 < jcostEdgeWeight f a k → x a = x (flipBit a k) := by
proof body
Tactic-mode proof.
170 intro a k hpos
171 unfold JCostLaplacianForm at hzero
172 -- Step 1: ½ · S = 0 with S ≥ 0 implies S = 0
173 have hS_nonneg : 0 ≤ Finset.univ.sum (fun a : Fin n → Bool =>
174 Finset.univ.sum (fun k : Fin n =>
175 jcostEdgeWeight f a k * (x a - x (flipBit a k))^2)) := by
176 apply Finset.sum_nonneg; intro a' _
177 apply Finset.sum_nonneg; intro k' _
178 exact mul_nonneg (jcostEdgeWeight_nonneg f a' k') (sq_nonneg _)
179 have hS_zero : Finset.univ.sum (fun a : Fin n → Bool =>
180 Finset.univ.sum (fun k : Fin n =>
181 jcostEdgeWeight f a k * (x a - x (flipBit a k))^2)) = 0 := by
182 nlinarith [hS_nonneg]
183 -- Step 2: outer sum = 0 with all inner sums ≥ 0 → the a-th inner sum = 0
184 have hInner_nonneg : ∀ a' : Fin n → Bool, 0 ≤ Finset.univ.sum (fun k' : Fin n =>
185 jcostEdgeWeight f a' k' * (x a' - x (flipBit a' k'))^2) := by
186 intro a'; apply Finset.sum_nonneg; intro k' _
187 exact mul_nonneg (jcostEdgeWeight_nonneg f a' k') (sq_nonneg _)
188 have hInner_zero := Finset.sum_eq_zero_iff_of_nonneg (fun a' _ => hInner_nonneg a')
189 |>.mp hS_zero a (Finset.mem_univ a)
190 -- Step 3: inner sum = 0 with all terms ≥ 0 → the k-th term = 0
191 have hTerm_nonneg : ∀ k' : Fin n, 0 ≤
192 jcostEdgeWeight f a k' * (x a - x (flipBit a k'))^2 := by
193 intro k'; exact mul_nonneg (jcostEdgeWeight_nonneg f a k') (sq_nonneg _)
194 have hTerm_zero := Finset.sum_eq_zero_iff_of_nonneg (fun k' _ => hTerm_nonneg k')
195 |>.mp hInner_zero k (Finset.mem_univ k)
196 -- Step 4: w · d² = 0 with w > 0 → d² = 0 → d = 0
197 have hd_sq_zero : (x a - x (flipBit a k))^2 = 0 := by
198 rcases mul_eq_zero.mp hTerm_zero with hw | hd
199 · linarith
200 · exact hd
201 have hd_zero : x a - x (flipBit a k) = 0 := by
202 exact_mod_cast sq_eq_zero_iff.mp hd_sq_zero
203 linarith
204
205/-! ## Cost Landscape Connectivity -/
206
207/-- Two assignments are cost-connected if there is a path through positive-weight edges. -/