subBit5
plain-language theorem explainer
Conditional decrement on the cyclic index set of size 5: if the control bit is true, subtract one modulo 5; otherwise leave the index fixed. Gravity auditors of the corrected N=5 Freudenthal axis-stencil residual use it to flip coordinate bits when matching base cells. The body is a one-line boolean branch over the modular predecessor.
Claim. For an index $i \in \{0,1,2,3,4\}$ and a bit $b\in\{\mathrm{true},\mathrm{false}\}$, return $i-1\pmod{5}$ when $b$ is true and return $i$ unchanged when $b$ is false.
background
The ambient 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 never uses floating-point arithmetic.
Indices live in $\mathrm{Fin},5$, the cyclic group of order 5. The sibling predecessor map sends $i$ to $(i+4)\bmod 5$, i.e. subtracts one modulo 5. Vertices are triples of such indices; edges and translations are built from the same modular arithmetic.
The present map packages that predecessor behind a boolean switch so that a bit pattern can selectively decrement each coordinate of a target vertex.
proof idea
Pure definitional branch: if the bit is true, apply the modular predecessor $(i+4)\bmod 5$; otherwise return $i$. No lemmas are invoked at the definition site.
why it matters
It is the coordinate-wise primitive used by the matching-base-cell map, which, given an 8-bit address and a target vertex in $(\mathrm{Fin},5)^3$, decrements each coordinate exactly when the corresponding address bit is set. That matching step is part of the exact rational certificate for the corrected Freudenthal axis-stencil residual.
It also feeds the commutation identity that the bit-controlled decrement intertwines with modular translation: decrementing after translating equals translating after decrementing. Together these facts keep the stencil residual bookkeeping exact on the five-point cyclic fiber, which is the discrete geometry underlying the gravity-side certificate in this module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.