cyclicShiftIter
plain-language theorem explainer
Defines the n-fold iterate of the one-tick cyclic shift on eight-component signals: T^0 = id and T^{n+1} = T ∘ T^n. Anyone working the discrete time evolution or DFT eigenstructure of the recognition operator cites it. The body is a plain recursive definition by composition, not a proved statement.
Claim. For each natural number $n$, write $T^n$ for the $n$-fold composition of the one-tick cyclic shift $T$ on eight-tick complex signals $f:\mathbb{Z}/8\mathbb{Z}\to\mathbb{C}$, with $T^0=\mathrm{id}$ and $T^{n+1}=T\circ T^n$. Explicitly, $(T^n f)(k)=f(k+n\bmod 8)$.
background
The ambient object is Signal8: complex-valued functions on the eight-tick cycle $\mathbb{Z}/8\mathbb{Z}$. In Recognition Science this is the discrete carrier of the recognition operator; the module keeps a legacy ledger surface but the canonical dynamics here are analytic on these eight-tick signals.
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 it "the fundamental discrete time-evolution generator" on the eight-tick octave forced at T7.
Iterates $T^n$ are the natural discrete-time powers. They feed linearity lemmas, DFT mode eigenrelations, and the concrete $P^4=-I$ identity on the quarter-turn core used in the paper.
proof idea
No proof: this is a recursive definition. Base case $n=0$ is the identity map on Signal8. Successor case composes one further one-tick cyclic shift onto the already-built $n$-fold iterate. Downstream lemmas prove properties of this object by induction on $n$, unfolding the two clauses.
why it matters
This is the discrete-time power map for the recognition operator's shift generator. Downstream it underwrites: additivity and scalar-homogeneity of iterates; the DFT mode formula $T^n e_k=(\omega_8^k)^n e_k$; and the paper-facing theorems that four shifts (equivalently two beats squared) act as $-I$ on the quarter-turn core, the concrete $P^4=-I$ statement.
Framework-wise it sits on the T7 eight-tick octave: once period $2^3$ is forced, powers of the cyclic shift are the discrete evolution, and the quarter-turn core is where that evolution realizes a complex structure ($T^4=-I$). Without a named iterate, those eigenstructure and $P^4$ arguments cannot even be stated cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.