canonicalGlobalSqEdge
plain-language theorem explainer
Canonical squared length of a globally indexed positive-displacement edge on the periodic Freudenthal torus is read from the seven-class displacement table. Anyone wiring a finite triangulation into the Regge first-variation incidence package cites this as the global edge-length assignment. The body is a one-line composition of the edge-index equivalence with the displacement-squared lookup.
Claim. For positive integers $N_x,N_y,N_z$ and each finite index $e$ of a positive-displacement periodic edge on the $N_x\times N_y\times N_z$ torus, the canonical global squared edge length equals the squared length of that edge's displacement class among the seven positive cube displacements.
background
The module supplies a scalable typed model of a periodic Freudenthal tiling on a 3-torus of periods $N_x,N_y,N_z$. It does not yet pin a concrete finite mesh; it defines typed vertices, edges, and tetrahedra and isolates the encoder into finite index sets needed by the nonlinear Regge first-variation theorem.
A positive-displacement periodic edge is a base vertex together with one of seven positive cube displacements. Endpoints are obtained by modular addition of the displacement bit pattern. The finite index set of such edges is identified with $\mathrm{Fin}(\mathrm{card},E)$ by the canonical equivalence that inverts Fintype.equivFin.
Squared lengths depend only on the displacement class: the table assigns $1$ to the three axis steps, $2$ to the face diagonals, and completes the seven entries. This definition turns a global edge index into that table value.
proof idea
One-line definitional wrapper. Decode the finite index via the edge-index equivalence to a typed periodic edge, project to its displacement field in $\mathrm{Fin},7$, and evaluate the displacement-class squared-length table. No tactics and no side conditions.
why it matters
Fills the globalSqEdge field of the canonical periodic incidence-consistency package built from an endpoint-incidence hypothesis. That package is exactly the remaining interface so any finite triangulation encoding the typed torus carries the incidence edge-slot partition required by the nonlinear Regge first-variation theorem (module goal).
It also underwrites the local-to-global squared-length match when a global edge sits in a typed tetrahedron, and is cited in the physical six-tet cubic Dirichlet instance: encoded periodic global squared length equals the typed displacement table entry, and the mixed-hinge deficit expanded length-chain target is stated against this map. In the broader stack this is discrete $D=3$ geometry scaffolding for Regge gravity on the forced three-dimensional lattice, not a dynamical or continuum claim.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.