addBit_true_eq_mk
plain-language theorem explainer
On the circular index set Fin N (N > 0), advancing a vertex index by the Boolean true bit equals the modular successor (i+1) mod N. Geometry and discrete-Regge authors cite it to simplify edge and tetrahedron incidence after a true-bit step. The proof is definitional reflexivity once bit true unfolds to 1.
Claim. For every positive integer $N$ and every index $i \in \{0,\ldots,N-1\}$, the circular advance of $i$ by the Boolean value $\mathsf{true}$ equals the residue class $(i+1)\bmod N$ (as an element of $\mathrm{Fin}\,N$).
background
The module builds a typed periodic Freudenthal torus: a scalable target shape for an arbitrary periodic Freudenthal tiling. It does not yet fix a concrete $n\times m\times k$ mesh; it defines vertices, edges, and tetrahedra on circular coordinates and proves that any finite triangulation encoding this model carries the global incidence/edge-slot partition required by the nonlinear Regge first-variation theorem.
Indices live in $\mathrm{Fin},N$ with $N\neq 0$. The helper bit sends Booleans to ${0,1}$. The operation addBit advances an index by that amount modulo $N$:
$\mathrm{addBit}(i,b)=\langle(i+\mathrm{bit},b)\bmod N,\ldots\rangle$.
When $b=\mathsf{true}$, $\mathrm{bit},b=1$, so the advance is exactly the modular successor. The same pattern appears in the 4D twin module.
proof idea
One-line reflexivity. Unfolding addBit and the definition of bit true (equal to 1) makes the two sides definitionally equal as $\mathrm{Fin},N$ pairs, so rfl closes the goal. Marked @[simp] for automatic rewriting.
why it matters
Small but load-bearing simp fact in the periodic Freudenthal geometry stack. Downstream the 4D module reuses the identical statement for its own circular coordinates. Together with the companion false-bit lemmas it lets incidence and displacement calculations reduce to ordinary modular arithmetic on vertex indices, which is exactly the algebra needed before a finite encoder into Fin nV, Fin nE, Fin nT can discharge the remaining scaffolding toward the Regge first-variation partition. It sits in the geometry layer that supports discrete curvature and eight-tick spatial structure (T7/T8), not in the forcing chain itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.