localEdgeOf_endpoints_match_tetVerts
plain-language theorem explainer
On the periodic Freudenthal torus, each local tetrahedral edge slot of a cube cell has endpoints that agree (up to order) with the two vertices obtained by offsetting the cell by the standard Freudenthal tet-vertex bit patterns. Anyone wiring incidence or squared-edge tables for the nonlinear Regge first variation would cite this. The proof is exhaustive case analysis on the six tets and six edge slots, discharged by simplification of the lookup tables.
Claim. Fix nonzero lattice sizes $N_x,N_y,N_z$. For any periodic cell $c$, tetrahedron index $t\in\{0,\ldots,5\}$, and local edge slot $f\in\{0,\ldots,5\}$, let $e$ be the chosen global periodic edge for that slot in $c$, and let $(a,b)$ be the two Freudenthal cube-corner indices of $t$ that bound slot $f$. Writing $c\oplus\cdot$ for the torus bit-offset of cube corners, the unordered pair of endpoints of $e$ equals $\{c\oplus a,\,c\oplus b\}$.
background
The module builds a typed periodic Freudenthal torus: vertices are the product lattice $\mathrm{Fin},N_x\times\mathrm{Fin},N_y\times\mathrm{Fin},N_z$, and the goal is a scalable model whose any finite encoding carries the global edge-slot incidence partition required by the nonlinear Regge first-variation theorem. It does not yet pin a concrete $n\times m\times k$ mesh; it isolates the remaining encoder into finite index types.
Cube corners are coded by $\mathrm{Fin},8$ bit triples. Offsetting a cell by a corner uses bit-addition on each torus coordinate (wrapping via the nonzero-size hypotheses). The six tetrahedra of the Freudenthal cube triangulation are fixed vertex lists of four corners each; each tet has six local edge slots whose two endpoints are read from a standard edge-vertex table.
Upstream, the single-cube triangulation supplies the lookup tables that assign, for every tet and local slot, a global edge representative and the four corner indices of that tet. The periodic model lifts those tables by attaching a base cell and a displacement, so endpoint identity becomes a statement about bit-offsets of those fixed corner codes.
proof idea
Pure case explosion: fin_cases on the tetrahedron index and on the local edge slot (thirty-six concrete pairs). Each residual goal is closed by simp unfolding the periodic local-edge constructor, periodic edge endpoints, the single-cube local-edge and tet-vertex tables, the foundation edge-vertex pairs, and the bit-offset stack (cube edge base/displacement, displacement bits, vertex bits, add-bits). No algebraic lemma is needed beyond definitional equality of the lookup tables.
why it matters
This is the bridge from abstract periodic edge records to concrete tet-corner geometry. Immediately downstream, the canonical periodic endpoint-incidence theorem uses it to show every edge-in-tet witness has matching endpoints under the typed incidence relation, which is exactly the global IncidenceEdgeSlotPartition the module promises for Regge first variation.
Gravity consumers reuse the same identity: the conformal squared-edge preflight equates frozen-wave local edge tuples to the typed conformal edge field read through these local-edge tables, and the physical six-tet cubic Dirichlet instance equates explicit fiber edge slots to endpoints after the same cell-plus-tetVerts offset. Without endpoint matching, those typed-field and fiber equalities would not type-check against the triangulation encoding.
In the broader Recognition geometry stack this is scaffolding closure for the periodic target shape, not a forcing-chain step (T0–T8). It keeps the remaining open work where the module doc places it: a finite encoder from the typed torus into Fin nV, Fin nE, Fin nT.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.