jcostEdgeWeight_le_varDegree_prop
The declaration defines the proposition that the J-cost edge weight for flipping bit j is at most the variable degree of j in a CNF formula. Analysts of the J-cost Laplacian on the Boolean hypercube would cite this bound when controlling edge contributions to the quadratic form. The definition follows immediately from the observation that only clauses containing j can alter their satisfaction status under the flip.
claimLet $f$ be a CNF formula on $n$ variables, $a$ an assignment to those variables, and $j$ a variable index. The J-cost edge weight $|satJCost(f,a) - satJCost(f, flipBit(a,j))|$ is at most the number of clauses in $f$ that contain variable $j$.
background
The J-Cost Laplacian module equips the Boolean hypercube with edge weights equal to the absolute change in satJCost under a single bit flip. The upstream definition jcostEdgeWeight computes exactly this difference: |satJCost f a - satJCost f (flipBit a k)|. The companion definition varDegree counts the clauses containing a given index j by filtering the clause list with containsVar and taking the length.
proof idea
This is a direct definition of the bounding proposition as the stated inequality. The accompanying doc-comment invokes the list-filter symmetric difference counting lemma (predicates agreeing outside a subset S satisfy |filter(P).length - filter(Q).length| ≤ S.length) to justify why the cost difference cannot exceed the number of clauses containing j.
why it matters in Recognition Science
The bound limits individual edge weights in the J-cost graph by variable degrees, supporting control of the quadratic form Q_J. It aligns with the module's listed key results on non-negativity and edge-weight bounds. Within Recognition Science it supplies a concrete complexity estimate inside the SAT-encoding layer, though no direct tie to the T0-T8 forcing chain or RCL appears here.
scope and limits
- Does not prove the inequality holds; it only names the proposition.
- Does not supply the list-filter symmetric difference counting lemma.
- Does not extend to formulas outside CNF or to other cost functions.
- Does not bound the full Laplacian spectrum or establish positive semi-definiteness.
formal statement (Lean)
126def jcostEdgeWeight_le_varDegree_prop {n : ℕ} (f : CNFFormula n) (a : Assignment n)
127 (j : Fin n) : Prop :=
proof body
Definition body.
128 jcostEdgeWeight f a j ≤ varDegree f j
129
130/-! ## J-Cost Weighted Degree -/
131