subOneMod5
plain-language theorem explainer
Predecessor on the five-point circle: each index i in Fin 5 is sent to i−1 mod 5. The Freudenthal axis-stencil coefficient certificate uses it whenever a Boolean flag selects a one-step backward shift along a fiber coordinate. Implementation is the standard packing of (i+4) mod 5 into Fin 5, with the bound proved by omega.
Claim. For every index $i\in\{0,1,2,3,4\}$, return the unique $j\in\{0,1,2,3,4\}$ with $j\equiv i-1\pmod{5}$, equivalently $j=(i+4)\bmod 5$.
background
The ambient module is an exact rational certificate for the corrected Freudenthal axis-stencil residual at $N=5$. It mirrors a Python audit script and deliberately avoids floating-point arithmetic: every coefficient of an unordered monomial $\xi(u)\xi(v)$ in the mixed explicit-fiber residual is checked over the rationals.
Indices live in $\mathrm{Fin},5$, the cyclic five-point set that labels the discrete fiber. Sibling helpers already supply modular addition, negation, and edge translation on that set. The present map is the one-step backward generator of that cyclic action, needed when a stencil contribution is optionally shifted by a single fiber step.
proof idea
One-line definitional construction: form the natural number $(i.1+4)\bmod 5$ and pack it into $\mathrm{Fin},5$. The proof that the representative lies in ${0,1,2,3,4}$ is discharged by the omega tactic. No external lemmas are invoked.
why it matters
Direct consumer is the conditional shift subBit5, which applies the predecessor exactly when a Boolean bit is true and otherwise leaves the index fixed. That helper in turn feeds the commutation identity subBit5_addFin5, proving that the bit-controlled shift intertwines with modular translation of the base index. Together they let the certificate enumerate every monomial contribution to the $N=5$ axis-stencil residual without floating-point error, closing one discrete bookkeeping step in the gravity-sector audit of Recognition Science.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.