canonicalPeriodicEdgeEquiv
plain-language theorem explainer
Canonical bijection between the finite edge indices of the periodic Freudenthal triangulation skeleton and the typed positive-displacement periodic edges on an $N_x\times N_y\times N_z$ torus. Anyone wiring Fin-indexed Regge data to the geometric edge model cites it. The body is a one-line alias of the Fintype edge equivalence, using that the skeleton edge count equals the cardinality of PeriodicEdge.
Claim. For positive integers $N_x,N_y,N_z$, there is a canonical equivalence $\mathrm{Fin}(n_E)\simeq E_{\mathrm{per}}(N_x,N_y,N_z)$ between the finite edge-index set of the canonical periodic Freudenthal triangulation (whose $n_E$ is the number of positive-displacement periodic edges) and the set of typed periodic edges, each given by a base vertex and one of seven positive cube displacements.
background
The Periodic Freudenthal Torus module supplies the scalable typed target for an arbitrary periodic Freudenthal tiling: vertices, positive-displacement edges, and tetrahedra on an $N_x\times N_y\times N_z$ lattice torus, together with the claim that any finite Triangulation3D encoding of that model carries the global incidence/edge-slot partition needed by nonlinear Regge first variation. It deliberately stops short of a concrete mesh encoder into Fin nV, Fin nE, Fin nT.
A periodic edge is a base vertex plus a displacement in Fin 7 (the seven positive cube edge classes); its endpoints are the base and the base shifted by the corresponding bit pattern, with wraparound. The canonical periodic triangulation skeleton sets $n_E$ to the Fintype cardinality of that edge type. The upstream finite-index equivalence is the symmetric Fintype equivalence Fin (card PeriodicEdge) ≃ PeriodicEdge.
proof idea
One-line wrapper: return the existing edge finite-index equivalence for $(N_x,N_y,N_z)$. That map is already (Fintype.equivFin (PeriodicEdge)).symm. Because the skeleton defines $n_E$ as Fintype.card (PeriodicEdge), the types Fin (canonicalPeriodicTriangulation).nE and Fin (card PeriodicEdge) coincide, so no further transport is needed.
why it matters
This name is the edge leg of the typed-to-Fin dictionary for the periodic torus. Downstream, the encoded periodic Freudenthal torus package builds on it (together with incidence and no-duplication hypotheses) so that Fin-indexed edge vertices and global squared lengths match the typed endpoints and displacement-class table. Physical six-tet cubic Dirichlet instances and the tensor shear sector then quote those equalities when expanding mixed hinge deficits and checking endpoint symmetry on the encoded torus. In the module's own terms, it isolates remaining encoder work while giving gravity/Regge developments a stable edge equivalence to cite.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.