addBit_injective
plain-language theorem explainer
Adding a single boolean offset (0 or 1) modulo N is injective on the cyclic index set Fin N. Anyone assembling periodic Freudenthal vertex displacements cites this to guarantee one-coordinate bit flips never collide. The proof cases on the bit: the zero offset is the identity, and the +1 case invokes the already-proved modular successor injectivity.
Claim. For every positive integer $N$ and every bit $b\in\{0,1\}$, the map $i\mapsto (i+b)\bmod N$ on $\{0,\ldots,N-1\}$ is injective.
background
The module builds a typed periodic Freudenthal torus: a scalable vertex/edge/tetrahedron model whose any finite triangulation encoding must carry the global incidence-edge-slot partition required by the nonlinear Regge first-variation theorem. Concrete $n\times m\times k$ meshes are deferred; the typed model isolates the encoder work.
Indices live in $\mathrm{Fin},N$ with $N>0$. The helper $\mathrm{bit}$ sends false to 0 and true to 1. The one-step wrap map is $\mathrm{addBit}(i,b)=(i.\mathrm{val}+\mathrm{bit},b)\bmod N$. The nontrivial half, injectivity of $+1\bmod N$, is already recorded as a sibling lemma; the present statement packages both bits uniformly so multi-coordinate shifts can quote a single fact.
proof idea
Case-split on the boolean. When the bit is false, $\mathrm{addBit}(\cdot,\mathrm{false})$ is definitionally the identity on $\mathrm{Fin},N$, so injectivity is immediate by simplification of the equality hypothesis. When the bit is true, the claim is exactly the sibling lemma that $i\mapsto(i+1)\bmod N$ is injective, applied verbatim.
why it matters
Parent use is the three-coordinate statement that simultaneous boolean offsets $(d_x,d_y,d_z)$ act injectively on torus vertices: that proof reduces coordinatewise to this lemma. The same pattern is mirrored in the 4D torus module for four-bit vertex shifts. Together these injectivity facts underwrite that periodic Freudenthal displacements label distinct vertices, which is required before the incidence-edge-slot partition can be assembled for the Regge first-variation theorem. In the broader RS geometry stack this sits under the $D=3$ spatial forcing (T8) and the eight-tick discrete period, supplying the discrete torus on which those structures live. No open scaffold remains here; the result is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.