edgeFinEquiv4
plain-language theorem explainer
Gives a canonical bijection from a finite ordinal index set onto the set of positive-displacement periodic 4-edges on the N-period 4-torus. Anyone wiring the 4D Freudenthal carrier into Fin-indexed edge tables cites it. The body is the one-line inverse of Mathlib's Fintype.equivFin.
Claim. For every period $N\ge 1$, there is a canonical equivalence $\mathrm{Fin}(|E_N|)\simeq E_N$, where $E_N$ is the finite set of positive-displacement periodic 4-edges (base vertex in the $N$-periodic 4-torus together with one of the fifteen positive 4-cube displacement classes).
background
The module constructs the typed periodic Freudenthal triangulation of the 4-torus: four-coordinate periodic vertices, the fifteen positive-displacement edge classes of the 4-cube, and the Kuhn triangulation into $4!=24$ four-simplices. It is the 4D mirror of the 3D PeriodicFreudenthalTorus development and deliberately defines its own carrier shape rather than extending the tetrahedron-only BoundedComplex.
A periodic 4-edge is a pair (base vertex, displacement class in $\mathrm{Fin},15$). The structure derives Fintype, so the set of such edges is finite for each period $N\ge 1$. Downstream carrier code indexes edges by $\mathrm{Fin},n_E$ rather than by the structure type itself, so a fixed equivalence between the ordinal index set and the edge type is needed.
This definition supplies that bridge. It does not encode geometry; it only freezes a choice of enumeration so that endpoint maps, loop-freeness, and skeleton incidence can be stated uniformly in Fin coordinates.
proof idea
One-line definitional wrapper: take Mathlib's Fintype.equivFin on PeriodicEdge4 N and reverse it. The forward map sends each edge to its ordinal rank; the inverse (this definition) sends each finite index to the corresponding edge. Noncomputable because classical choice underlies the generic Fintype enumeration.
why it matters
The canonical 4D carrier is assembled by indexing vertices, edges, and simplices with Fin. This equivalence is the edge half of that indexing. Downstream it feeds canonicalEdgeVerts4 (endpoint pairs in Fin coordinates), the no-loops and no-multiedges theorems for the carrier skeleton, the skeleton incidence statement that every simplex face pair is realized by some edge, and mesh-scale attainment arguments that quantify over edges.
In the Recognition geometry stack this is scaffolding for the missing 4D MetricRefinementFamily recon object: without a stable Fin enumeration of the fifteen-class periodic edges, the simplicial carrier and mesh machinery cannot be stated. It does not itself force $D=3$ or the eight-tick octave; those live upstream in the forcing chain. The honesty boundary of the module still excludes side schedules, Config, coarsen, and the MetricRefinementFamily instance proper.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.