cubeEdgeBase
plain-language theorem explainer
Lookup table sending each of the 19 one-cube Freudenthal edge representatives to its base vertex among the 8 cube corners. Geometers and Regge analysts cite it when assembling periodic edge data from local tetrahedral slots. The body is a pure pattern-match table on Fin 19, with an absurd branch ruling out out-of-range indices.
Claim. A function $b:\{0,\ldots,18\}\to\{0,\ldots,7\}$ that assigns to each of the 19 one-cube Freudenthal edge representatives the index of its base vertex in the unit cube (the eight corners labeled $0$ through $7$).
background
The module builds a typed periodic Freudenthal torus: vertices, edges, and tetrahedra on an $N_x\times N_y\times N_z$ lattice with wrap-around, without yet fixing a concrete finite mesh encoder. The goal is the global incidence/edge-slot partition required by the nonlinear Regge first-variation theorem.
A unit cube has eight corners. The classical Freudenthal triangulation cuts that cube into six tetrahedra. Edges that live inside a single cube are represented by a fixed list of 19 combinatorial types. Each such type is an oriented segment from a base corner to a positive displacement; this definition records only the base corner.
Sibling data (bit flips, vertex-bit addition, displacement tables) turn the base index into a concrete periodic edge once a cell origin is chosen. Downstream, localEdgeOf translates the base by the cell's vertex bits and pairs it with the matching displacement.
proof idea
No proof: it is a definition by exhaustive pattern match. Cases $0$ through $18$ return fixed values in $\mathrm{Fin},8$ (seven edges from vertex $0$, three from $1$, three from $2$, one from $3$, three from $4$, one from $5$, one from $6$). The residual constructor $\langle n+19,h\rangle$ is discharged by absurd and omega, so the match is total on $\mathrm{Fin},19$.
why it matters
This table is the geometric anchor for every translated local edge on the periodic torus. localEdgeOf builds a global periodic edge as base = cell $\oplus$ cubeEdgeBase(e) with the matching displacement; endpoint-matching lemmas and the incidence partition rest on that construction.
In the gravity stack it feeds Bloch/Regge assembly: slot base bits, doubled-midpoint identities, exact phase decompositions (including periodic seams), and the grounding theorem that midpoint phases equal the preregistered slot table. Those results sit on the path to the nonlinear Regge first-variation theorem on a Freudenthal mesh.
Framework-wise it is pure discrete geometry scaffolding for the $D=3$ spatial lattice (forcing chain T8) and the eight-corner cube that matches the eight-tick register combinatorics, not a dynamical claim about $J$, $\varphi$, or $\alpha$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.