eigenvalue_2_is_I
plain-language theorem explainer
The mode-2 eigenvalue of the eight-tick cyclic shift is exactly the imaginary unit i. Anyone proving that the ledger shift cannot be diagonalized over the reals cites this identification. The proof unfolds the eigenvalue definition and applies the known identity that the primitive eighth root squared equals i.
Claim. Let $\zeta$ be a primitive eighth root of unity and let the eigenvalue of the eight-tick shift at mode $k\in\{0,\ldots,7\}$ be $\zeta^k$. Then the eigenvalue at $k=2$ equals $i=\sqrt{-1}$.
background
The module Complex Structure Forcing argues that the T7 eight-tick forces a cyclic shift $T$ on the eight-slot ledger state space with $T^8=I$, whose spectrum is the eighth roots of unity. Diagonalization over $\mathbb{R}$ fails once a non-real root appears; complexification is then algebraically required, not optional.
Locally, eigenvalue at mode $k$ is defined as $\zeta^k$. The $k=2$ case is $\zeta^2=e^{i\pi/2}=i$. Upstream, the same eigenvalue abbreviation is re-exported from the operator-core layer so the forcing chain and spectral DFT-8 code share one spectrum.
This sits between T7 (period $2^3$) and the later claim that the DFT-8 is the canonical unitary diagonalization, with J-cost depending only on mode moduli (phase invariance).
proof idea
One-line tactic proof. Unfold the definition of the mode eigenvalue (power of $\zeta$ at the Fin-8 index), then discharge by the already-proved identity $\zeta^2=i$. No further algebraic work is done here; the content is the identification of the $k=2$ spectrum point with $\mathrm{Complex.I}$.
why it matters
This is the concrete witness that the eight-tick shift has a purely imaginary eigenvalue. Downstream, complexification_forced packages exactly that witness with the fact that $x^2+1\neq 0$ for all real $x$, concluding that $T$ cannot be fully diagonalized over $\mathbb{R}$. The same equality is the has_imaginary_eigenvalue field of complex_structure_certificate.
In the Unified Forcing Chain it feeds the T7-to-canonical-shift and carrier bridges: the period-8 cyclic advance is not merely combinatorial; its spectrum already forces $\mathbb{C}$. That closes the registry gap "complex Hilbert space from cost" between T5/T7/T8 and genuine unitarity (Parseval, admissible evolutions as unitary operators). Companion fact: the $k=6$ eigenvalue is $-i$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.