nextIdx
plain-language theorem explainer
Advances a reading index on the eight-tick cycle by one step modulo 8. Anyone defining the discrete time-evolution generator on Signal8 cites this. The body is a one-line Fin constructor: add one and reduce mod 8, with a trivial bound proof.
Claim. For each index $k \in \{0,1,\ldots,7\}$, the successor index is $(k+1)\bmod 8$, returned as an element of the same eight-point set.
background
The module Complex Structure Forcing shows that the eight-tick shift cannot be diagonalized over the reals, so complexification is algebraically forced. T7 supplies a cyclic period-8 evolution on the ledger state space; the discrete generator is the cyclic shift $T$ with $T^8 = I$.
Signal8 is the space of real (later complex) assignments on eight ticks. The fundamental RS time quantum is one tick ($\tau_0 = 1$). The successor map on indices is the combinatorial skeleton of $T$: reading at $k$ after one tick means reading the original signal at the next index.
Upstream constants fix the tick unit; the sibling shift is defined by $(Tf)(k) = f(\mathrm{next}(k))$. The OperatorCore layer re-exports this same successor for the forcing-chain bridge.
proof idea
Pure definition, not a theorem. Unpack the Fin 8 value, add one, reduce modulo 8, and repack with the standard Nat.mod_lt bound (discharged by norm_num on the constant 8). No lemmas beyond modular arithmetic are required.
why it matters
This is the atomic step behind the canonical cyclic shift. Downstream, shift is $(Tf)(k) = f(\mathrm{next}(k))$, shiftIter iterates it, and nextIdx_8 proves eight applications return the start, feeding the theorem $T^8 = \mathrm{id}$.
The UnifiedForcingChain bridge T7_To_CanonicalShift_Bridge names the defining equation of the cyclic shift as advance-by-one-tick on Fin 8; that equation is literally this successor. Framework landmark: T7 (eight-tick octave, period $2^3$). Closing the complex-structure gap depends on having a clean period-8 generator whose eigenvalues are the 8th roots of unity, including $i$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.