dft8_shift_eigenvector
plain-language theorem explainer
Each DFT-8 mode is an eigenvector of the cyclic one-tick shift, with eigenvalue the corresponding power of the primitive eighth root of unity. Anyone deriving discrete time evolution, gap weights, or Schrödinger-type mode dynamics on the eight-tick cycle cites this identity. The proof is a short pointwise calculation: expand both sides, use the modular exponent rule, and factor via the power-addition law.
Claim. For every mode index $k \in \{0,\ldots,7\}$, the cyclic shift of the $k$-th DFT-8 basis vector equals $\omega^k$ times that vector, where $\omega = e^{2\pi i/8}$ is the primitive eighth root of unity. Equivalently, if $v^{(k)}_t = \omega^{tk}/\sqrt{8}$, then $v^{(k)}_{t+1 \bmod 8} = \omega^k\, v^{(k)}_t$ for all ticks $t$.
background
The DFT-8 module builds the canonical unitary basis for the eight-tick recognition cycle forced by $D=3$ (period $2^3=8$). The primitive root $\omega_8 = e^{2\pi i/8}$ generates the matrix entries $B_{t,k} = \omega^{tk}/\sqrt{8}$. Mode $k$ is the $k$-th column of that matrix, viewed as an 8-vector on the discrete circle.
Cyclic shift is the fundamental discrete time-evolution generator: it advances the reading index by one tick, $(Tf)(t) = f(t+1 \bmod 8)$. In the broader foundation this is the same shift that appears as the one-tick recognition operator on Signal8. The module's physical claim is that DFT-8 is (up to permutation and phase) the unique unitary basis that diagonalizes this shift, separates the DC mode from the mean-free neutral subspace, and supplies $\varphi$-lattice phases via complex exponentials.
Upstream, $\omega_8^8=1$ and the modular arithmetic of exponents on $\mathrm{Fin},8$ are already available; the present statement is the eigenvector form of that diagonalization.
proof idea
Pointwise equality of functions on $\mathrm{Fin},8$. After funext and unfolding cyclic shift, mode, and entry, both sides are pure powers of $\omega$ times the common $1/\sqrt{8}$ factor. The left-hand exponent is $((t+1)\bmod 8),k$; mod8_mul_eq converts that to ordinary integer multiplication modulo the order of $\omega$. The elementary identity $(t+1)k = tk + k$ plus pow_add factors out $\omega^k$, and a final ring matches the scalar multiple on the right-hand side.
why it matters
This is the spectral identity that makes DFT-8 the backbone of eight-tick dynamics: cyclic shift acts as $\bigoplus_k \omega^k, I$ on the mode decomposition. Downstream, eigenmode_evolution_exact is literally this theorem under the Schrödinger-derivation name; cyclicShiftIter_mode lifts it to every iterate of the shift; shift_mul_dft8_entry rewrites the same fact in matrix form $(SB){t,j}=\omega^j B{t,j}$.
Gap-weight work uses it to evaluate discrete difference energy: diffEnergy8_mode obtains $|\omega^k-1|^2$ (hence the $\sin^2(\pi k/8)$ Laplacian spectrum) directly from the eigenvalue. Quarter-turn core invariance under one-tick propagation also routes through mode-wise eigenvectors. In the forcing chain this sits under T7 (eight-tick octave) and T8 ($D=3$): once the period is eight, diagonalizing the cycle is the canonical spectral step for recognition evolution.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.