canonicalPeriodicTriangulation
plain-language theorem explainer
Concrete finite periodic Freudenthal triangulation skeleton on an $N_x\times N_y\times N_z$ torus of cubic vertices. Anyone assembling the encoded periodic torus certificate, incidence consistency, or edge/tet equivalences cites this structure. It packages vertex, edge, and tet cardinalities with the canonical incidence maps and a uniform nondegenerate Freudenthal tetrahedron on every cell. The body is pure structure assembly from the typed periodic model; incidence wraparound proofs remain separate.
Claim. For positive integers $N_x,N_y,N_z$, the canonical periodic triangulation is the finite 3D triangulation whose vertices are the periodic cubic lattice points $\mathrm{Fin}\,N_x\times\mathrm{Fin}\,N_y\times\mathrm{Fin}\,N_z$, whose edges and tetrahedra are the typed periodic Freudenthal edges and tets, with incidence given by the canonical edge-vertex, tet-vertex, and edge-in-tet maps, and with every tetrahedron carrying the standard nondegenerate unit-cube Freudenthal geometry.
background
The module isolates a scalable target shape for an arbitrary periodic Freudenthal tiling: typed periodic vertices, edges, and tetrahedra, plus the global incidence-edge-slot partition needed by the nonlinear Regge first-variation theorem. It does not yet enumerate a concrete mesh encoder into finite index types; that encoder is the remaining work.
Periodic cubic vertices are simply triples of finite indices $\mathrm{Fin},N_x\times\mathrm{Fin},N_y\times\mathrm{Fin},N_z$. Upstream, the unit-cube Freudenthal package supplies the local geometry: nineteen unique edges on the cube, six tetrahedra as vertex lists, an incidence map from global edge and tet to a local edge slot, and a single nondegenerate tetrahedron (positive squared edge lengths and positive Cayley-Menger content). The two-cube strip variants of those maps handle adjacent-cell incidence patterns that the periodic model reuses.
A Triangulation3D is the finite skeleton carrying counts $n_V,n_E,n_T$ together with edge-vertex, tet-vertex, and edge-in-tet data and a geometric tet at each cell. This definition fills that record from the typed periodic counts and the canonical incidence maps.
proof idea
Structure-field assembly, not a tactic proof. Vertex count is the cardinality of the periodic cubic vertex type; edge and tet counts are the cardinalities of the typed periodic edge and tet types. The three incidence fields are the already-defined canonical maps (edge vertices, tet vertices, edge-in-tet) for the given periods. Every geometric tetrahedron is the constant unit-cube nondegenerate Freudenthal tet from the cube triangulation package. No lemmas are applied beyond those field definitions and Fintype.card.
why it matters
This is the concrete skeleton the rest of the periodic torus stack sits on. Downstream, the edge and tet equivalences identify finite indices with the typed periodic edges and tets; incidence-consistency constructors (from endpoint incidence, and the packaged consistent instance) take this triangulation as their carrier; the encoded periodic Freudenthal torus builder consumes an incidence-consistent instance of it together with a local-edge no-duplication hypothesis. Gravity stencil preflight compares the canonical edge stencil against the Freudenthal stencil using the same carrier.
In the module's own terms, the point is to isolate remaining work: wraparound no-duplication and local/global squared-edge proofs still sit between this skeleton and a full encoded torus certificate. That certificate is the finite encoder the nonlinear Regge first-variation theorem needs. The construction is geometry infrastructure for discrete gravity on a periodic Freudenthal mesh, not a forcing-chain step (T0-T8), but it is the mesh shape those continuum limits would discretize against.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.