canonicalPeriodicLocalEdgeNoDup
plain-language theorem explainer
Within each lattice cell and each of the six Freudenthal tetrahedra on the periodic torus, the six local edge slots map injectively to distinct global periodic edges. Anyone building the encoded periodic Freudenthal torus or regrouping Regge edge sums needs this injectivity. The proof is exhaustive Fin-case analysis on tetrahedron and slot indices, reduced by the cube edge tables.
Claim. For all positive integers $N_x,N_y,N_z$, every lattice cell $c$, every Freudenthal tetrahedron index $t\in\{0,\ldots,5\}$, and every pair of local edge slots $f,g\in\{0,\ldots,5\}$, if the translated global periodic edges assigned to slots $f$ and $g$ in cell $c$ and tetrahedron $t$ coincide, then $f=g$.
background
The module supplies the scalable typed model for an arbitrary periodic Freudenthal tiling: vertices on an $N_x\times N_y\times N_z$ torus, six tetrahedra per cube cell, and translated global edges. It does not yet enumerate a concrete finite mesh; it isolates the remaining encoder into Fin indices and proves the incidence/slot partition needed by nonlinear Regge first variation.
The local edge map sends a cell, a tetrahedron index, and a slot $f\in\mathrm{Fin},6$ to a periodic edge by looking up the one-cube Freudenthal representative and attaching the cell via bit-addition of the cube base together with a fixed positive displacement (cubeEdgeDisp). The cube triangulation table chooses, for each of the six tets and six slots, one of nineteen edge representatives.
The proposition proved here is the remaining wraparound/no-duplication target: that table, after translation to the torus, must be injective in the slot index inside a fixed cell and tet.
proof idea
Introduce the cell, tetrahedron, two slots, and the equality of their translated edges. Case-split exhaustively on the tetrahedron index and both slot indices (each ranges over six values). In every branch, unfold the periodic local-edge map, the cube-triangulation local-edge table, and the displacement table; simplification collapses both sides to concrete edge data and forces the two slots to be equal. No arithmetic on the torus sizes is required: injectivity is combinatorial in the finite lookup tables.
why it matters
This injectivity is a gate on the path from the typed periodic skeleton to a full encoded periodic Freudenthal torus and to incidence-consistent triangulations (via the endpoint-incidence constructors in the same module). Downstream, the Regge analysis reuses it as part of the regrouping bijection: edge-sums of slot-matched values equal slot-sums over a tet's six local edges, which is the incidence involution behind every regrouped Regge sum. The physical six-tet cubic Dirichlet instance likewise equates typed edge angle contributions with sums over local slots guarded by geometric equality to the local-edge map, and equates slot-witness incidence with that geometric witness. Without slot injectivity those regroupings would double-count or drop contributions. In the broader Recognition geometry stack this is pure combinatorial scaffolding for the discrete gravity side, not a forcing-chain step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.