varDegree
plain-language theorem explainer
The definition counts the number of clauses in a CNF formula that contain a given variable index j. Researchers analyzing the J-cost Laplacian on the Boolean hypercube cite it to bound edge weights arising from single-bit flips. It is realized as a direct filter of the clause list by the containsVar predicate followed by a length computation.
Claim. Let $φ$ be a CNF formula over $n$ variables. For $j ∈ {0,…,n−1}$, the variable degree of $j$ in $φ$ is the number of clauses in $φ$ that contain variable $j$ in either polarity.
background
The J-Cost Laplacian module equips a CNF formula with a weighted graph on the Boolean hypercube whose edges correspond to single-bit flips and whose weights equal the absolute change in satJCost. A CNF formula is a list of clauses together with a matching variable count; each clause is itself a list of literals. The auxiliary predicate containsVar returns true precisely when a clause list contains the index j in any polarity.
proof idea
One-line wrapper that applies list filter using the containsVar predicate on the clauses field and returns the resulting length.
why it matters
This definition supplies the right-hand side of the bound jcostEdgeWeight_le_varDegree_prop, which states that flipping bit j changes the J-cost by at most the number of clauses containing j. It thereby quantifies the locality of cost changes under the Recognition Composition Law and supports non-negativity and kernel properties of the Laplacian quadratic form. The module records one remaining sorry in the zero-form implication chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.