addBit_injective
plain-language theorem explainer
For any period N ≥ 1 and any Boolean bit b, modular translation of a cyclic coordinate by that bit is injective on Fin N. Lattice and triangulation authors cite it when lifting one-axis edge moves to injective vertex maps on the periodic Freudenthal 4-torus. The proof is a two-case split: false is the identity, true reuses the dedicated one-step injectivity lemma.
Claim. Let $N \ge 1$. For each bit $b \in \{\mathrm{false},\mathrm{true}\}$, the map $i \mapsto (i + [b]) \bmod N$ on $\mathrm{Fin}\, N$ is injective, where $[b]=0$ if $b$ is false and $[b]=1$ if $b$ is true.
background
The module constructs the typed periodic Freudenthal triangulation of the 4-torus used by the 4D metric-refinement reconstruction: four-coordinate periodic vertices, the fifteen positive-displacement edge classes of the 4-cube, and the Kuhn triangulation into $4!=24$ four-simplices. It is the self-contained 4D mirror of the 3D periodic Freudenthal torus carrier.
On each cyclic axis the primitive move is modular addition of a single bit. Writing $\mathrm{bit}(\mathrm{false})=0$ and $\mathrm{bit}(\mathrm{true})=1$, one defines $\mathrm{addBit}(i,b)=(i+[b])\bmod N$ on $\mathrm{Fin}, N$ (with $N\ne 0$). Injectivity of this one-coordinate map is the elementary combinatorial fact needed before multi-axis vertex translations can be shown injective.
The nontrivial half is already recorded as the true-bit injectivity lemma in the same geometry layer; the false-bit half is literally the identity.
proof idea
Term-mode case split on the Boolean bit. If the bit is false, $\mathrm{addBit}(-,\mathrm{false})$ is the identity on $\mathrm{Fin}, N$, so equal images simplify directly to equal preimages. If the bit is true, the goal is exactly the already-proved true-bit injectivity lemma, which is applied as a one-line citation.
why it matters
This lemma is the one-axis engine behind multi-bit injectivity on four-coordinate vertices: downstream, $\mathrm{addBits4_injective}$ reduces componentwise to four applications of this fact, and the 3D sibling $\mathrm{addBits_injective}$ uses the same pattern. Without injective edge translations, the finite encoder and the simpliciality evidence for the Kuhn 4-simplices on the periodic lattice would not be well-defined as combinatorial embeddings.
In the Recognition geometry stack the 4-torus carrier is the missing object named by the 4D recon for a $\mathrm{MetricRefinementFamily}$ instance. The result is pure finite combinatorics (no continuum limit, no metric yet), but it sits under the same forcing chain that fixes $D=3$ spatial dimensions and the eight-tick octave: here the fourth coordinate is the typed time/balance axis of the 4D carrier, kept deliberately separate from extending the 3D $\mathrm{BoundedComplex}$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.