addBit
plain-language theorem explainer
Modular successor on a cyclic lattice index: add 0 or 1 to a residue class modulo N. Geometers building the periodic Freudenthal torus cite it as the one-step wraparound move along a single axis. The definition is the standard Fin constructor with Nat modular arithmetic and the NeZero positivity witness.
Claim. For $N \ge 1$ and $i \in \mathbb{Z}/N\mathbb{Z}$, and a bit $b \in \{0,1\}$, define $\mathrm{add}(i,b) := (i + b) \bmod N$ as an element of $\mathbb{Z}/N\mathbb{Z}$.
background
The module builds a typed periodic Freudenthal torus: vertices, edges, and tetrahedra on a product of cyclic lattices, without yet fixing a concrete finite mesh size. The remaining encoder work is to map this typed model into finite index types for the nonlinear Regge first-variation theorem and its incidence-edge-slot partition.
A vertex is a triple of residues in $\mathrm{Fin}, N_x \times \mathrm{Fin}, N_y \times \mathrm{Fin}, N_z$. Axis steps are Boolean: the helper bit sends false to 0 and true to 1. Adding a bit to one coordinate is the elementary wraparound translation used to generate cube displacements and edge incidences on the torus.
Upstream, only that Boolean-to-nat map is required. Everything else is ordinary modular arithmetic on a nonempty finite cyclic group.
proof idea
Definitional, not a proof. Unpack the Fin value, add bit b (0 or 1), reduce modulo N, and repack with the standard Nat.mod_lt bound from NeZero N. No lemmas beyond that positivity witness.
why it matters
This is the atomic cyclic shift for the periodic Freudenthal model. Downstream, addBits lifts it to simultaneous $(dx,dy,dz)$ moves on a 3D vertex; simp lemmas (addBit_false, addBit_true_eq_mk, composition identities) and injectivity (addBit_injective, addBit_true_injective) feed edge and tetrahedron incidence constructions.
In the broader Recognition geometry stack, the torus is the scalable target shape whose finite encodings must carry the global incidence partition needed by the nonlinear Regge first-variation theorem. Isolating wraparound addition here keeps the typed periodic combinatorics separate from any concrete $n \times m \times k$ mesh encoder still left open by the module doc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.