localEdgeOf
plain-language theorem explainer
Given a cubic cell on the periodic Nx×Ny×Nz torus, one of its six Freudenthal tetrahedra, and a local edge slot, this returns the matching positive-displacement periodic edge. Discrete-geometry and Regge-calculus work cites it when wiring global edge-slot incidence on the typed torus model. The body is a pure lift: read the one-cube edge table, then translate its base offset and displacement into the cell.
Claim. For $N_x,N_y,N_z\ge 1$, cell $c$ on the $N_x\times N_y\times N_z$ torus, tetrahedron index $\tau\in\{0,\ldots,5\}$, and local edge slot $f\in\{0,\ldots,5\}$, return the positive-displacement periodic edge whose base is $c$ shifted by the local cube-vertex offset of the standard one-cube Freudenthal edge for $(\tau,f)$, and whose displacement is that edge's positive cube direction.
background
The module defines a scalable typed model of a periodic Freudenthal tiling on an $N_x\times N_y\times N_z$ cubic torus. Vertices are triples in $\mathrm{Fin},N_x\times\mathrm{Fin},N_y\times\mathrm{Fin},N_z$. A periodic edge is a base vertex together with one of seven positive cube displacements (three axes, three face diagonals, one space diagonal).
Each cubic cell is cut into the six standard Freudenthal tetrahedra. Upstream, the one-cube triangulation fixes a table sending every tetrahedron-and-slot pair to one of nineteen edge representatives inside a single cube, plus maps from those labels to a local base vertex in $\mathrm{Fin},8$ and a displacement in $\mathrm{Fin},7$. Adding vertex bits translates that local base into the chosen periodic cell.
The module isolates the remaining work: a finite encoder into concrete $\mathrm{Fin},n_V$, $\mathrm{Fin},n_E$, $\mathrm{Fin},n_T$ that inherits the global incidence edge-slot partition needed by the nonlinear Regge first-variation theorem.
proof idea
Definitional construction only. Look up the one-cube edge index $e$ from the Freudenthal cube table at $(\tau,f)$. Build the periodic edge with base equal to the cell shifted by the local cube-vertex bits of $e$, and displacement equal to the positive cube displacement of $e$. No case split runs here; all combinatorial content lives in the upstream lookup tables for the one-cube representatives.
why it matters
This is the periodic lift of the one-cube and two-cube-strip local-edge maps. Those maps underwrite edge-in-tetrahedron incidence, local-edge completeness, and the IncidenceEdgeSlotPartition instances on the cube and strip models. The module doc states the target: any finite Triangulation3D encoding of this typed torus must carry that same unique/no-duplication edge-slot partition for the nonlinear Regge first-variation theorem. The definition supplies the typed global edge for every local slot so the encoder can inherit the partition. It lives in the discrete-geometry layer for Regge calculus, not in the T0–T8 forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.