jcostEdgeWeight
plain-language theorem explainer
The J-cost edge weight on the hypercube is the absolute difference in the number of unsatisfied clauses between an assignment and the result of flipping one chosen bit. Researchers modeling SAT instances via the spectrum of a discrete Laplacian would cite this quantity as the basic edge weight. It is introduced by a direct one-line definition that subtracts the two J-cost values and applies the absolute value.
Claim. For a CNF formula $φ$ on $n$ variables, an assignment $a$, and index $k$, the edge weight is $w(φ,a,k) := |J(φ,a) - J(φ,a^{(k)})|$, where $J(φ,a)$ counts the clauses of $φ$ left unsatisfied by $a$ and $a^{(k)}$ is the assignment differing from $a$ only at coordinate $k$.
background
The module constructs a weighted graph on the Boolean hypercube whose vertices are all assignments to the $n$ variables of a CNF formula. Edges connect assignments at Hamming distance one, and the weight of the edge obtained by flipping bit $k$ equals the absolute change in J-cost. The J-cost of an assignment equals the number of unsatisfied clauses; it vanishes precisely on satisfying assignments. The resulting quadratic form is $Q_J(x) = ½ ∑_a ∑_k w(a,flip(a,k)) (x(a)-x(flip(a,k)))^2$ (module doc).
proof idea
The definition is a direct one-line expression that subtracts the J-cost after the bit flip from the original J-cost and takes the absolute value. It invokes the upstream definitions of J-cost (length of the filtered list of unsatisfied clauses) and the single-bit-flip operation.
why it matters
This supplies the edge weights used by the CostConnected inductive relation, the jcostDegree sum, and the non-negativity, symmetry, and bounding theorems. It underpins the module's key results that the Laplacian quadratic form is positive semi-definite with constants in the kernel. It forms the discrete operator whose spectrum is intended to connect to the J-cost forcing steps in the Recognition Science chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.