vertexPairHingeWeight
plain-language theorem explainer
For a finite 3D Regge triangulation with incidence data, the hinge weight of an unordered vertex pair is the sum, over all edges, of the incidence edge-pair weights. Each contributing edge adds the square root of its global squared length when its endpoints are exactly that pair. Anyone building independent dual weights for the Regge component comparison cites this. The body is a one-line sum over the edge-pair incidence weight.
Claim. Given a finite 3D Regge triangulation $K$ with incidence geometry $h_K$, and vertices $i,j$, the independent dual (hinge) weight of the pair $(i,j)$ is $$w(i,j)=\sum_{e}\,w_{\mathrm{edge}}(i,j;e),$$ where $w_{\mathrm{edge}}(i,j;e)$ equals $\sqrt{\ell_e^2}$ if the endpoints of $e$ are $\{i,j\}$ and $0$ otherwise.
background
The module isolates an independent dual-weight construction from the weak-field coefficient matrix, so that a later theorem can turn pure geometry into the Regge component comparison. A Triangulation3D is a finite abstract 3D Regge complex: vertex, edge, and tetrahedron counts, edge endpoint pairs, and tetrahedron vertex maps, plus a nondegenerate squared-edge tuple on each tet.
IncidenceGeometry supplies pure incidence consistency and a global squared-edge chart $\ell_e^2$ on edges, without packaging local Schläfli identities as structure fields. The sibling edge-pair incidence weight is the local summand: it returns $\sqrt{\ell_e^2}$ precisely when edge $e$ has endpoints $(i,j)$ or $(j,i)$, and zero otherwise. The present definition aggregates those summands over all edges, yielding a hinge weight read directly from the incidence-level length chart rather than from a negated Regge Hessian entry.
proof idea
Definitional one-liner: unfold to the finite sum over edges $e\in\mathrm{Fin},n_E$ of the edge-pair incidence weight for $(i,j,e)$. No lemmas are applied; the mathematical content is entirely in that summand (indicator on matching endpoints times $\sqrt{\ell_e^2}$).
why it matters
This is the geometric hinge weight that populates the independent dual-weight package. Downstream, independentDualWeightsOfIncidence sets its weight field to this function and packages the companion symmetry and nonnegativity theorems, so the dual side of the Regge component comparison is incidence-defined rather than Hessian-derived.
That separation is the module's stated purpose: keep dual weights independent of the weak-field coefficient matrix, then feed a clean geometric object into the comparison target. In the broader gravity thread this supports discrete curvature bookkeeping on 3D triangulations (Regge calculus in $D=3$), aligned with the framework's forced spatial dimension $D=3$ (T8) without yet invoking the full forcing chain or the Recognition Composition Law. Symmetry and nonnegativity of the same weight are proved immediately after, so the definition is the hinge of that small local cluster.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.