localEdgeLength_eq_globalEdgeLength
plain-language theorem explainer
In an incidence-consistent 3D Regge triangulation, the local edge length at any tetrahedron-incident edge equals the global edge length fixed by the consistency chart. Builders of global Schläfli data from incidence mixins cite this bridge. The proof unfolds the global-length definition and rewrites by the squared-edge identity.
Claim. Let $K$ be a 3D Regge triangulation that is incidence-consistent. If global edge $e$ meets tetrahedron $\tau$ in local edge slot $f$, then the local length $\sqrt{s_\tau(f)}$ equals the global edge length of $e$ determined by the consistency chart.
background
The module upgrades the abstract 3D Regge scaffold Triangulation3D with incidence and local-Schläfli data so that global Schläfli cancellation can be assembled without caller-supplied Schläfli packages. An incidence-consistent triangulation carries a global squared-edge chart together with vertex-matching rules (local tetrahedral edge slots agree with global endpoints up to orientation) and a closed-form local Schläfli proof on each tetrahedron.
Global edge length is the nonnegative square root of that global squared-edge chart. Local length is the square root of the tetrahedron's own squared-edge coordinate at the incident slot. The incidence map edgeInTet records which global edges sit in which local slots of which tetrahedra (as in the Freudenthal cube and two-cube-strip models).
The immediate upstream fact is the squared version: under the same incidence hypothesis, local and global squared edge lengths already agree. Taking square roots then yields the length statement used by length-based geometric identities.
proof idea
Term-mode, two steps. Unfold the definition of global edge length (square root of the global squared-edge chart). Rewrite the remaining equality by the sibling lemma that local and global squared edge lengths coincide under incidence consistency and the given edgeInTet witness. No case analysis or arithmetic beyond that rewrite.
why it matters
Global Schläfli cancellation on a 3D Regge complex needs a single length per global edge, not a cloud of local copies. This lemma certifies that every local length pulled from an incident tetrahedron matches the consistency chart, so dihedral and deficit bookkeeping can be written in global coordinates.
It sits beside the squared-edge identity and feeds the constructors that build triangulation Schläfli data from incidence (and the corresponding global Schläfli theorems in the same module). The setting is strictly three-dimensional Regge geometry, aligning with the framework landmark that spatial dimension is forced to $D=3$ (T8) and with the eight-tick octave structure that organizes discrete recognition ticks.
No downstream dependents are recorded yet; the lemma is infrastructure for the incidence-to-global-Schläfli path rather than a leaf result.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.