matchingBaseCell5
plain-language theorem explainer
Given a cube-corner label a in {0,...,7} and a target vertex on the 5×5×5 periodic lattice, returns the unique base-cell origin whose a-corner lands on that target. Lattice auditors of the Freudenthal axis-stencil residual cite it when pinning the reference cell for an edge. The body is a coordinate-wise conditional decrement by the binary bits of a.
Claim. For cube-corner index $a \in \{0,\ldots,7\}$ and target vertex $v$ on the $5\times 5\times 5$ torus, the matching base cell is the vertex obtained by subtracting one (mod 5) from each coordinate of $v$ whose corresponding bit in the binary cube label of $a$ is set.
background
The module certifies coefficients in the corrected $N=5$ mixed explicit-fiber Freudenthal axis-stencil residual by exact rational arithmetic (no floats), mirroring the Python audit script named in the module doc.
Vertices live on the product torus $\mathrm{Fin},5\times\mathrm{Fin},5\times\mathrm{Fin},5$. Local cube corners are labeled by $a\in\mathrm{Fin},8$; vertexBits maps each label to a triple of booleans (the binary offsets of that corner inside the unit cube). The helper subBit5 decrements a $\mathrm{Fin},5$ coordinate by one mod 5 exactly when its bit is true, otherwise leaves it fixed.
Together these give a pure lattice translation that undoes the cube-corner offset, recovering a candidate base-cell origin from any observed target vertex and corner label.
proof idea
Definitional, not a proof. Unpack the binary cube label of $a$ via the upstream vertexBits table, then apply subBit5 independently on each of the three $\mathrm{Fin},5$ coordinates of the target. The result is the triple of adjusted coordinates, typed as a $5\times 5\times 5$ vertex.
why it matters
This selector is the geometric inverse used throughout the axis-stencil certificate. Downstream, matchingBaseCell5_spec proves that adding the same cube bits back recovers the original target (so the base cell is a true preimage). matchingBaseCell5_translate shows the construction commutes with lattice translation. selectedCell5 applies it to a periodic edge and a Freudenthal local pair, choosing the base cell whose cube-edge matches the pair.
In the broader gravity stack this pins the reference cell for every unordered monomial $\xi(u)\xi(v)$ in the $N=5$ residual audit, keeping the Freudenthal fiber geometry exact on the discrete torus.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.