canonicalLocalSqEdge_eq_global
plain-language theorem explainer
When a finite-indexed periodic edge sits in slot f of a finite-indexed periodic Freudenthal tetrahedron, the unit-cube squared length at that slot equals the edge's canonical global squared length. Incidence-consistency proofs for the canonical periodic triangulation cite this length match. The argument extracts the edge identity from the lookup hypothesis, then applies the local-displacement squared-length identity.
Claim. Let $N_x,N_y,N_z\ge 1$. For a finite index $e$ of a positive-displacement periodic edge, a finite index $\tau$ of a periodic Freudenthal tetrahedron, and a slot $f\in\{0,\ldots,5\}$, if the canonical edge-in-tetrahedron lookup returns $f$, then the squared edge length of the unit Freudenthal tetrahedron at slot $f$ equals the canonical global squared length of edge $e$.
background
The module builds a typed periodic Freudenthal torus: vertices on an $N_x\times N_y\times N_z$ lattice, edges as a base vertex plus one of seven positive cube displacements, and tetrahedra as a cell vertex paired with one of the six Freudenthal tets per cube. The goal is the global incidence/edge-slot partition needed by the nonlinear Regge first-variation theorem, without yet encoding a concrete finite mesh into Fin ranges.
A unit-cube Freudenthal tetrahedron supplies a fixed six-slot squared-edge table. The periodic model lifts those lengths via displacement: canonicalGlobalSqEdge reads the displacement of the decoded periodic edge and returns the corresponding squared length. The lookup canonicalEdgeInTet asks whether a finite edge index appears as a local slot inside a finite tet index; when it returns some f, the companion lemma identifies the decoded edge with the local edge of that cell and tet at slot $f$.
proof idea
Term-mode proof in four steps. First apply canonicalEdgeInTet_eq_some_implies to the hypothesis that the lookup returns some f; this yields equality of the decoded periodic edge with the local edge of the decoded cell/tet at slot $f$. Unfold canonicalGlobalSqEdge (squared length of the edge's displacement). Rewrite by the extracted edge identity. Finish with freudenthalTet_sqEdge_eq_periodicDispSqEdge_localEdgeOf on the decoded cell, tet index, and slot $f`, which equates the unit Freudenthal squared length at $f$ to the periodic displacement squared length of that local edge.
why it matters
Squared-edge agreement between local Freudenthal slots and global periodic edges is a required field of IncidenceConsistent for the canonical periodic triangulation. Downstream, canonicalPeriodicIncidenceConsistent_of_endpoint packages canonicalGlobalSqEdge as the global length function and needs this identity whenever an edge-in-tet witness is present, so vertex/endpoint incidence lines up with lengths.
In the module's program this is infrastructure, not a forcing-chain landmark: it closes one algebraic obligation on the path from the typed periodic torus to a finite Triangulation3D with the incidence partition the Regge first-variation theorem consumes. The remaining open work named in the module doc is the finite encoder into Fin nV, Fin nE, Fin nT.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.