laplacian_form_nonneg
plain-language theorem explainer
The theorem proves non-negativity of the J-cost Laplacian quadratic form on the Boolean hypercube for any CNF formula. Researchers in recognition-based complexity or spectral methods on hypercubes would cite it to confirm the operator is positive semi-definite. The proof unfolds the quadratic form definition and applies non-negativity of the constant 1/2, of finite sums, of edge weights, and of squares.
Claim. Let φ be a CNF formula on n variables and let x map assignments (Fin n → Bool) to real numbers. Then the quadratic form Q_J(x) = (1/2) Σ_a Σ_k w(a, flip(a,k)) (x(a) - x(flip(a,k)))^2 satisfies Q_J(x) ≥ 0, where w denotes the J-cost edge weight.
background
The module equips each CNF formula φ on n variables with a weighted graph on the Boolean hypercube whose vertices are assignments. Edges connect assignments at Hamming distance 1 via single-bit flips, and the edge weight w(a, a') equals the absolute difference of satJCost values at those assignments. The associated Laplacian quadratic form is then Q_J(x) = (1/2) Σ_a Σ_k w(a, flip(a,k)) (x(a) - x(flip(a,k)))^2. This construction sits inside the broader Recognition Science treatment of complexity via J-cost functionals. The proof relies on the upstream result that every edge weight is non-negative, obtained directly from the absolute-value definition.
proof idea
The term-mode proof unfolds the definition of JCostLaplacianForm, factors the positive constant 1/2 via mul_nonneg, then applies Finset.sum_nonneg twice to the double sum. The inner summand is handled by mul_nonneg applied to jcostEdgeWeight_nonneg (which yields 0 ≤ w) and sq_nonneg (which yields 0 ≤ (difference)^2).
why it matters
This result supplies the PSD property required by the downstream JCostLaplacianCert bundle, which packages non-negativity, the constant kernel, and weight bounds for use in complexity certificates. It directly supports the module's claim that the J-cost Laplacian is a well-defined positive semi-definite operator on the hypercube, closing one of the listed key results in the J-cost Laplacian section.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.