two_bit_steps_ne_id
plain-language theorem explainer
On a cyclic grid of length N>2, two successive unit-or-zero steps return to the start only if both steps are zero. Anyone proving that oriented edges of the periodic Freudenthal 4-torus cannot reverse will cite this. The proof is exhaustive Bool casework plus modular arithmetic, using that a single true step never fixes a vertex.
Claim. Let $N>2$ be a positive integer and $x\in\mathbb{Z}/N\mathbb{Z}$. Write $\mathrm{addBit}(x,b)=x+[b=\mathrm{true}]\bmod N$. If $\mathrm{addBit}(\mathrm{addBit}(x,b_1),b_2)=x$, then $b_1=b_2=\mathrm{false}$.
background
The module constructs the typed periodic Freudenthal triangulation of the 4-torus: four-coordinate vertices on a side-$N$ grid, the fifteen positive-displacement edge classes of the 4-cube, and the Kuhn triangulation into $4!=24$ four-simplices. It is the 4D mirror of the 3D periodic Freudenthal torus, kept self-contained because the existing bounded complex only admits tetrahedra.
Coordinate motion along one axis is encoded by addBit: on $\mathrm{Fin},N$ it adds $0$ or $1$ according to a Boolean flag, reduced mod $N$. The identity law addBit_false says a false flag is a no-op. The companion fact addBit_true_ne_self (under $N>2$) says a true flag never fixes a vertex. Together these control when a short walk on a single coordinate can close.
The ambient arithmetic is ordinary modular arithmetic on $\mathbb{N}$ (associativity of addition and transitivity of $<$), not the Recognition-calculus naturals; those appear only as ambient imports.
proof idea
Introduce the closing hypothesis and case-split on the two Booleans.
- Both false:
simpwithaddBit_falsereduces the goal to reflexivity. - Exactly one true: rewrite the false step away, then apply
addBit_true_ne_self(needs $N>2$) to obtain a contradiction. - Both true: project to underlying values to get $((x+1)\bmod N+1)\bmod N=x$. Split on whether $x+1<N$ or $x+1=N$. In the interior branch, reduce to $(x+2)\bmod N=x$ and split again on $x+2$ vs $N$; both subcases yield $2=0$ or a wrap to $0$ that forces $x\equiv 0$ incompatibly with $N>2$. On the wrap $x+1=N$, the equation collapses to $1\bmod N=x\bmod\cdots$, and $1\bmod N=1$ (since $1<N$) again contradicts by
omega.
No induction; pure finite case analysis and modular reduction.
why it matters
Feeds directly into reverse_impossible4, which asserts that no two periodic 4-edges can share the same unordered endpoints with opposite orientation. That non-reversal fact is part of the combinatorial hygiene of the 4D Freudenthal carrier: edges are positive-displacement classes of the 4-cube, so a reverse pair would break the oriented simplicial structure used by the Kuhn tables and the endpoint-incidence theorem.
In the broader Recognition geometry stack this sits under the 4D metric-refinement recon: the typed 4-torus is the missing carrier named for the 4D MetricRefinementFamily. The lemma itself is local and combinatorial; it does not touch the forcing chain (T0–T8), the J-cost, or the eight-tick octave. It closes a small but necessary gap so that later assembly (period-doubling projection, Gap2 instance) can treat edges as irreversibly oriented without extra casework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.