localSqEdge_eq_globalSqEdge
plain-language theorem explainer
Whenever incidence places a global edge into a tetrahedron's local edge slot, the local squared length equals the global squared-edge chart value. Builders of global Schläfli cancellation from incidence-consistent 3D Regge data cite this agreement lemma. The proof is a one-line projection of the consistency structure's local-to-global squared-edge field.
Claim. Let $K$ be a 3D triangulation that is incidence-consistent, with global squared-edge chart $q$. If global edge $e$ is incident to tetrahedron $\tau$ in local edge slot $f$, then the squared length of that local edge equals $q(e)$.
background
The module strengthens the abstract 3D Regge triangulation scaffold with incidence and local-Schläfli data needed for global Schläfli cancellation. An incidence-consistent triangulation carries a global squared-edge chart together with vertex-matching rules (local edge endpoints agree with global endpoints up to orientation) and a local-to-global squared-edge identity.
The incidence map sends a global edge and a tetrahedron to an optional local edge slot in ${0,\ldots,5}$. Concrete Freudenthal cube models supply explicit charts and incidence tables; the structure here abstracts those so any $K$ with the same consistency package inherits the same local-global agreement.
Upstream, the Freudenthal cube triangulation proves the concrete case by exhaustive case analysis on edges, tets, and slots. The structure field packages that identity as a hypothesis on general $K$.
proof idea
One-line term proof: apply the structure field local_sqEdge_eq_global from the incidence-consistency witness at the given edge, tetrahedron, slot, and incidence hypothesis. No further rewriting.
why it matters
This is the squared-length bridge used immediately by the sibling length theorem: local edge length (square root of the local squared slot) equals the global edge length read from the consistency chart. That length agreement is part of assembling triangulation Schläfli data from incidence alone, so global Schläfli cancellation can be built without caller-supplied Schläfli packages.
In the Recognition geometry stack this sits under 3D Regge consistency supporting the forced $D=3$ spatial setting (forcing chain T8) and eight-tick discrete structure. It does not itself compute curvature or masses; it only locks local metric slots to the global edge chart so later cancellation identities are well-defined.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.