PeriodicSimplex4
plain-language theorem explainer
The type of periodic Kuhn 4-simplices at grid side N is the product of the N^4 periodic 4-torus vertices with Fin 24 (the 4! Kuhn permutations of the unit 4-cube). Carrier builders, simplex-count lemmas, and the 4D period-doubling witness all index through this type. It is a one-line product abbreviation of finite types, so finiteness is immediate.
Claim. For each $N \in \mathbb{N}$, a periodic Kuhn 4-simplex at side $N$ is a pair $(v,\sigma)$ where $v$ is a vertex of the side-$N$ periodic 4-torus grid $(\mathbb{Z}/N)^4$ and $\sigma \in \{0,\ldots,23\}$ selects one of the $4!=24$ Kuhn 4-simplices inside the corresponding cubic cell.
background
This module supplies the typed periodic Freudenthal triangulation of the 4-torus demanded by the 4D MetricRefinementFamily recon: four-coordinate periodic vertices, the fifteen positive-displacement edge classes of the 4-cube, and the Kuhn (permutation) split of each 4-cube into $4!=24$ four-simplices. It is deliberately self-contained; the existing BoundedComplex carrier is tetrahedron-only and cannot hold Fin-5 corners.
Vertex4 N is the finite grid Fin N × Fin N × Fin N × Fin N. The Kuhn tables list corners as partial sums of the 24 axis permutations in lex order. A periodic 4-simplex is then just a base cell vertex together with which of those 24 local simplices sits in that cell. The product of finite types is finite at every side N, which is the whole point of the abbreviation.
proof idea
Definitional abbreviation only: unfold to the product type Vertex4 N × Fin 24. No tactics, no lemmas. Downstream cardinality is immediate from Fintype.card_prod, card_vertex4, and Fintype.card_fin.
why it matters
This is the simplex index type for the whole 4D periodic Freudenthal stack. canonicalCarrier4D sets its simplex count nS to Fintype.card (PeriodicSimplex4 N). canonicalSimplexVerts4 and simplexFinEquiv4 decode a finite index into a cell-plus-Kuhn-label pair and map the five Kuhn corners into the global vertex index set. card_periodicSimplex4 records the closed count $24 N^4$.
Outside the geometry module, freudenthal4D_period_doubling_simplicial_witness quantifies over PeriodicSimplex4 N to exhibit an explicit coarse 4-simplex under the period-doubling vertex map, the Gap2 4D period-doubling projection. The type is the 4D mirror of the 3D PeriodicFreudenthalTorus simplex set and is infrastructure for the still-external MetricRefinementFamily assembly (side schedule, Config, coarsen, action control), not a physics claim by itself. Landmarks touched only indirectly: D=3 is the 3D sibling; here the ambient lattice is 4D spacetime cells.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.