simplexFinEquiv4
plain-language theorem explainer
Canonical bijection from finite ordinals onto the set of periodic Kuhn 4-simplices at side length N. Anyone indexing the 4D Freudenthal carrier (corner maps, injectivity, skeleton edges, mesh scale) cites this equivalence. It is a one-line Mathlib wrapper: the symmetric of the standard finite-type enumeration.
Claim. For every positive integer $N$, writing $S_N$ for the finite set of periodic Kuhn 4-simplices (each a pair of a 4-torus lattice vertex and one of the $24$ Kuhn permutation types), there is a canonical equivalence $\mathrm{Fin}(|S_N|) \simeq S_N$.
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 (permutation) decomposition of each cubic cell into $4! = 24$ four-simplices. It is deliberately self-contained, defining its own carrier shape rather than extending the 3D tetrahedron-only complex.
A periodic Kuhn 4-simplex is a pair consisting of a base vertex in the $N$-periodic 4-lattice and an index in $\mathrm{Fin},24$ selecting one of the 24 ordered axis-permutations. The product is finite at every side $N$, with cardinality $24 N^4$. Downstream code needs a stable ordinal index for that finite set when building corner maps and carrier predicates.
The only mathematical content here is the standard finite-type enumeration: every nonempty finite type is equivalent to an initial segment of the naturals.
proof idea
One-line definitional wrapper. Apply Mathlib's Fintype.equivFin to the finite type of periodic Kuhn 4-simplices and take the symmetric equivalence, yielding $\mathrm{Fin}(\mathrm{card},S_N)\simeq S_N$. No combinatorial argument is local to this declaration; finiteness is inherited from the product structure of the simplex type.
why it matters
This equivalence is the indexing spine of the canonical 4D carrier. The corner map that sends an ordinal simplex index and a local corner $k\in\mathrm{Fin},5$ to a lattice vertex is defined by decoding through this bijection, then applying the Kuhn vertex table and the vertex enumeration. Injectivity of those corner maps and the skeleton theorem (every pair of distinct simplex corners is realized by some carrier edge) both open by setting the decoded cell-simplex equal to this equivalence applied to the ordinal. Mesh-scale attainment on the hyperbody diagonal likewise sits on the same carrier.
In the Recognition geometry stack this is the 4D mirror of the 3D periodic Freudenthal torus: the missing typed object named by the 4D metric-refinement recon. It does not itself force $D=3$ or the eight-tick octave; it supplies the combinatorial carrier those continuum and discrete structures act on once the 4D assembly worker attaches period-doubling and the refinement family instance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.