eigenvalue
plain-language theorem explainer
Defines the eigenvalue of the 8-tick cyclic shift at mode k as the k-th power of the primitive 8th root of unity ζ. Anyone working the complex-structure forcing argument, DFT-8 diagonalization, or Clifford grading correspondence cites this. It is a one-line definitional assignment, not a derived equality.
Claim. For each mode index $k \in \{0,\ldots,7\}$, the eigenvalue of the 8-tick shift operator $T$ at mode $k$ is $\zeta^k$, where $\zeta$ is a primitive 8th root of unity in $\mathbb{C}$.
background
The module Complex Structure Forcing argues that the 8-tick shift $T$ on the ledger state space (with $T^8 = I$, from T7) cannot be diagonalized over $\mathbb{R}$. Its spectrum consists of the 8th roots of unity $\omega^k = e^{2\pi i k/8}$. In particular $\omega^2 = i$ has no real representative, since $x^2 + 1 > 0$ for all real $x$, so complexification is algebraically forced rather than chosen. The DFT-8 is the canonical unitary diagonalization.
Upstream, phaseExp from EightTick supplies the complex exponential of the discrete phase $k\pi/4$, and the sibling equality later identifies this eigenvalue with that phase exponential. The setting depends on T5 (J-cost uniqueness), T7 (eight-tick octave), and T8 ($D=3$).
proof idea
Pure definition: assign to each $k : \mathrm{Fin}, 8$ the complex number $\zeta^{k.\mathrm{val}}$. No tactics, no lemmas. A sibling lemma later proves this equals phaseExp k from EightTick.
why it matters
This is the spectral label that the whole complex-structure story hangs on. Downstream, complexification_forced and ComplexStructureCertificate use it to show $T$ is not real-diagonalizable. GapWeight projections use it for DFT-8 column norms and for the discrete difference energy identity $\mathrm{diffEnergy}_8(\mathrm{mode}_k) = |\omega^k - 1|^2$, which produces the $\sin^2(\pi k/8)$ factor. SymplecticAction links reciprocal eigenvalue pairing to $J(x)=J(1/x)$. CliffordBridge identifies mode $k$ with Clifford grade $k$ in $\mathrm{Cl}_8$, so the same $\zeta^k$ labels both the DFT spectrum and the $\mathbb{Z}/8\mathbb{Z}$ grading. Framework landmarks: T7 eight-tick octave and the forced passage to a complex Hilbert space needed for genuine unitarity of the recognition operator.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.