addBit
plain-language theorem explainer
On a cyclic coordinate of length N>0, add a Boolean step of 0 or 1 and wrap modulo N. Anyone building periodic lattice vertices or positive cube displacements on the Freudenthal torus cites this. The body is a one-line Fin constructor: value plus bit, reduced mod N, with the standard remainder bound.
Claim. Fix $N\in\mathbb{N}$ with $N\neq 0$. For $i\in\{0,\ldots,N-1\}$ and $b\in\{\mathrm{false},\mathrm{true}\}$, define the modular step $\mathrm{add}(i,b):=(i+[b])\bmod N$, where $[\mathrm{false}]=0$ and $[\mathrm{true}]=1$. The result is again an element of $\{0,\ldots,N-1\}$.
background
The module constructs the typed periodic Freudenthal triangulation of the 4-torus: 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 4D mirror of the 3D periodic Freudenthal torus and deliberately defines its own carrier rather than extending the tetrahedron-only bounded complex.
Each spatial axis is a cyclic index in $\mathrm{Fin},N$ with $N\neq 0$. The helper $\mathrm{bit}:\mathrm{Bool}\to\mathbb{N}$ sends false to 0 and true to 1. Modular addition of that bit is the elementary move used to step a single coordinate while staying on the periodic lattice.
The same definition already exists in the 3D module; the 4D file reintroduces it so the 4D carrier stays self-contained.
proof idea
Pure definition, not a proved theorem. Unpack $i$ to its underlying natural, add $\mathrm{bit},b\in{0,1}$, reduce modulo $N$, and repackage as $\mathrm{Fin},N$ using $\mathrm{Nat.mod_lt}$ together with positivity of $N$ from the $\mathrm{NeZero}$ instance. No lemmas beyond the standard remainder bound are invoked.
why it matters
This is the atomic coordinate step for the periodic Freudenthal lattice. Downstream it feeds the multi-axis displacement map that sends a vertex $(x,y,z)$ (or its 4D analog) by independent Boolean increments on each axis, and the suite of simplification and injectivity lemmas (false is identity, true is injective, mixed true/false reductions). Those lemmas underwrite positive cube edge classes and the Kuhn corner tables that the 4D recon named as the missing carrier for metric refinement.
In the broader Recognition geometry stack this sits under the mesh and period-doubling machinery that eventually supports the 4D metric-refinement family; it does not itself touch forcing-chain landmarks (T5–T8) or the J-cost, but it is the lattice primitive those geometric layers assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.