cyclicShiftIter
plain-language theorem explainer
Defines the n-fold iterate of the one-tick cyclic shift on eight-component complex signals: zero iterates is the identity, and each successor composes one more shift. Anyone working the discrete time generator, DFT mode eigenvalues, or the quarter-turn core identity P^4 = -I cites this. The body is a plain recursive definition by composition, not a proved statement.
Claim. For each natural number $n$, the map $T^n : \mathrm{Signal}_8 \to \mathrm{Signal}_8$ is defined by $T^0 = \mathrm{id}$ and $T^{n+1} = T \circ T^n$, where $T$ is the one-tick cyclic shift $(Tf)(k) = f(k+1 \bmod 8)$ on complex-valued functions of the eight-tick cycle.
background
The ambient object is Signal8: complex-valued functions on the discrete eight-tick cycle, the analytic carrier of the recognition operator in this module. The one-tick generator $T$ (written shift / cyclic_shift upstream) advances the reading index by one: $(Tf)(k) = f(k+1 \bmod 8)$. Upstream docs call this "the fundamental discrete time-evolution generator."
That eight-tick period is the T7 landmark of the forcing chain (period $2^3$). The present definition packages the free monoid action of $\mathbb{N}$ on signals by iterated composition of $T$, so later lemmas can talk about $T^n$ without unrolling compositions by hand.
The module also keeps a legacy ledger surface; the canonical operator here is this analytic 8-tick operator on Signal8, not the older ledger-field API.
proof idea
No proof: this is a recursive definition. Base case $n=0$ returns the identity map on Signal8. Successor case composes the one-tick cyclic shift with the already-defined $n$-fold iterate. Downstream lemmas prove properties of this object by induction on $n$, typically simplifying the zero case with simp [cyclicShiftIter] and using the inductive hypothesis plus the corresponding one-step fact for cyclic_shift.
why it matters
This is the discrete-time power that the recognition operator calculus needs. Immediate consumers are linearity facts (cyclicShiftIter_add, cyclicShiftIter_smul) and the spectral fact that every DFT mode is an eigenvector of each iterate (cyclicShiftIter_mode).
Those feed the paper-facing identities on the quarter-turn core: shift_four_eq_neg_on_quarterTurnCore states the concrete $P^4 = -I$ claim ("Four shifts act as $-I$ on the quarter-turn core"), and twoBeat_square_eq_neg_on_quarterTurnCore rewrites two beats squared as the same $-I$. Both reduce via the mode eigenvalue formula for $T^n$.
In framework terms this is the free $\mathbb{N}$-action generated by the T7 eight-tick shift, the discrete skeleton behind complex structure and the quarter-turn / two-beat algebra on the structured sector.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.