omega8
plain-language theorem explainer
Defines the primitive eighth root of unity ω = exp(2πi/8) = exp(iπ/4) on ℂ. Cycle-operator and DFT-8 work cite it as the eigenvalue generator for the Gray-code period-8 shift on ℂ⁸. The body is a one-line complex exponential; no proof content.
Claim. Let $\omega_8 := e^{2\pi i/8} = e^{i\pi/4}\in\mathbb{C}$. This is a primitive eighth root of unity (so $\omega_8^8=1$ and the order is exactly $8$).
background
The module builds the cycle operator $\hat R$ on $\mathbb{C}^8$: the unitary permutation matrix induced by the 8-tick Gray-code walk on the cube $Q_3$. Vertices of $Q_3$ are the standard basis; one tick flips a single bit along the Gray path, and a full period is eight ticks (the Recognition T7 octave).
Eigenvalues of a period-8 unitary cycle are eighth roots of unity, and the eigenstates are the DFT-8 modes used later for Born-rule and gap-weight forcing. This definition supplies the positive-phase primitive root $\omega=e^{2\pi i/8}$ used to write those modes and eigenvalues.
A sibling definition in Spectral.DFT8 uses the opposite convention $\omega=e^{-2\pi i/8}$. Downstream spectral identities must track which sign is in force; here the CycleOperator convention is the positive exponential.
proof idea
Pure definition: bind omega8 to Complex.exp (2 * Real.pi * Complex.I / 8). No tactics, no lemmas. Adjacent module comments record the intended algebraic facts ($\omega^8=1$, powers give the full group of eighth roots) for later theorems to prove.
why it matters
This is the scalar seed for the whole eight-tick spectral story. Locally it feeds dft8Mode, the normalized DFT-8 basis states that diagonalize the cycle operator with eigenvalues $\omega^k$. Downstream, ComplexStructureForcing equates star-ζ powers to powers of this root and identifies the local DFT with matrix multiplication.
In Constants, GapWeight uses it for discrete difference energy of DFT modes: diffEnergy8_mode shows that energy equals $|\omega^k-1|^2$, which is why a $\sin^2(k\pi/8)$ factor appears (Laplacian spectrum of the 8-tick shift). AlphaGenesis SpectralForcing packages the trig closure $|\omega^k-1|^2=4\sin^2(k\pi/8)$ into the M6 spectral-forcing certificate that constrains $\alpha$.
Framework landmark: T7 eight-tick octave. Without a fixed primitive eighth root, the cycle operator’s spectrum, generation-axis phases, and CKM-oriented mixing angles have no algebraic carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.