selectedCell5
plain-language theorem explainer
On the 5×5×5 periodic Freudenthal torus, each periodic edge and local tetrahedral pair is assigned a unique base cell so that the pair's local cube geometry sits flush with the edge. Gravity and discrete-Regge auditors cite this cell when expanding mixed explicit-fiber axis-stencil residuals into rational monomial coefficients. The body is a pure composition: match the cube-edge base of the pair's local edge slot against the periodic edge base.
Claim. Given a periodic edge $e$ on the $5\times5\times5$ Freudenthal torus and a local Freudenthal tetrahedral pair $(\tau,f)$, the selected cell is the unique torus vertex obtained by translating $e$'s base so that it matches the one-cube base vertex of the global edge representative of slot $(\tau,f)$.
background
The module certifies the corrected $N=5$ mixed explicit-fiber axis-stencil residual by exact rational arithmetic (no floats), auditing every unordered monomial $\xi(u)\xi(v)$ coefficient. The ambient geometry is the periodic Freudenthal triangulation of the $5\times5\times5$ torus: vertices are $\mathrm{Vertex},5,5,5$, and edges are periodic edges with a base vertex and a displacement.
A Freudenthal local pair names a tetrahedron index and a local edge slot inside the standard six-tet cube decomposition. The map localEdgeOf sends each such slot to one of the 19 one-cube global edge representatives; cubeEdgeBase then returns the Fin-8 corner of the unit cube that anchors that representative. matchingBaseCell5 subtracts those corner bits from a target torus vertex, producing the cell origin at which the local tet geometry is realized relative to a given periodic edge base.
Together these pieces fix a canonical evaluation cell for every (edge, pair) that appears in the explicit-fiber length and Schläfli expansions.
proof idea
One-line definitional composition. Read the local edge representative of the pair via the cube-triangulation slot map, take its unit-cube base corner, and feed that corner together with the periodic edge's base into matchingBaseCell5, which bit-subtracts the corner from the base to obtain the aligned torus vertex. No proof obligations; pure data plumbing.
why it matters
Every scaled coefficient atom and endpoint expansion in the $N=5$ certificate evaluates potentials and edge lengths at this cell. Downstream consumers include the flat local edge-length directional derivative rewritten in typed vertex coordinates, the scaled pair local-vertex coefficient, the closed-form endpoint expansion value, and the theorems that expand one explicit-fiber local-pair (or slot) contribution into checked rational monomial atoms after square-root cancellation.
Without a fixed cell choice, the axis-stencil residual would not be comparable term-by-term to the Python rational audit the module mirrors. In the broader Recognition gravity stack this is scaffolding for the discrete first-variation / Regge side of the continuum limit, not a forcing-chain (T0–T8) step itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.