107theorem singletonHinge_edges {n : ℕ} (i j : Fin n) (w : ℝ) (hw : 0 ≤ w) : 108 (singletonHinge i j w hw).edges = [(i, j)] := by
proof body
Term-mode proof.
109 unfold singletonHinge; rfl 110 111/-! ## §3. The cubic deficit functional via pattern matching -/ 112 113/-- Deficit at a hinge: if the hinge carries a single edge `(i, j)`, 114 return `(ε_i − ε_j)²`; otherwise return 0. -/
used by (2)
From the project-wide theorem graph. These declarations reference this one in their body.