subBit5_addFin5
plain-language theorem explainer
Conditional unit subtraction on Fin 5 commutes with modular translation: subtracting a bit after adding a equals adding a after subtracting the bit. Gravity auditors cite it when moving matching base cells under lattice translation in the N=5 Freudenthal axis-stencil residual. The proof is a two-case boolean split, then simp and omega on the underlying modular arithmetic.
Claim. For all $a,i\in\mathbb{Z}/5\mathbb{Z}$ and $b\in\{\mathrm{false},\mathrm{true}\}$, writing $i\ominus b$ for $i$ if $b$ is false and $i-1\pmod{5}$ if $b$ is true, one has $(a+i)\ominus b = a+(i\ominus b)$.
background
The module certifies every unordered monomial coefficient in the corrected $N=5$ mixed explicit-fiber axis-stencil residual for the Freudenthal construction. It mirrors an exact rational Python audit and uses no floating-point arithmetic.
Indices live in $\mathrm{Fin},5$, i.e. $\mathbb{Z}/5\mathbb{Z}$. Modular addition is addFin5: $(i+j)\bmod 5$. Unit subtraction is subOneMod5: $i\mapsto(i+4)\bmod 5$. The bit map subBit5 applies that unit subtraction when the boolean is true and is the identity otherwise. These are the elementary lattice moves used to translate vertices and edges on the five-point periodic cell.
proof idea
Case-split on the boolean $b$. In each branch, unfold the definitions of bit-subtraction, unit subtraction, and modular addition, then use ext to compare the underlying natural numbers in $\mathrm{Fin},5$. The resulting equalities of residues modulo 5 are discharged by omega. No external lemmas beyond those three local definitions are required.
why it matters
The identity is the coordinate-wise engine behind matchingBaseCell5_translate, which states that matching a base cell after translating a target vertex equals translating the already-matched cell. That translation covariance is needed so the axis-stencil residual coefficients are well-defined on the periodic five-cell and independent of base-point choice.
In the broader Recognition gravity stack this sits inside the exact rational certificate for the corrected Freudenthal fiber endpoint analysis. It is pure finite-group bookkeeping, not a physical law, but without it the stencil coefficient audit cannot move freely on the lattice.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.