addBits
plain-language theorem explainer
Componentwise modular shift of a periodic cubic vertex by three boolean steps (0 or 1 along each axis). Geometry and gravity code cite it whenever a Freudenthal edge or stencil needs the far endpoint of a unit cube displacement on the torus. The body is a three-line product of the 1D wrap-around adder.
Claim. On the periodic lattice $\mathrm{Fin}\,N_x\times\mathrm{Fin}\,N_y\times\mathrm{Fin}\,N_z$ (each $N_\bullet\ge 1$), given a vertex $v$ and bits $d_x,d_y,d_z\in\{0,1\}$, return the vertex whose $i$-th coordinate is $v_i+d_i$ taken modulo $N_i$.
background
The module builds a typed periodic Freudenthal torus: vertices, positive-displacement edges, and tetrahedra on an $N_x\times N_y\times N_z$ cubic lattice with wrap-around, as the scalable target shape for any finite triangulation that must carry the incidence partition used by nonlinear Regge first variation.
A periodic cubic vertex is just a triple of modular indices. The 1D helper adds a boolean bit (0 or 1) to a single Fin N coordinate and reduces modulo $N$, which is well-defined once $N\ne 0$. The three-axis map applies that helper independently on each factor.
This is the elementary translation step underlying seven-class cube displacements, local edge endpoints, and later stencil shifts in the gravity analysis layer.
proof idea
Definition, not a proof. Unpack the vertex triple and apply the 1D modular adder on each coordinate with the matching boolean displacement; reassemble the triple. No lemmas are invoked beyond the well-typedness of the 1D adder (mod-$N$ residual is in range because $N>0$).
why it matters
This is the primitive translation used everywhere the periodic model moves along a cube edge. Downstream, injectivity of the map for fixed bits is proved separately; the eight-corner cube walk is built by decoding a Fin 8 into three bits and calling this map; periodic edges store a base vertex plus a positive displacement whose far endpoint is obtained the same way.
Gravity analysis reuses it for stencil shifts and moment-tensor witnesses on the sampled field (seven-class weights $1,\sqrt{2},\sqrt{3}$), and Regge/TT Bloch assembly tracks vertex coordinates after bit shifts. In the broader RS geometry stack it supports the D=3 Freudenthal scaffolding that feeds the incidence partition required by the nonlinear Regge first-variation theorem; the remaining open work named by the module is a finite encoder into Fin nV, Fin nE, Fin nT.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.