laplacian_form_zero_imp
plain-language theorem explainer
If the J-cost Laplacian quadratic form Q_J(x) vanishes on the Boolean hypercube, then x must take identical values on any pair of assignments joined by a positive-weight edge. Researchers analyzing discrete harmonic functions or the kernel of weighted graph Laplacians on hypercubes would cite the result when characterizing level sets of the cost landscape. The argument first proves the double sum of non-negative terms equals zero, then isolates the relevant summand via repeated application of sum_eq_zero_iff_of_nonneg and mul_eq_zero.
Claim. Let $Q_J(x) = ½ ∑_a ∑_k w(f,a,k) (x(a) - x(flip(a,k)))^2$ denote the quadratic form associated to a CNF formula $f$. Then $Q_J(x) = 0$ implies $x(a) = x(flip(a,k))$ whenever the edge weight $w(f,a,k) > 0$.
background
The module equips the Boolean hypercube with a weighted graph whose vertices are assignments (Fin n → Bool) and whose edges connect Hamming-distance-1 neighbors via single-bit flips. Edge weight w(a, flip(a,k)) is defined as the absolute difference |satJCost(f,a) - satJCost(f, flip(a,k))|. The associated quadratic form is exactly JCostLaplacianForm, which expands to ½ times the double sum of w times squared differences. The local setting is the study of non-negative quadratic forms on this graph, with prior results establishing non-negativity of the form and that constant functions lie in its kernel. Upstream lemmas supply flipBit (the single-bit toggle), jcostEdgeWeight (the absolute satJCost difference), and its non-negativity theorem.
proof idea
Unfold JCostLaplacianForm inside the hypothesis to obtain a double sum S equal to zero. Non-negativity of every summand (via jcostEdgeWeight_nonneg and sq_nonneg) yields S ≥ 0, hence S = 0 by nlinarith. Apply sum_eq_zero_iff_of_nonneg to the outer sum over a to conclude that the inner sum over k for the given a vanishes. Repeat the same extraction on the inner sum to isolate the single term w(a,k) (x(a) - x(flip(a,k)))^2 = 0. Since w(a,k) > 0, mul_eq_zero forces the squared difference to vanish, and sq_eq_zero_iff recovers the desired equality.
why it matters
The result supplies the converse direction needed to characterize the kernel of the J-cost Laplacian: zero energy forces constancy along positive-weight edges, complementing the already-proved facts that the form is PSD and that constants achieve zero. It therefore supports connectivity arguments in the cost landscape, directly feeding the module's stated goal of analyzing harmonic functions on the weighted hypercube. The surrounding module lists this implication among its key results alongside non-negativity and the bound on edge weights by clause count.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.