matchingBaseCell5_spec
plain-language theorem explainer
On the 5×5×5 periodic torus, subtracting the three bit offsets of an octave index a∈{0,…,7} from a target vertex and then adding them back recovers that vertex. Auditors of the corrected Freudenthal axis-stencil residual cite this to justify the base-cell matching map used in cell selection. The proof is pure exhaustive case analysis over Fin 5 coordinates and all eight bit patterns.
Claim. For every octave index $a\in\{0,\ldots,7\}$ and every vertex $v$ on the $5\times 5\times 5$ periodic lattice, if $b$ is the base cell obtained by subtracting the three coordinate bits of $a$ from $v$, then adding those same bits to $b$ recovers $v$.
background
The module certifies rational coefficients in the corrected $N=5$ mixed explicit-fiber axis-stencil residual for the Freudenthal triangulation. It mirrors a Python audit script and uses no floating-point arithmetic: every unordered monomial coefficient $\xi(u)\xi(v)$ in the residual is checked exactly.
Vertices live on a $5\times 5\times 5$ periodic torus. An octave index $a\in\mathrm{Fin},8$ unpacks to a triple of bits; translating a vertex by those bits is addVertexBits, while the matching base cell subtracts them coordinatewise. The claimed identity says subtraction then addition is the identity on every target.
The eight values of $a$ match the T7 eight-tick octave (period $2^3$) in the Recognition forcing chain. The local setting is discrete gravity stencil geometry on the Freudenthal complex, not continuum GR.
proof idea
Destructure the target into its three $\mathrm{Fin},5$ coordinates. Case-split exhaustively on each coordinate and on $a\in\mathrm{Fin},8$ via fin_cases, then close every goal with decide. The argument is finite arithmetic on bit-subtract/add over a 5-periodic grid; no intermediate lemmas beyond the definitions of the matching base cell and bit translation are required.
why it matters
Downstream, selectedCell5_eq_freudenthalExplicitFiberPairSelectedCell uses this recovery identity (via uniqueness of the periodic matching base cell) to equate the module's selected-cell map with the explicit-fiber pair selection from the external analysis. That equality is the bridge between the certificate's internal geometry and the fiber-endpoint audit.
The parent certificate checks every monomial coefficient in the corrected $N=5$ axis-stencil residual, a concrete gravity-side rational check in the RS discrete geometry stack. The $\mathrm{Fin},8$ indexing aligns with the eight-tick octave (T7). Without base-cell recovery, selected-cell uniqueness would not discharge.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.