jcostEdgeWeight
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.
claimFor 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 in Recognition Science
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.
scope and limits
- Does not prove any bounds, non-negativity, or symmetry of the weight.
- Does not construct the Laplacian matrix or compute its eigenvalues.
- Does not address paths or connectivity in the weighted graph.
- Does not depend on clause structure beyond the J-cost count.
formal statement (Lean)
56def jcostEdgeWeight {n : ℕ} (f : CNFFormula n) (a : Assignment n) (k : Fin n) : ℝ :=
proof body
Definition body.
57 |satJCost f a - satJCost f (flipBit a k)|
58