eigenvalue
plain-language theorem explainer
The cyclic shift on the eight-tick signal has eigenvalues that are successive powers of a primitive eighth root of unity. Anyone computing DFT-8 mode costs, discrete difference energy, or the DFT–Clifford grade map cites this symbol. The declaration is a module-local abbreviation of the foundation definition, with no extra proof content.
Claim. For each mode index $k \in \{0,\ldots,7\}$, the eigenvalue of the eight-tick cyclic shift on DFT mode $k$ is $\zeta^k$, where $\zeta$ is a fixed primitive eighth root of unity in $\mathbb{C}$.
background
In the eight-tick setting the discrete time circle is $\mathrm{Fin},8$. The cyclic shift $T$ advances the tick index by one. Its Fourier modes are the DFT-8 columns; on mode $k$ one has $T v^{(k)} = \zeta^k v^{(k)}$, so the spectrum is exactly the eighth roots of unity.
The parent module forces a complex structure from the recognition cost and the eight-tick period (T7 in the forcing chain). The local OperatorCore layer re-exports the same eigenvalue map so that cost, gap-weight, and Clifford bridge developments can name it without a long qualified path.
Upstream, the foundation definition is simply $\mathrm{eigenvalue}(k) := \zeta^{k.\mathrm{val}}$, with the phase expressed via the eight-tick exponential.
proof idea
One-line abbreviation: the symbol is definitionally equal to IndisputableMonolith.Foundation.ComplexStructureForcing.eigenvalue. No tactics, no lemmas, no new equalities are introduced here.
why it matters
This name is the shared spectral handle for the eight-tick octave. Downstream, discrete difference energy of a DFT mode reduces to $|\omega^k-1|^2$, which is why a $\sin^2(\pi k/8)$ factor appears in gap-weight projections. The DFT–Clifford bridge identifies eigenvalue $\omega^k$ with Clifford grade $k$ in $\mathrm{Cl}_8$, and grading addition is compatible with mode addition mod 8.
On the cost side, reciprocal eigenvalue pairing for area-preserving events forces $\mu=\lambda^{-1}$, which is the spectral reason the recognition cost satisfies $J(x)=J(1/x)$; the calibrated trace cost on the split torus then equals $J$. The abbreviation therefore sits under T7 (eight-tick period) and feeds both the complex-structure certificate and the symplectic-action identification of cost with $J$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.