laplacian_form_const_zero
plain-language theorem explainer
The theorem shows that constant functions lie in the kernel of the J-cost Laplacian quadratic form for any CNF formula on n variables. Researchers examining the spectral properties of the weighted hypercube graph induced by J-cost differences would cite this kernel membership. The proof is a one-line wrapper that unfolds the quadratic form definition and reduces the resulting expression by numerical simplification.
Claim. For any natural number $n$, any CNF formula $f$ on $n$ variables, and any real number $c$, the J-cost Laplacian quadratic form $Q_J$ evaluated at the constant function with value $c$ equals zero.
background
The J-cost Laplacian quadratic form on the Boolean hypercube is defined by $Q_J(x) = (1/2) sum over assignments a and bit positions k of the edge weight w(a, flip(a,k)) times (x(a) - x(flip(a,k)))^2. Edge weights are given by the absolute difference in satJCost between neighboring assignments. The module sets this construction in the context of CNF formulas encoded as lists of clauses, with the quadratic form serving as a measure of variation under single-bit flips weighted by J-cost changes.
proof idea
The proof is a one-line wrapper that unfolds the definition of the J-cost Laplacian form and applies norm_num to obtain the zero identity.
why it matters
This result supplies the const_kernel component of the JCostLaplacianCert record, which aggregates the non-negativity, kernel, and weight properties of the form. It completes one of the three key results enumerated in the module documentation for the J-cost Laplacian. The kernel property is the standard algebraic signature that constants produce zero quadratic form, aligning with the Laplacian structure used downstream in complexity certificates.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.