PeriodicTet
plain-language theorem explainer
Periodic Freudenthal tetrahedra are pairs (cubic cell, tet index): a vertex of the Nx×Ny×Nz torus times one of the six Freudenthal tets in that cell. Anyone building the finite periodic skeleton, edge-in-tet lookup, or encoded Triangulation3D cites this type. It is a pure type abbreviation, not a proved statement.
Claim. For natural numbers $N_x,N_y,N_z$, a periodic Freudenthal tetrahedron is an element of $V_{N_x,N_y,N_z}\times\{0,\ldots,5\}$, where $V_{N_x,N_y,N_z}=\mathbb{Z}/N_x\mathbb{Z}\times\mathbb{Z}/N_y\mathbb{Z}\times\mathbb{Z}/N_z\mathbb{Z}$ is the set of periodic cubic vertices. The second factor labels which of the six Freudenthal tetrahedra sits inside that cubic cell.
background
The module builds a scalable typed model of a periodic Freudenthal tiling on a 3-torus. It does not yet fix a concrete mesh size; it defines vertices, edges, and tetrahedra so that any finite Triangulation3D encoding of the model carries the incidence and edge-slot partition needed by the nonlinear Regge first-variation theorem.
A periodic cubic vertex is a triple of modular coordinates (i,j,k) with i < Nx, j < Ny, k < Nz. The classical Freudenthal decomposition splits each unit cube into six tetrahedra (one per permutation of the three axes, with a fixed orientation convention from the cube-triangulation import).
This abbreviation packages that geometry: each tet is named by the base cell of the torus together with a Fin 6 label for which of the six local Freudenthal tets it is.
proof idea
No proof. The declaration is a type abbreviation: the product of the periodic vertex type with Fin 6. Downstream code treats elements as (cell, tetIndex) pairs and uses the cube-triangulation API to recover vertices, edges, and slots from the second component.
why it matters
This is the tetrahedron carrier for the entire periodic Freudenthal torus stack. Downstream definitions index finite tet sets by Fintype.card (PeriodicTet Nx Ny Nz) and decode via equivalences into cell-plus-local-tet data: canonical edge-in-tet lookup, completeness of local edges, equality of square-edge data with the global Freudenthal table, the canonical periodic triangulation, and the encoded torus whose tetVerts match the typed model.
In the Recognition geometry pipeline this is the typed half of the remaining encoder work named in the module doc: map the periodic torus into Fin nV, Fin nE, Fin nT while preserving incidence. That encoding feeds Regge first-variation and hinge-aware zero-mode analysis on periodic meshes. It sits in the D = 3 spatial setting (T8) as the discrete 3-complex on which curvature and mass-gap bookkeeping run, not as a new forcing step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.