addBit_add_right
plain-language theorem explainer
Bit-increment on a coordinate of the periodic circle Z/NZ commutes with translation: adding a Boolean step after shifting by s equals shifting the bit-incremented value by s. Anyone building translation-equivariant edge or vertex maps on the Freudenthal torus cites this. The proof is a short Fin-extensionality argument reducing to modular arithmetic and right-commutativity of natural addition.
Claim. Let $N \ge 1$. For $i,s \in \mathbb{Z}/N\mathbb{Z}$ and $b \in \{0,1\}$, writing $\mathrm{addBit}(i,b) = i + b \bmod N$, one has $\mathrm{addBit}(i+s,\,b) = \mathrm{addBit}(i,\,b) + s$ in $\mathbb{Z}/N\mathbb{Z}$.
background
The ambient module records path-sum probes on the canonical periodic Freudenthal torus, packaged as a BoundedComplex for the Seven Gaps program. It makes no continuum or measure claims; it only attaches the torus geometry and checks that the translation group embeds into relabeling automorphisms (probe C6).
On each periodic axis the helper addBit sends a residue $i \in \mathrm{Fin},N$ and a Boolean $b$ to $i$ plus the bit value of $b$, reduced mod $N$. Componentwise application yields addBits on vertices $\mathrm{Fin},N \times \mathrm{Fin},N \times \mathrm{Fin},N$. Translation of vertices is componentwise modular addition.
The present lemma is the one-dimensional commutation fact that bit-increment intertwines with that modular translation. Upstream, addBit is defined by the modular formula above; the proof also unfolds Fin.add_def (value-wise addition mod $N$).
proof idea
Term-mode proof by ext on the underlying natural values of the two Fin N sides. Unfold addBit and Fin.add_def, then apply Nat.mod_add_mod so both sides become a single modular sum of three naturals (the coordinate, the bit, and the shift). Finish with add_right_comm to reorder the bit past the shift inside ordinary natural addition; the moduli match, so the Fin values agree.
why it matters
This is the coordinate-wise engine for addBits_add_right, which states that Boolean cube displacements commute with full vertex translation on the periodic torus. That three-dimensional commutation is part of the algebraic backbone of probe C6: showing that the translation group $\mathbb{Z}_N^3$ embeds into the automorphism monoid of the Freudenthal image complex (translationAut injective, unital, and additive).
In the Seven Gaps gravity lane the embedding yields concrete bounds such as $|\mathrm{Aut}(T_N)| \ge N^3$ and $\mu(T_N) \le 1/N^3$. Without bit-translation commutation, edge and tet incidence maps would not be translation-equivariant, and the Aut-vacuity landmine check would fail. The lemma is pure finite modular arithmetic; it does not itself touch continuum limits or path-sum values.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.