globalEdgeLength
plain-language theorem explainer
Extracts the Euclidean length of a global edge in an incidence-consistent 3D Regge triangulation by taking the positive square root of the incidence chart's squared length. Anyone writing Schläfli bookkeeping or first-variation identities for the Regge action cites this as the common length scale on shared edges. The body is a one-line definition: square root of the global squared-edge field.
Claim. Given a finite 3D Regge triangulation $K$ equipped with strong incidence consistency (a global squared-edge chart $\ell^2_{\mathrm{glob}} : E(K)\to\mathbb{R}$ compatible with local tetrahedral edge slots), the global edge length of edge $e$ is $\sqrt{\ell^2_{\mathrm{glob}}(e)}\in\mathbb{R}$.
background
The module upgrades the abstract finite 3D Regge scaffold to data strong enough for global Schläfli cancellation. A triangulation records vertex/edge/tet counts, edge endpoints, tet vertex maps, and a nondegenerate squared-edge 6-tuple on each tetrahedron.
Strong incidence consistency supplies a single global squared-edge chart on all edges, forces local tet edge slots to match those global endpoints up to orientation, equates local squared lengths with the global chart on incident slots, and packages the local closed-form Schläfli identity needed later. Concrete Freudenthal cube and strip models already exhibit analogous global squared-edge tables (axis edges length-squared 1, face diagonals 2, etc.).
Global length is the geometric quantity that appears when one reindexes sums over local edge slots against sums over global edges in the Regge action.
proof idea
Pure definitional wrapper: return the real square root of the incidence structure's global squared-edge value at $e$. No lemmas, no tactics beyond the definitional equation.
why it matters
This length is the common scale that makes local and global edge data interchangeable. The sibling theorem equating local tet edge length to this global length is proved by unfolding the definition and applying the incidence squared-edge agreement field.
Downstream, incidence edge-slot bookkeeping structures in the Regge first-variation module weight global edges by this length when proving that summing a local slot weight over global edges and tets equals summing directly over local slots. That bookkeeping feeds conformal Schläfli incidence identities used for first variation of the Regge action. In the broader RS geometry stack this is scaffolding for global Schläfli cancellation on incidence-consistent 3D triangulations (the module's stated goal), not a forcing-chain step (T0–T8).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.