addVertexBits
plain-language theorem explainer
Translates a base cell on the periodic Nx×Ny×Nz cubic lattice by one of the eight binary cube-corner offsets labeled by Fin 8. Anyone building Freudenthal tetrahedra, local edges, or incidence data on the torus cites it as the cell-to-vertex map. The body is a thin composition: decode the Fin 8 label to three Bools, then apply coordinatewise modular addBit.
Claim. On the periodic lattice $\mathrm{Vertex}(N_x,N_y,N_z)=\mathrm{Fin}\,N_x\times\mathrm{Fin}\,N_y\times\mathrm{Fin}\,N_z$ (with each $N_i\ge 1$), given a base cell $v$ and a cube-corner label $a\in\{0,\ldots,7\}$, return the vertex obtained by adding the three Boolean offsets of $a$ (the binary cube coordinates) to the three coordinates of $v$, each addition taken modulo the corresponding period.
background
The module supplies the typed periodic target for Freudenthal tilings: vertices, edges, and the six-tetrahedron decomposition of each unit cube, without yet fixing a concrete finite mesh encoding. Vertices are triples of modular indices. The eight corners of the unit cube are labeled by Fin 8 and decoded by vertexBits into Boolean triples (binary cube coordinates).
Coordinatewise displacement is addBits, which applies addBit on each Fin N_i factor: false leaves the index fixed, true advances it by one modulo $N_i$. The present map packages those two steps so that every local cube corner relative to a base cell is a single call.
This sits upstream of the incidence and edge-slot partition needed by the nonlinear Regge first-variation theorem on any finite triangulation that encodes the periodic model.
proof idea
Definitional one-liner. Unpack $a:\mathrm{Fin},8$ via vertexBits to a triple of Booleans, then feed that triple to addBits on the base vertex. No lemmas or tactics; pure composition of the two sibling helpers.
why it matters
This is the primitive cell-to-corner translation used throughout the periodic Freudenthal model. Downstream, injectivity and surjectivity of the map (for fixed corner label) give unique base-cell recovery; existsUnique_addVertexBits_eq packages that uniqueness. Canonical tetrahedron vertex maps and localEdgeOf build global tet vertices and translated edges by calling it on Freudenthal local offsets. Those feed the encoded periodic torus whose incidence edge-slot partition is the geometric input to the nonlinear Regge first-variation theorem. In the broader RS geometry stack it realizes the discrete cubic skeleton on which the eight-tick / $D=3$ forcing eventually sits, though this declaration itself is pure lattice bookkeeping.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.