addBit_true_after_false
plain-language theorem explainer
On the circular index set Fin N, stepping by the false bit and then the true bit equals a single true-bit step. Anyone simplifying bit-walks on the periodic Freudenthal torus cites this. The proof is a one-line simp reduction of modular arithmetic on the underlying natural.
Claim. For every positive integer $N$ and every index $i \in \mathrm{Fin}\, N$, adding the false bit and then the true bit equals adding the true bit alone: $\mathrm{addBit}(\mathrm{addBit}(i,\mathsf{false}),\mathsf{true}) = \mathrm{addBit}(i,\mathsf{true})$.
background
The module builds a typed periodic vertex/edge/tetrahedron model for an arbitrary periodic Freudenthal tiling. It does not yet pin a concrete finite mesh; it isolates the encoder work needed so any finite Triangulation3D of this model carries the IncidenceEdgeSlotPartition used by the nonlinear Regge first-variation theorem.
Indices live in Fin N with N nonzero. The helper bit maps Bool to {0,1}, and addBit advances an index by that amount modulo N: addBit(i,b) = (i.val + bit b) mod N. False therefore leaves the index fixed; true advances it by one wrap-around step. Sibling lemmas record the other compositions (false after true, true after true, etc.).
proof idea
One-line wrapper: simp unfolds addBit and bit, then reduces (i + 0 + 1) mod N to (i + 1) mod N by the standard Nat modular arithmetic simp set. No custom lemmas are invoked beyond the definitional expansion of addBit.
why it matters
Bit-step identities keep torus walks and edge displacements normal-form under simp, which is required when building vertexBits, dispBits, and addVertexBits on the periodic Freudenthal model. The 4D twin module reuses the same statement verbatim for its own circular indices. Within the geometry stack this is scaffolding for the finite encoder into Fin nV / Fin nE / Fin nT that closes the path from the typed torus to the Regge first-variation hypotheses. It is local arithmetic, not a forcing-chain landmark, but without clean bit algebra the periodic incidence partition cannot be stated.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.