addBits_injective
plain-language theorem explainer
Componentwise Boolean displacements on the periodic cubic lattice act injectively on vertices. Anyone building edge or cube orbits on the Freudenthal torus cites this to keep distinct lattice points distinct after a fixed (dx,dy,dz) shift. The proof is a three-line product argument: injectivity of the one-dimensional bit shift on each Fin factor.
Claim. Let $N_x,N_y,N_z\ge 1$ and fix Boolean displacements $d_x,d_y,d_z\in\{0,1\}$. On the periodic vertex set $\mathrm{Fin}\,N_x\times\mathrm{Fin}\,N_y\times\mathrm{Fin}\,N_z$, the map sending a vertex $v$ to the componentwise bit-shift of $v$ by $(d_x,d_y,d_z)$ is injective.
background
The module builds the typed periodic Freudenthal torus: a scalable vertex/edge/tetrahedron model whose finite encodings must carry the global incidence-edge-slot partition used by the nonlinear Regge first-variation theorem. Vertices are simply the product lattice $\mathrm{Fin},N_x\times\mathrm{Fin},N_y\times\mathrm{Fin},N_z$ (each factor nonzero).
A one-dimensional bit shift addBit either leaves an index alone (false) or advances it by one modulo $N$ (true). The three-dimensional map addBits applies that shift independently on each coordinate. Upstream, injectivity of the one-dimensional shift is already proved by case split on the Boolean: the false case is the identity, the true case uses the modular successor injectivity lemma.
proof idea
Term-style proof by unpacking both vertices into coordinate triples, simplifying the definition of the three-dimensional shift, and feeding each coordinate equality into the one-dimensional injectivity lemma. The three resulting equalities reassemble to vertex equality. No extra arithmetic is needed beyond the product structure.
why it matters
Feeds directly into addVertexBits_injective, which lifts the same idea from a single Boolean triple to the eight cube-corner labels in $\mathrm{Fin},8$. That injectivity is part of the incidence bookkeeping that any finite encoder of the periodic torus into Fin nV, Fin nE, Fin nT must preserve so the global edge-slot partition remains well-defined for the Regge first-variation theorem. In the broader geometry stack this is scaffolding for the $D=3$ spatial lattice (forcing chain T8), not a physics identity itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.