eigenvalue_eq_phaseExp
plain-language theorem explainer
The k-th spectral value of the eight-tick cyclic shift equals the complex exponential of the eight-tick phase kπ/4. Anyone matching the DFT-8 spectrum to the EightTick phase ladder cites this bridge. The proof is a short algebraic reduction: unfold both sides, apply the natural-multiple exponential identity, and finish the exponent equality by ring.
Claim. For every mode index $k \in \{0,\ldots,7\}$, the eigenvalue $\zeta^k$ of the eight-tick cyclic shift equals $\exp(i\, k\pi/4)$, where $\zeta=e^{2\pi i/8}$ is the primitive eighth root of unity and the phase ladder is $\mathrm{phase}(k)=k\pi/4$.
background
The module Complex Structure Forcing argues that the eight-tick shift operator $T$ (forced by T7) satisfies $T^8=I$, so its eigenvalues are the eighth roots of unity $\omega^k=e^{2\pi i k/8}$. The mode $\omega^2=i$ has no real representative, since $x^2+1>0$ for all real $x$; thus $T$ cannot be diagonalized over $\mathbb{R}$ and complexification is algebraically forced. The DFT-8 is the canonical unitary diagonalization.
Locally, the eigenvalue at mode $k$ is defined as $\zeta^k$. Independently, EightTick supplies the phase ladder $\mathrm{phase}(k)=k\pi/4$ and its complex exponential $\mathrm{phaseExp}(k)=\exp(i\cdot\mathrm{phase}(k))$. The present result equates these two presentations of the same spectral data.
Upstream, EightTick already records that each phase exponential has eighth power equal to $1$ by $2\pi$-periodicity of the complex exponential. That fact is the geometric counterpart of $T^8=I$.
proof idea
Unfold the definitions of the eigenvalue ($\zeta^{k}$), of $\zeta$ itself, of the phase exponential, and of the real phase $k\pi/4$. Rewrite the power via Complex.exp_nat_mul so both sides are complex exponentials of linear forms in $k$. Congruence reduces the goal to equality of the exponents; push_cast and ring discharge the arithmetic identity $k\cdot(2\pi i/8)=i\cdot(k\pi/4)$.
why it matters
This is the dictionary between the operator-theoretic spectrum of the eight-tick shift and the geometric phase ladder of EightTick. Sibling results in the same module (the second power of $\zeta$ equals $i$; the $k=2$ eigenvalue is exactly $\sqrt{-1}$) rest on the same identification and supply the algebraic step that forces complex structure: no real root of $x^2+1=0$, so $T$ is not diagonalizable over $\mathbb{R}$.
In the forcing chain the result sits under T7 (eight-tick octave, period $2^3$) and supports the module registry goal of closing the gap from cost axioms to the complex Hilbert-space structure needed for genuine unitarity. Once the spectrum is identified, Parseval and the phase-invariance of $J$-cost (modulus only) become available; those later links connect T5 cost uniqueness to unitary recognition operators. No downstream consumers are recorded yet; the immediate consumers are the local $i$-forcing lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.