addBitTrueComparable5
plain-language theorem explainer
On a five-periodic coordinate, adding one tick keeps the result order-comparable to the start: either the step advances without wrap, or it wraps 4→0. Gravity auditors of the N=5 Freudenthal axis stencil cite this when checking endpoint order on axis edges. The proof is an exhaustive five-way case split discharged by decide.
Claim. For every $i \in \{0,1,2,3,4\}$, writing $i\oplus 1 := (i+1)\bmod 5$, one has $i \le i\oplus 1$ or $i\oplus 1 \le i$ in the standard order on $\mathrm{Fin}\,5$.
background
The module certifies rational coefficients in the corrected $N=5$ mixed explicit-fiber axis-stencil residual on the periodic Freudenthal torus, matching an exact Python audit with no floating point.
Coordinates live in $\mathrm{Fin},5$. The bit-step addBit sends $i$ to $(i + b)\bmod N$ for a Boolean bit $b$; here $b=\mathrm{true}$ is the unit tick. Comparability is the usual total order on residues ${0,1,2,3,4}$, not a product order yet: that appears only when three coordinates are assembled into a vertex.
Upstream, the same addBit is defined for general $N$ on the periodic Freudenthal torus (and its 4D variant). Downstream geometry packages axis edges as a base vertex plus a pure-axis displacement built from these bit steps.
proof idea
Tactic proof: fin_cases i splits into the five concrete residues $0..4$, then decide closes each Boolean disjunction by computation. No lemmas are invoked; the statement is a finite arithmetic fact about modular successor on $\mathrm{Fin},5$.
why it matters
Feeds axisEdgeEndpointsComparable5, which lifts the one-coordinate fact to both endpoints of a pure-axis edge on the $N=5$ periodic torus (product order on Vertex5). That parent remains useful for local geometry audits even though the full coefficient expansion now routes through vertex5CanonLE for every unordered pair.
In the Recognition gravity stack this sits inside the corrected Freudenthal axis-stencil certificate: every unordered monomial $\xi(u)\xi(v)$ in the residual must have a certified rational coefficient. Order-comparability of axis endpoints is a small but necessary bookkeeping step so endpoint pairs can be normalized before the monomial audit. It is local discrete geometry, not a forcing-chain (T0–T8) step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.