eigenvalue_6_is_neg_I
plain-language theorem explainer
The mode-6 eigenvalue of the eight-tick cyclic shift equals -i. Anyone citing the forced complex spectrum of the T7 shift needs this identity alongside the mode-2 value +i. The proof unfolds the eigenvalue definition and applies the known power ζ^6 = -i.
Claim. Let $\zeta$ be a primitive eighth root of unity and write $\lambda_k = \zeta^k$ for the eigenvalue of the eight-tick cyclic shift at mode $k\in\{0,\ldots,7\}$. Then $\lambda_6 = -i$.
background
The module Complex Structure Forcing argues that the eight-tick shift forced by T7 cannot be diagonalized over the reals, so complexification is algebraic rather than optional. The shift $T$ on the eight-slot ledger satisfies $T^8 = I$, so its spectrum is the eighth roots of unity $\omega^k = e^{2\pi i k/8}$.
Locally, eigenvalue at mode $k$ is defined as $\zeta^k$. Modes $k=2$ and $k=6$ give $\zeta^2 = i$ and $\zeta^6 = -i$. Both are non-real; the companion fact that $x^2+1>0$ for all real $x$ is the obstruction that blocks a real eigenbasis.
Upstream, the eigenvalue definition and the phase-exponential form of $\zeta^k$ from the EightTick/DFT-8 layer supply the concrete complex values used here.
proof idea
Term-mode one-liner. Unfold the definition of the mode eigenvalue (which is $\zeta$ raised to the mode index), then discharge the resulting goal by the already-proved identity $\zeta^6 = -i$. No further case analysis or arithmetic is performed in this declaration.
why it matters
This identity is one of the two non-real spectral points (with mode 2 equal to $+i$) that force the eight-tick shift off the real line. It feeds the T7-to-canonical-shift and T7-to-canonical-carrier bridge certificates in UnifiedForcingChain, which package the period-8 law, the full eigenvalue spectrum, and the universal property of the cyclic advance. It also sits under the Hamiltonian-emergence story in the same module: once the complex eigenbasis is forced, the small-deviation expansion of the J-cost can be read as a quadratic kinetic term on that Hilbert space.
In the forcing chain this closes part of the gap between T7 (eight-tick octave) and the complex Hilbert structure needed for genuine unitarity, as flagged in the module registry (depends on T5 cost uniqueness, T7, and T8 with $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.