addBit_true_injective
plain-language theorem explainer
Advancing a cyclic index by one residue is injective on Fin N for every positive N. Lattice and triangulation authors cite it when proving that a true-bit coordinate shift on the periodic Freudenthal torus never collides vertices. The argument is a four-way wrap-around case split, each branch closed by omega after reducing the Fin equality to modular arithmetic.
Claim. For every positive integer $N$, the map $i \mapsto (i+1)\bmod N$ on the residues $\{0,\ldots,N-1\}$ is injective.
background
The module builds a typed periodic Freudenthal torus: vertices, edges, and tetrahedra on a scalable cyclic lattice, not yet a concrete finite mesh. Its goal is the global incidence/edge-slot partition required by the nonlinear Regge first-variation theorem, isolating the remaining encoder into finite index types.
Indices live in Fin N with N > 0. The helper bit sends false to 0 and true to 1. The operation addBit i b returns the residue class of i.val + bit b modulo N, so addBit i true is exactly the unit cyclic shift $i \mapsto (i+1)\bmod N$.
The same definitions and injectivity statement appear in the 4D companion module; the 3D proof is self-contained modular arithmetic on Fin values.
proof idea
Assume addBit i true = addBit j true. Project to underlying naturals to obtain (i.val + 1) % N = (j.val + 1) % N. Split on whether each of i.val + 1 and j.val + 1 is strictly less than N or equal to N (the only possibilities by omega). In each of the four branches, replace the modular expression by either the unwrapped sum or 0 via Nat.mod_eq_of_lt / Nat.mod_self, then finish with omega to force i.val = j.val, hence i = j after ext.
why it matters
This is the nontrivial half of coordinate-shift injectivity on the periodic torus. The parent theorem addBit_injective cases on the Boolean: the false branch is the identity, and the true branch is exactly this result. The identical lemma is reused in the 4D torus module.
Injective bit advances guarantee that flipping a single torus coordinate produces distinct vertices, which is required before one can assemble well-defined edges and tetrahedra and discharge the incidence/edge-slot partition demanded by the Regge first-variation setup. The module still leaves open the finite encoder from the typed periodic model into concrete Fin nV, Fin nE, Fin nT; this lemma is local plumbing toward that encoder, not the encoder itself.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.