canonicalEdgeInTet
plain-language theorem explainer
Canonical edge-in-tetrahedron lookup on the finite periodic Freudenthal skeleton. Given Fin-indices of a positive-displacement periodic edge and a periodic tetrahedron on an Nx×Ny×Nz torus, it returns the local slot in {0..5} if the edge lies in that tet, else none. Incidence, completeness, and triangulation-assembly lemmas cite it. The body is a thin decode-and-delegate wrapper around the typed local slot probe.
Claim. For positive integers $N_x,N_y,N_z$, finite index $e$ of a positive-displacement periodic edge, and finite index $\tau$ of a periodic Freudenthal tetrahedron, return $\mathrm{some}(f)$ with $f\in\{0,\ldots,5\}$ if edge $e$ occupies local edge-slot $f$ of tetrahedron $\tau$, and $\mathrm{none}$ otherwise.
background
The module builds a scalable typed model of a periodic Freudenthal tiling on an $N_x\times N_y\times N_z$ torus. It does not yet pin a concrete mesh encoder; it supplies typed vertices, edges, and tetrahedra so any finite Triangulation3D realizing the model inherits the global edge-slot partition used by the nonlinear Regge first-variation theorem.
A periodic edge is a base vertex plus one of seven positive cube displacements. A periodic tetrahedron is a cubic cell (vertex) paired with one of the six Freudenthal tets inside that cell. Finite indices are decoded by the canonical equivalences that identify Fin-labels with these typed objects.
Upstream, the typed probe canonicalEdgeSlot? decides whether a given periodic edge equals one of the six local edges of a cell-tet pair, returning the matching slot or none. This definition is the Fin-indexed front end of that probe.
proof idea
One-line definitional wrapper. Decode the tetrahedron index via the tet Fin-equivalence to a cell-tet pair; decode the edge index via the edge Fin-equivalence to a typed periodic edge; hand both to the typed local slot lookup canonicalEdgeSlot?. No extra case analysis lives here.
why it matters
This is the Fin-level incidence oracle for the canonical periodic skeleton. Downstream lemmas read its some/none answers: implication from a successful lookup, the no-duplication biconditional, completeness (every local slot is hit by some global edge), and equality of local squared edges with the global Freudenthal table.
It is wired into the concrete canonicalPeriodicTriangulation skeleton and into the remaining endpoint-orientation predicate that demands local Freudenthal endpoints match global periodic endpoints up to orientation. Gravity-side six-tet Dirichlet targets also consume it when assembling typed edge-angle sums.
In the module's own framing, this isolates residual work: wraparound no-duplication and local/global squared-edge proofs still sit between the typed torus and a full encoded incidence certificate for Regge variation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.