singletonHinge_edges
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.