EncodedPeriodicFreudenthalTorus
plain-language theorem explainer
A structure packaging any finite 3D triangulation that realizes the typed periodic Freudenthal torus on an $N_x\times N_y\times N_z$ lattice with sides strictly larger than 2. It records incidence consistency plus equivalences from Fin indices to periodic vertices/tets and positive-displacement edges, with a matching edge-in-tet law. Downstream edge-slot partition, bookkeeping, and Regge first-variation arguments cite this interface. Pure definition: no proof body.
Claim. For $N_x,N_y,N_z\in\mathbb{N}$ with each side strictly greater than $2$, an encoded periodic Freudenthal torus is a finite 3D triangulation $K$ that is incidence-consistent, together with equivalences identifying the tetrahedra of $K$ with pairs (periodic cubic vertex, local tet index in $\{0,\ldots,5\}$) and the edges of $K$ with positive-displacement periodic edges, such that $K$'s edge-in-tet incidence equals the typed local-edge assignment on the torus.
background
The module isolates the scalable target shape for an arbitrary periodic Freudenthal tiling: typed periodic vertices, positive-displacement edges, and six tets per cube, without yet fixing a concrete mesh size. The remaining work is a finite encoder into Fin index sets. Vertices are the product lattice $\mathrm{Fin},N_x\times\mathrm{Fin},N_y\times\mathrm{Fin},N_z$. A periodic edge is a base vertex plus one of seven positive cube displacements; its endpoints are obtained by adding the corresponding bit pattern with wraparound.
Upstream single-cube and two-cube Freudenthal models already fix the local edge-slot tables: each of the six tets has six local edge slots mapped to global edge representatives, and an incidence map returns the local slot when a global edge belongs to a tet. The present structure lifts those local tables to a fully periodic torus by requiring that the abstract triangulation's incidence agree with the typed localEdgeOf after transport along the equivalences.
Side lengths must exceed 2 so that $+1$ and $-1$ wraparounds remain distinct; otherwise the positive-displacement edge model collapses.
proof idea
No proof: this is a structure declaration. The fields are hypotheses and data (side bounds, the triangulation $K$, incidence consistency, tet and edge equivalences, and the biconditional tying $K$'s edge-in-tet map to the typed local-edge assignment). Concrete inhabitants are built later by the canonical encoder from endpoint or incidence data.
why it matters
This is the contract every finite periodic Freudenthal mesh must satisfy before the nonlinear Regge first-variation machinery applies. From any such package one derives the global incidence edge-slot partition and the corresponding bookkeeping structure, which the module doc identifies as the ingredient needed by the Regge first-variation theorem.
Canonical constructors (from incidence consistency, from endpoint incidence, and the fully canonical instance) inhabit the structure for every admissible $(N_x,N_y,N_z)$. Downstream gravity code uses it to certify that the canonical Hessian on the six-tet cubic Dirichlet instance is the Dirichlet form. In the broader Recognition geometry stack this is the scalable $D=3$ discrete substrate on which curvature and mass-ladder calculations sit; it does not itself invoke $J$, $\varphi$, or the forcing chain, but it is the mesh those continuum limits presuppose.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.