cyclicShiftIter_add
plain-language theorem explainer
Iterated cyclic shift on eight-tick complex signals is additive: shifting f+g by n ticks equals the sum of the shifted signals. Anyone proving linearity of the discrete time-evolution operator on Signal8 cites this. The proof is induction on n, reducing each step to the one-tick shift via extensionality.
Claim. For every natural number $n$ and every pair of eight-tick signals $f,g:\mathbb{Z}/8\mathbb{Z}\to\mathbb{C}$, the $n$-fold cyclic shift satisfies $T^n(f+g)=T^n f+T^n g$, where $T$ advances the reading index by one tick modulo 8.
background
In the RecognitionOperator foundation layer, the canonical state space is Signal8: complex-valued functions on the eight-tick circle (the discrete octave forced by T7). The one-tick generator $T$ is the cyclic shift $(Tf)(k)=f(k+1\bmod 8)$, the fundamental discrete time-evolution operator from ComplexStructureForcing.
The iterated operator $T^n$ is defined recursively: $T^0=\mathrm{id}$ and $T^{n+1}=T\circ T^n$. Pointwise addition of signals makes Signal8 a complex vector space, so additivity of $T^n$ is the first half of $\mathbb{C}$-linearity needed for spectral and core-subspace arguments.
The module keeps a legacy ledger compatibility surface, but this lemma lives entirely on the analytic eight-tick operator, not on ledger fields such as time or Z-patterns.
proof idea
Induction on $n$.
Base case $n=0$: $T^0$ is the identity, so both sides are $f+g$; finish by pointwise extensionality and unfolding the iterator.
Successor: assume $T^n(f+g)=T^n f+T^n g$. Apply one more cyclic shift and use that the one-tick shift itself is additive (unfolded via cyclic_shift / shift). Extensionality on the tick index plus simplification closes the step.
why it matters
Additivity is the first structural fact needed before treating $T$ as a linear operator on the eight-tick space. The sole recorded consumer is shift_four_eq_neg_on_quarterTurnCore, which proves $T^4=-I$ on the quarter-turn core (the concrete $P^4=-I$ statement used in the paper) by submodule span induction; that argument needs $T^4$ to respect linear combinations of odd Fourier modes.
In the broader forcing chain this sits under the eight-tick octave (T7) and the complex-structure forcing that isolates the quarter-turn generator. Without additivity, eigenvalue and core-subspace identities for the recognition operator cannot even be stated as linear maps.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.