shift
plain-language theorem explainer
Defines the cyclic shift operator T on 8-tick complex signals: (Tf)(k) = f(k+1 mod 8). Anyone working the complex-structure forcing argument, DFT-8 diagonalization, or eight-tick time evolution cites this as the discrete generator. The body is a one-line pullback along the modular index advance.
Claim. For a signal $f:\mathbb{Z}/8\mathbb{Z}\to\mathbb{C}$, the cyclic shift is $(Tf)(k)=f(k+1\bmod 8)$. Equivalently, $T$ advances the reading index by one tick on the eight-tick cycle.
background
The module Complex Structure Forcing argues that the eight-tick shift cannot be diagonalized over $\mathbb{R}$, so complexification is algebraically forced. Landmark T7 supplies the period-$2^3$ octave; the ledger state on that cycle is a signal $f:\mathrm{Fin},8\to\mathbb{C}$ (abbreviated Signal8).
The companion index map advances $k$ by one tick: $\mathrm{nextIdx}(k)=\langle(k+1)\bmod 8\rangle$. The shift operator is the fundamental discrete time-evolution generator: it pulls $f$ back along that advance, so $T^8=I$ will be the algebraic content of the period-8 theorem proved later in the same file.
Upstream, the same modular advance is re-exported in OperatorCore; a related occupation shift on $\mathrm{ZMod},8$ appears in EightTickWeyl (with opposite orientation $k\mapsto k-1$). The present definition is the canonical $T$ used for eigenvalue and DFT-8 work.
proof idea
Pure definition, not a proof. The body is the function $k\mapsto f(\mathrm{nextIdx},k)$, i.e. composition with the already-defined modular successor on $\mathrm{Fin},8$. No lemmas are applied; well-typedness follows from $\mathrm{nextIdx}:\mathrm{Fin},8\to\mathrm{Fin},8$ and Signal8 $=\mathrm{Fin},8\to\mathbb{C}$.
why it matters
This $T$ is the object whose spectrum forces $\mathbb{C}$. Module thesis: eigenvalues are 8th roots of unity; $\omega^2=i$ has no real representative ($x^2+1>0$ on $\mathbb{R}$), so $T$ is not diagonalizable over $\mathbb{R}$. Downstream siblings (shiftIter, shift_period_8, dftBasis, eigenvalue_2_is_I) build the DFT-8 unitary diagonalization and the $i$-eigenmode on that fact.
Used widely: Action.Noether time-shift language, CostAlgebra reciprocal identities, GapWeight DFT-8 norm sums, and the pulsar-period track (recycling_rung_shift = 8, bimodal $\varphi^8$ ratio) all depend on the same eight-tick generator. Closes the registry gap "complex Hilbert space from cost" together with T5 (J-uniqueness), T7 (eight-tick), and T8 ($D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.