shift_eigenvalue
plain-language theorem explainer
Defines the eigenvalue of the length-8 cyclic shift on DFT mode k as ω^k, where ω is the primitive eighth root of unity. Anyone citing the DFT-8 diagonalization of time translation on the eight-tick cycle needs this label. It is a one-line abbreviation of the power ω^{k}.
Claim. For each mode index $k \in \{0,\ldots,7\}$, the eigenvalue of the cyclic shift on that mode is $\omega^k$, where $\omega = e^{-2\pi i/8}$ is the primitive eighth root of unity used by the DFT-8 basis.
background
The DFT-8 module builds the canonical unitary basis for the eight-tick recognition cycle forced by T7 (period $2^3$) and T8 ($D=3$). The primitive root is $\omega = e^{-\pi i/4}$, so $\omega^8=1$. DFT matrix entries are $\omega^{tk}/\sqrt{8}$; columns are the modes.
The cyclic shift $S$ advances the tick index by one (mod 8). On a pure mode $k$, time translation multiplies by a pure phase. That phase is exactly the $k$-th power of $\omega$. The local definition packages this phase so the diagonalization theorem can name the spectrum without repeating the power expression.
Upstream, both the foundation CycleOperator and this module expose $\omega_8$; the spectral copy uses the negative-frequency convention matching the DFT sign.
proof idea
Pure definitional abbreviation: the value on mode $k$ is written as $\omega_8$ raised to the natural number underlying $k$. No proof obligations; noncomputable only because complex exponentiation is.
why it matters
Feeds the main spectral theorem dft8_diagonalizes_shift, which states $B^H S B = \mathrm{diag}(1,\omega,\omega^2,\ldots,\omega^7)$. That identity is the precise sense in which DFT-8 is the eigenbasis of time-translation symmetry on the eight-tick octave.
In the Recognition framework this closes the spectral half of the T7 story: the forced period-8 cycle admits a unique (up to phase/permutation) unitary basis that diagonalizes the shift, separates the DC mode from the seven neutral modes, and supplies the complex-exponential ladder used for $\varphi$-lattice quantization. Without a named eigenvalue map, the diagonal form cannot be stated cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.