addBit_false
plain-language theorem explainer
Adding the zero bit leaves any periodic coordinate fixed. Geometry and gravity proofs that shift vertices on the N-periodic Freudenthal torus cite this as a simp rule when a displacement class carries no step. Proof is Fin extensionality plus the elementary fact that (i+0) mod N equals i when i < N.
Claim. For every positive integer $N$ and every residue $i \in \{0,\ldots,N-1\}$, the modular shift of $i$ by the Boolean value false (read as the integer $0$) equals $i$ itself.
background
The module builds a typed periodic Freudenthal torus: vertices are triples of residues in $\mathrm{Fin},N$, and edges are generated by Boolean bit displacements along coordinate axes (and diagonals). The local goal is a scalable periodic model whose finite encodings inherit the incidence partition needed by the nonlinear Regge first-variation theorem.
Two tiny helpers sit under the theorem. The map bit sends false to $0$ and true to $1$. The map addBit adds that integer to a residue and reduces modulo $N$, producing another element of $\mathrm{Fin},N$. Shifts of vertices and stencil displacements are built by applying addBit coordinatewise, so the false case is the identity step on that axis.
proof idea
Term-mode proof by ext on the underlying natural number of the Fin N value. Unfold addBit and bit: the right-hand side is $(i.val + 0) \bmod N$. Because $i.val < N$, Nat.mod_eq_of_lt collapses the modulus, yielding $i.val$, hence equality of the Fin values. Marked @[simp] so later shift lemmas discharge the no-step case automatically.
why it matters
Parent uses sit in the gravity layer. stencil_inner_sum_witness evaluates the seven-class Freudenthal stencil on a sampled witness field: classes with no first-coordinate step must contribute zero, and the identity action of a false bit is exactly that no-step case. axisEdgeEndpointsComparable5 compares endpoints of axis edges on the $N=5$ torus; its case split on axis displacements unfolds addBits/dispBits, which reduce through this identity.
In the broader Recognition geometry stack this is scaffolding hygiene for the periodic torus that feeds Regge energy and moment-tensor identities, not a forcing-chain landmark. It closes a trivial but repeatedly hit branch so the nonlinear first-variation and stencil-coefficient certificates stay simp-driven rather than ad hoc.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.