cubeEdgeDisp
plain-language theorem explainer
Lookup table sending each of the 19 one-cube Freudenthal edge representatives to one of the seven positive lattice displacements in {0,1}^3\{0}. Anyone wiring periodic edges, local slots, or Regge midpoint phases cites it. The body is a pure pattern-match table with an out-of-range absurdity clause.
Claim. A function $\mathrm{cubeEdgeDisp}:\{0,\ldots,18\}\to\{0,\ldots,6\}$ assigning to each one-cube Freudenthal edge representative its positive displacement class among the seven nonzero vectors in $\{0,1\}^3$ (axis edges $x,y,z$, face diagonals $x{+}y,x{+}z,y{+}z$, and space diagonal $x{+}y{+}z$).
background
The module builds a typed periodic Freudenthal torus: vertices on a product of cyclic groups, edges as base vertex plus positive displacement, and six tetrahedra per cube cell. It isolates the scalable geometry so any finite encoder into a Triangulation3D inherits the incidence/edge-slot partition needed by the nonlinear Regge first-variation theorem.
Freudenthal triangulation of the unit cube uses a fixed catalogue of local edges. Those edges are indexed by a 19-element finite type (the one-cube edge representatives). Displacements live in a 7-element type corresponding to the nonzero bit-masks on the three axes: pure $x,y,z$, the three face diagonals, and the body diagonal.
Sibling bit arithmetic (addBit, dispBits, addVertexBits) translates a local representative by adding those displacement bits to a cell base vertex, wrapping on the periodic lattice. This table is the displacement half of that translation.
proof idea
Definition by exhaustive pattern match on Fin 19. Indices 0–6 are the canonical axis, face-diagonal, and body-diagonal classes (comments mark $x,y,z,x{+}y,x{+}z,y{+}z,x{+}y{+}z$). Indices 7–18 repeat those classes for the remaining one-cube edge representatives. Any index $\ge 19$ is discharged by absurd plus omega. No lemmas are invoked.
why it matters
This table is the displacement coordinate of every translated periodic edge. Downstream, localEdgeOf builds a global PeriodicEdge as { base := addVertexBits cell (cubeEdgeBase e), disp := cubeEdgeDisp e }, and theorems such as canonicalPeriodicLocalEdgeNoDup, freudenthalTet_sqEdge_eq_periodicDispSqEdge_localEdgeOf, and localEdgeOf_endpoints_match_tetVerts reason about those edges.
Gravity-side consumers read the same table: slotDispBit and slotMidTwice_eq_geometry in Regge TT Bloch assembly extract displacement bits and doubled midpoints; edgeMidpointPhase_grounded and the six-tet cubic Dirichlet instance use it for phase and angle-sum targets. In the broader RS geometry stack this is scaffolding for the D=3 cubic/Freudenthal mesh that feeds Regge first variation on the periodic torus, not a forcing-chain step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.