omega8
plain-language theorem explainer
Primitive eighth root of unity ω = exp(−iπ/4), the generator of the DFT-8 spectral basis for the eight-tick recognition cycle. Cited wherever shift eigenvalues, mode weights, or spectral forcing of α appear. One-line complex-exponential definition (negative-frequency convention).
Claim. Define $\omega := e^{-i\pi/4}\in\mathbb{C}$. Equivalently $\omega=e^{-2\pi i/8}$, a primitive eighth root of unity (clockwise orientation on the unit circle).
background
The DFT-8 module supplies the canonical unitary basis for the eight-tick recognition cycle. Recognition Science forces period $\tau_0=2^D$ with $D=3$ (T7 octave, T8 spatial dimension), so the natural spectral language is the 8-point DFT.
Powers of a primitive eighth root fill the DFT matrix entries $\omega^{tk}/\sqrt{8}$ and serve as eigenvalues of the cyclic shift. The foundation cycle operator defines a twin constant with opposite phase $\exp(+i\pi/4)$; this spectral module uses the conjugate $\exp(-i\pi/4)$, matching the usual signal-processing DFT sign convention.
Sibling facts in the same file record $\omega^8=1$, $|\omega|=1$, and $\omega^4=-1$, which unlock the mode algebra used downstream.
proof idea
Pure definition: $\omega$ is Complex.exp of $-I\cdot\pi/4$. No tactic proof; noncomputability comes only from the real exponential. Algebraic identities ($\omega^8=1$, nonzero powers, absolute value one) live in sibling lemmas, not here.
why it matters
Seed constant for the entire DFT-8 backbone and about forty downstream uses. Parent results include the trig closure $|\omega^k-1|^2=4\sin^2(k\pi/8)$ that closes SpectralForcingCert (M6), the identity that discrete difference energy of mode $k$ equals that same squared modulus (source of the $\sin^2(\pi k/8)$ gap-weight factor), positivity of the DFT candidate weight, and the identification of the complex-structure root $\zeta$ with this $\omega$.
Together these pin the eight-tick spectral ladder: DC mode separated from neutral modes $k=1..7$, shift diagonalized, and $\varphi$-lattice quantization carried by complex exponentials on the forced octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.