pith. machine review for the scientific record. sign in
theorem proved term proof

jcostDegree_nonneg

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 135theorem jcostDegree_nonneg {n : ℕ} (f : CNFFormula n) (a : Assignment n) :
 136    0 ≤ jcostDegree f a :=

proof body

Term-mode proof.

 137  Finset.sum_nonneg (fun k _ => jcostEdgeWeight_nonneg f a k)
 138
 139/-! ## J-Cost Laplacian Quadratic Form -/
 140
 141/-- The J-cost Laplacian quadratic form on (Fin n → Bool) → ℝ.
 142    Q_J(x) = ½ Σ_a Σ_k w(a, flip(a,k)) · (x(a) - x(flip(a,k)))² -/

depends on (8)

Lean names referenced from this declaration's body.