addBit_false_after_true
plain-language theorem explainer
Adding a true bit then a false bit to a periodic index equals adding only the true bit. Anyone simplifying Freudenthal torus vertex walks or edge displacements cites this. The proof is a one-line simp wrapper over the modular definition of bit addition.
Claim. For any positive integer $N$ and any index $i \in \mathbb{Z}/N\mathbb{Z}$, if $\mathrm{addBit}(i,b)$ means $i$ advanced by the integer value of the boolean $b$ modulo $N$, then $\mathrm{addBit}(\mathrm{addBit}(i,\mathrm{true}),\mathrm{false}) = \mathrm{addBit}(i,\mathrm{true})$.
background
The module builds a typed periodic Freudenthal torus: the scalable target shape for an arbitrary periodic Freudenthal tiling. It does not yet pin a concrete finite $n \times m \times k$ mesh; it defines vertices, edges, and tetrahedra so that any finite Triangulation3D encoding the model carries the global incidence partition needed by the nonlinear Regge first-variation theorem.
Indices live in $\mathrm{Fin}, N$ with $N \neq 0$. The helper $\mathrm{addBit}, i, b$ advances $i$ by the integer value of the boolean $b$ (0 for false, 1 for true) and reduces modulo $N$. Sibling lemmas record the other absorption and non-fixed-point identities for the same walk.
The same identity is mirrored in the 4D periodic torus module, which reuses this 3D bit arithmetic as a building block.
proof idea
One-line wrapper: simp unfolds addBit twice and reduces the arithmetic. Because the false bit contributes 0, the second modular addition is the identity on the already-advanced residue, so both sides normalize to the same Fin pair.
why it matters
Bit walks on the periodic lattice generate the discrete displacements that label edges and tetrahedra in the Freudenthal model. This absorption law keeps those walks idempotent under a trailing false step, which is exactly the simplification the 4D twin lemma and the larger addBits / dispBits stack need when normalizing vertex codes.
Downstream, the 4D module copies the same statement so that four-dimensional periodic Freudenthal data inherit the same simp normal form. In the broader Recognition geometry chain, clean torus arithmetic is a prerequisite for encoding a finite triangulation that satisfies the incidence partition used by the nonlinear Regge first-variation theorem; the remaining open work flagged by the module is the finite encoder into Fin nV, Fin nE, Fin nT.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.