edgeFinEquiv
plain-language theorem explainer
Canonical bijection from finite indices onto the set of positive-displacement periodic edges on an Nx×Ny×Nz torus. Anyone wiring a finite Freudenthal mesh (edge endpoints, edge-in-tet slots, squared lengths) cites it to replace typed edges by Fin cards. Proof is the one-line inverse of Mathlib's Fintype.equivFin, using the derived Fintype instance on PeriodicEdge.
Claim. For positive integers $N_x,N_y,N_z$, there is a canonical equivalence $\mathrm{Fin}(|E_{\mathrm{per}}|) \simeq E_{\mathrm{per}}$, where $E_{\mathrm{per}}$ is the finite set of positive-displacement periodic edges (each a base vertex on the $N_x\times N_y\times N_z$ torus together with one of the seven positive cube displacements).
background
The Periodic Freudenthal Torus module supplies the typed scalable 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, without yet fixing a concrete mesh encoder into Fin nV, Fin nE, Fin nT. The module's job is to prove that any finite triangulation encoding this model carries the global incidence/edge-slot partition needed by the nonlinear Regge first-variation theorem.
A periodic edge is a structure with a base vertex and a displacement index in $\mathrm{Fin},7$ (the seven positive cube displacements). It derives Fintype and DecidableEq, so the set is finite once the three periods are nonzero. Endpoints are recovered by adding the displacement bit-pattern to the base under toroidal wrap.
Downstream finite-index APIs (canonical edge vertices, edge-in-tet lookup, global squared edge lengths) all work on Fin (card PeriodicEdge) rather than the structure type, so a named equivalence is required as the bridge.
proof idea
One-line definition: take Mathlib's Fintype.equivFin on PeriodicEdge Nx Ny Nz (available from the derived Fintype instance) and reverse it. The result sends a finite index to the corresponding typed periodic edge. No custom case analysis; noncomputable only because equivFin is.
why it matters
This is the edge half of the finite encoder the module isolates as remaining work. It is consumed everywhere the skeleton is indexed by Fin: canonicalEdgeVerts (endpoint pairs in the finite vertex index set), canonicalEdgeInTet and its correctness lemmas (edge-in-tetrahedron slot lookup), canonicalGlobalSqEdge (squared length from the displacement), canonicalLocalEdge_complete (every local tet edge slot is hit), and canonicalPeriodicEdgeEquiv. Gravity preflight also uses it to identify the canonical edge stencil with the Freudenthal stencil.
In the broader Recognition geometry stack this keeps the periodic torus model aligned with the incidence data the Regge first-variation theorem demands, while leaving the concrete $n\times m\times k$ mesh enumeration as a separate encoder step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.