cyclicShiftIter_smul
plain-language theorem explainer
The n-fold cyclic shift on eight-tick complex signals is homogeneous: shifting a scalar multiple equals the scalar times the shifted signal. Anyone proving that DFT modes are eigenvectors of the shift iterates, or that four shifts act as minus identity on the quarter-turn core, cites this. The proof is induction on n with pointwise simplification.
Claim. For every natural number $n$, every complex scalar $a$, and every eight-tick signal $f$, the $n$-fold cyclic shift satisfies $T^n(a\cdot f)=a\cdot T^n(f)$.
background
In the Recognition Operator module the working space is Signal8: complex-valued functions on the eight discrete ticks of the octave (the T7 period $2^3$). The fundamental time-evolution generator is the cyclic shift $T$, defined by $(Tf)(k)=f(k+1\bmod 8)$. The iterated operator $T^n$ is defined recursively: identity at $n=0$, and $T\circ T^n$ at the successor.
Scalar multiplication is the pointwise $\mathbb{C}$-module structure on signals. Homogeneity of each single shift is elementary; the lemma lifts that fact to every iterate so that later spectral arguments can move scalars freely past $T^n$.
The local setting is the analytic eight-tick operator that replaces older ledger-side RecognitionOperator APIs while preserving bridge compatibility.
proof idea
Induction on $n$. Base case $n=0$: both sides are $a\cdot f$ after unfolding the identity iterate and extending pointwise. Successor: unfold one more composition with the single cyclic shift, apply the inductive hypothesis inside, then simplify with the definition of the one-step shift (which itself is linear). The argument is pure pointwise ext plus simp.
why it matters
Homogeneity is the scalar half of $\mathbb{C}$-linearity of $T^n$. The immediate parent is shift_four_eq_neg_on_quarterTurnCore, whose doc-comment states the concrete paper claim $P^4=-I$ on the quarter-turn core: that proof runs by submodule span induction and needs scalars to pass through four-fold shifts when reducing generators. The same fact underwrites the companion statement that every DFT mode is an eigenvector of each shift iterate. Framework-wise this sits inside the eight-tick octave (forcing chain T7) and the complex-structure forcing that produces the quarter-turn generator used for $i$ and the recognition operator spectrum.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.