edgePairIncidenceWeight
plain-language theorem explainer
For a 3D triangulation with incidence geometry, each edge contributes either the square root of its global squared length or zero to an unordered vertex pair, according as the edge endpoints match that pair. Regge/weak-field gravity workers cite it as the atomic summand of the independent dual (hinge) weight. The body is a pure case split on endpoint equality; no lemmas are invoked.
Claim. Let $K$ be a 3D triangulation equipped with incidence geometry data, and let $i,j$ be vertices and $e$ an edge. The edge-pair incidence weight is $\sqrt{\ell_e^{2}}$ if the endpoints of $e$ are exactly $\{i,j\}$ (in either order), and $0$ otherwise, where $\ell_e^{2}$ is the global squared edge length of $e$.
background
The module builds the final Regge component comparison target: it separates an independent dual-weight construction, read off the incidence-level edge-length chart, from the weak-field coefficient matrix, then records the theorem that turns that geometric computation into the Regge component comparison.
A triangulation $K$ supplies finite vertex and edge index sets together with an endpoint map sending each edge to an ordered pair of vertices. Incidence geometry packages a global squared-edge chart $\ell_e^{2}$ on those edges. The present weight is the indicator of endpoint match times $\sqrt{\ell_e^{2}}$: a global edge contributes to the unordered pair $(i,j)$ exactly when its endpoints are $(i,j)$ or $(j,i)$.
Downstream, summing this weight over all edges yields the independent dual/hinge weight for the vertex pair, defined directly from the incidence chart rather than by negating a Regge Hessian coefficient.
proof idea
Pure definition by case analysis. If the ordered endpoints of $e$ equal $(i,j)$ or $(j,i)$, return the real square root of the global squared edge length; otherwise return $0$. No lemmas, rewrites, or tactics are used.
why it matters
This is the atomic building block of the independent dual-weight side of the Regge component comparison. It is summed in the vertex-pair hinge weight, which the module explicitly refuses to define by negating a Regge Hessian entry. Symmetry in the two vertices is immediate from the unordered endpoint test, and nonnegativity of the summed hinge weight follows once the global squared-edge chart is nonnegative.
Those three downstream facts (symmetry of the edge weight, the hinge-weight sum, and hinge-weight nonnegativity) feed the canonical weak-field data extracted from incidence geometry and the bilinear-coefficient / off-diagonal component-match lemmas that close the comparison. In the broader Recognition gravity stack this keeps the dual weights geometrically native to the triangulation rather than parasitic on a second-variation matrix.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.