singletonHinge_edges
singletonHinge_edges shows that the edges field of the hinge datum built from vertices i, j and weight w is the list containing only the pair (i, j). It is used when specializing the cubic deficit and area functionals to singleton hinges. The proof consists of unfolding the singletonHinge definition and applying reflexivity.
claimLet $i, j$ be vertices in a set of cardinality $n$, and let $w$ be a real number with $w$ nonnegative. If $H$ denotes the hinge datum constructed from $i, j, w$, then the edge list of $H$ equals $[(i, j)]$.
background
The module discharges the Regge deficit linearization hypothesis for the cubic lattice by constructing a quadratic-in-ε deficit functional. A HingeDatum is a structure containing an edges list, a weight function on edges, and a proof that weights are nonnegative. The singletonHinge construction populates this structure with a single edge (i, j) carrying weight w. Upstream results define the deficit at a hinge as twice pi minus the sum of dihedral angles.
proof idea
The proof is a one-line wrapper: it unfolds the definition of singletonHinge and concludes by reflexivity.
why it matters in Recognition Science
This lemma enables the singleton specializations cubicDeficit_singleton and cubicArea_singleton. Those results establish the exact match between the cubic deficit functional and the squared potential difference, which discharges the linearization hypothesis and supports the field-curvature identity in the paper's Theorem 5.1. It forms part of the Phase A program to promote the draft argument to a Lean theorem within the Recognition Science framework.
scope and limits
- Does not extend to hinges containing multiple edges.
- Does not evaluate the deficit or area functionals.
- Does not depend on any edge length field or potential recovery.
- Applies exclusively to the singleton hinge construction.
formal statement (Lean)
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. -/