jcostDegree_nonneg
plain-language theorem explainer
The J-cost degree of an assignment for any CNF formula on the Boolean hypercube is non-negative. Analysts establishing spectral properties of the associated Laplacian quadratic form cite this basic graph fact. The argument is a direct one-line application of non-negativity to each term in the defining sum.
Claim. $0 ≤ ∑_{k=1}^n w(φ, σ, k)$, where $w(φ, σ, k)$ is the absolute difference in J-cost between assignment σ and the assignment obtained by flipping the k-th bit of σ, for any CNF formula φ on n variables.
background
The module equips each CNF formula φ with a weighted graph on the hypercube of all 2^n assignments. Vertices are functions from Fin n to Bool; edges connect assignments differing in exactly one coordinate. The edge weight between σ and its flip on coordinate k equals the absolute change in satJCost induced by that flip. jcostDegree(φ, σ) is defined as the sum of these n edge weights out of σ, i.e., the weighted degree of σ. The upstream result jcostEdgeWeight_nonneg states that each such weight is non-negative because it is an absolute value.
proof idea
The proof is a one-line term wrapper that applies Finset.sum_nonneg to the family of terms given by jcostEdgeWeight_nonneg f a k for each k. No further rewriting or case analysis is required.
why it matters
This non-negativity supplies the first step toward the positive semi-definiteness of the J-cost Laplacian quadratic form Q_J(x) = ½ Σ w(a, flip(a,k)) (x(a) - x(flip(a,k)))^2 recorded in the module header. It inherits the non-negativity built into the J-cost function of the multiplicative recognizer and therefore sits inside the Recognition Science cost framework. No downstream theorems yet depend on it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.