nextIdx_8

The module Complex Structure Forcing shows that the eight-tick shift cannot be diagonalized over the reals, so complexification is algebraically forced. The setup rests on T7 (eight-tick octave): ledger states are read on a cyclic clock of length $2^3 = 8$.

nextIdx advances the reading index by one tick modulo 8: $\mathrm{next}(k) = (k+1)\bmod 8$ on $\mathrm{Fin},8$. The cyclic shift operator $T$ on eight-component signals is defined by $(Tf)(k) = f(\mathrm{next}(k))$. Iterating $T$ therefore iterates the index map.

This lemma is the pure index-level statement that eight advances close the cycle. It is the combinatorial engine behind the operator identity $T^8 = \mathrm{id}$.

Tactic proof by exhaustion: fin_cases k splits into the eight concrete residues $0,\ldots,7$. On each goal, decide evaluates the nested modular increments and checks equality with the starting index. No external lemmas are needed beyond the definition of nextIdx and decidable arithmetic on Fin 8.

Feeds directly into shift_period_8, the theorem that $T^8 = \mathrm{id}$ on eight-tick signals: that proof reduces pointwise to this index identity via congrArg f (nextIdx_8 k). The module doc frames $T^8 = I$ as step 1 of the complex-structure forcing argument (eigenvalues are 8th roots of unity; $\omega^2 = i$ has no real square root, so diagonalization over $\mathbb{R}$ fails).

In the Recognition forcing chain this is the concrete T7 periodicity of the recognition clock: the eight-tick octave that later forces complex Hilbert structure and unitarity of the recognition operator. Without period 8 at the index level, the eigenvalue and DFT-8 development in the same module does not start.