addBit_true_ne_self

The module supplies the scalable typed model for a periodic Freudenthal tiling: vertices, positive-displacement edges, and tetrahedra on a product of circular coordinates, without yet enumerating a concrete finite mesh. Its goal is the global incidence/edge-slot partition required by the nonlinear Regge first-variation theorem; the remaining work is a finite encoder into Fin indices.

Coordinates live in Fin N. The helper that sends false to 0 and true to 1 turns a Boolean into a unit step, and advancing a coordinate by that step modulo N is the elementary circular shift used to build positive cube displacements. The present lemma is the elementary non-degeneracy fact for a single true step.

Assume for contradiction that advancing i by one modulo N returns i. Projecting to underlying naturals yields $(i+1)\bmod N = i$. Split on whether $i+1 < N$ or $i+1 = N$. In the first branch the modulus is inert, so $i+1 = i$, absurd. In the second branch the modulus collapses to 0, so $0 = i$, which with $N > 2$ and $i+1 = N$ is again absurd. Both contradictions are finished by omega.

Non-degeneracy of a single true bit-step is the first filter that positive-displacement edges are genuine edges (base vertex distinct from tip). It is consumed when assembling the periodic-edge structure (base vertex plus one of seven positive cube displacements) and, in the four-dimensional sibling module, when assembling 4-edges and when proving that two successive bit-steps recover the identity only if both bits are false.

Within the Recognition geometry stack this is pure scaffolding for the Freudenthal torus that will eventually feed the Regge first-variation theorem; it does not itself touch the forcing chain (T0–T8), the J-cost, or the phi-ladder. It closes a tiny but mandatory algebraic gap so that later incidence and partition arguments can treat single-bit edges as irreflexive.