cyclicShiftIter_mode
plain-language theorem explainer
Each DFT-8 mode is an eigenvector of every iterate of the cyclic shift, with eigenvalue ω^{k n} where ω is the primitive eighth root of unity. Anyone tracking the eight-tick shift action on frequency modes cites this. The proof is induction on the iterate count, reducing the successor step to the single-shift eigenvector identity.
Claim. For every $n \in \mathbb{N}$ and every mode index $k \in \{0,\ldots,7\}$, the $n$-fold cyclic shift of the $k$-th DFT-8 mode equals $(\omega_8^{k})^{n}$ times that mode, where $\omega_8 = e^{2\pi i/8}$.
background
In the Recognition Operator module, an eight-component complex signal (Signal8) is the discrete ledger state on the eight-tick octave forced by T7. The cyclic shift rotates the eight slots by one tick; its iterates are defined by cyclicShiftIter, with the zero iterate the identity and the successor the composition with one more shift.
The DFT-8 modes are the standard Fourier basis vectors on $\mathbb{C}^8$. The scalar $\omega_8 = e^{2\pi i/8}$ is the primitive eighth root of unity from CycleOperator. A single shift already multiplies the $k$-th mode by $\omega_8^k$ (the one-step eigenvector law used below). The present statement lifts that law from one shift to an arbitrary number of shifts.
Local setting: the operator algebra of the recognition ledger on the forced period-$8$ clock, prior to extracting the quarter-turn core and the $P^4 = -I$ identity.
proof idea
Induction on the iterate count $n$.
Base case $n=0$: both sides are the mode itself (zero iterates is id; any scalar to the power $0$ is $1$), checked by extensionality and simp.
Successor: unwind the recursive definition so that $n+1$ iterates equal one cyclic shift of the $n$-fold iterate. Rewrite the inner iterate by the inductive hypothesis, then pull the scalar $(\omega_8^k)^n$ out of the shift (shift is linear). Apply the one-step eigenvector identity dft8_shift_eigenvector to replace the remaining shift of the mode by $\omega_8^k$ times the mode. Reassociate powers via pow_succ and mul_assoc to obtain $(\omega_8^k)^{n+1}$ times the mode.
why it matters
Feeds directly into shift_four_eq_neg_on_quarterTurnCore, whose doc-comment states: "Four shifts act as $-I$ on the quarter-turn core. This is the concrete $P^4 = -I$ statement used in the paper." That parent theorem specializes the present eigenvector law at $n=4$ on odd modes, where $(\omega_8^k)^4 = -1$.
In the forcing chain this sits under T7 (eight-tick octave, period $2^3$): the cyclic shift is the discrete time generator on that octave, and the DFT modes diagonalize it. Establishing that every iterate remains diagonal in the same basis is the algebraic step that turns the single-tick phase into the quarter-turn and half-period sign flips used later in the recognition operator and complex-structure forcing.
No open scaffold: the lemma is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.