addVertexBits_injective
plain-language theorem explainer
On a nonempty periodic cubic lattice, translating every vertex by a fixed 3-bit offset labeled by Fin 8 is an injective self-map. Anyone proving bijectivity of Freudenthal cell translations or uniqueness of base cells cites this. The proof unfolds the Fin-8 packaging and reuses injectivity of the underlying Boolean triple shift.
Claim. Let $N_x,N_y,N_z\ge 1$. Write $V=\mathbb{Z}/N_x\mathbb{Z}\times\mathbb{Z}/N_y\mathbb{Z}\times\mathbb{Z}/N_z\mathbb{Z}$ for the periodic cubic vertices. For each fixed $a\in\{0,\ldots,7\}$, the map $v\mapsto v+\mathrm{bits}(a)$ on $V$ (componentwise modular addition of the three Boolean bits encoded by $a$) is injective.
background
The module builds a typed periodic Freudenthal torus: vertices, edges, and tetrahedra on a scalable $N_x\times N_y\times N_z$ cubic lattice, isolating the combinatorial model needed so any finite encoder into a Triangulation3D inherits the incidence/edge-slot partition used by the nonlinear Regge first-variation theorem.
Vertices are triples in $\mathrm{Fin},N_x\times\mathrm{Fin},N_y\times\mathrm{Fin},N_z$. The eight Freudenthal subcell offsets are indexed by $\mathrm{Fin},8$; vertexBits unpacks each index into a Boolean triple, and addVertexBits applies the corresponding modular shift via addBits.
Upstream, addBits_injective already shows that any fixed Boolean triple shift is injective on $V$ (by componentwise cancellation on the three $\mathrm{Fin}$ factors, using $N_i\ne 0$). The present statement is the same fact packaged through the $\mathrm{Fin},8$ labeling.
proof idea
Term-mode one-liner after a short intro. Assume two vertices map to the same image under addVertexBits (·) a. Unfold the definition so the hypothesis becomes equality after addBits with the three bits of vertexBits a. Conclude by addBits_injective on that Boolean triple.
why it matters
Injectivity is the hard half of bijectivity for the eight Freudenthal offsets on a finite torus. Downstream, addVertexBits_surjective obtains surjectivity from finiteness plus this injectivity; existsUnique_addVertexBits_eq then gives a unique base cell for each target and offset; sum_ite_eq_of_addVertexBits collapses indicator sums over that unique cell to a constant, the bookkeeping step for discrete variational identities.
In the Recognition geometry stack this supports the periodic Freudenthal model that feeds incidence partitions for Regge first variation. It is pure lattice combinatorics (no forcing-chain T0–T8 content), but it closes a necessary algebraic lemma on the path from typed torus to a finite mesh encoder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.