nextIdx
plain-language theorem explainer
Re-export of the mod-8 index advance: on a tick label k in {0,...,7}, send k to k+1 mod 8. Anyone building the eight-tick cyclic shift, its iterates, or the T7 bridge to the canonical shift cites this. The body is a one-line Fin constructor with a trivial modulus bound.
Claim. For each tick index $k \in \{0,1,\ldots,7\}$, the next index is $k+1 \bmod 8$, returned as an element of the same eight-point set.
background
In the complex-structure forcing layer, discrete time is an eight-tick octave: signals are maps from Fin 8 (the eight tick labels) into a value type. The fundamental clock step is advance-by-one on those labels, taken modulo 8 so the octave closes.
Upstream, the same function is defined as the Fin-valued map $k \mapsto \langle (k+1)\bmod 8\rangle$ with the standard modulus bound. The module doc for the cyclic shift states that $T$ advances the reading index by one tick, $(Tf)(k)=f(k+1\bmod 8)$, and calls this the fundamental discrete time-evolution generator. That generator is built by composing a signal with this index map.
Locally this file only re-exports the name into the OperatorCore namespace so downstream OperatorCore and UnifiedForcingChain material can cite a single short identifier.
proof idea
No proof: this is an abbrev alias of the upstream definition. That definition constructs a Fin 8 whose value is (k.val + 1) % 8 and discharges the bound with Nat.mod_lt plus norm_num. Nothing further is proved at this declaration.
why it matters
This is the atomic clock step behind the eight-tick story (forcing-chain landmark T7). Downstream, shift is defined by $(Tf)(k)=f(\mathrm{nextIdx},k)$, shiftIter iterates that operator, and nextIdx_8 proves eight applications return the start, feeding the theorem $T^8=\mathrm{id}$.
The UnifiedForcingChain bridge T7_To_CanonicalShift_Bridge packages the same advance-by-one law as the defining equation of the canonical cyclic shift, together with period-8, mode eigenvalues, and a universal property. Without a named mod-8 successor, that bridge has no carrier for "one tick." In RS terms this is the discrete generator whose period forces the octave structure used throughout the recognition ledger.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.