omega8_pow_4
plain-language theorem explainer
The primitive eighth root of unity satisfies ω⁴ = −1, i.e. a half-period on the eight-tick circle. Spectral and recognition-operator arguments cite this when four cyclic shifts must act as sign flip. The proof unfolds the exponential definition, multiplies the angle by four, and reduces to e^{−iπ} = −1 via standard complex identities.
Claim. Let $\omega = e^{-i\pi/4}$ be the primitive eighth root of unity used by the DFT-8 backbone. Then $\omega^4 = -1$.
background
The DFT-8 module supplies the canonical unitary basis for the eight-tick recognition cycle forced by T7 (period $2^3$) and T8 ($D=3$). Its primitive root is defined as $\omega = e^{-i\pi/4}$, so that $\omega^8 = 1$ and powers of $\omega$ are the eigenvalues of the cyclic shift on eight-vectors.
Half-period evaluation is the natural intermediate between full periodicity and the finer mode-by-mode spectrum. In complex analysis this is immediate from $4\cdot(-\pi/4) = -\pi$, hence $e^{-i\pi} = -1$. The same identity appears upstream under a conjugate phase convention ($e^{i\pi/4}$) in the cycle-operator layer; the spectral module uses the negative-frequency convention standard for DFT.
Locally this sits among sibling facts $\omega^8=1$, $|\omega|=1$, and the non-degeneracy statements that keep the DFT modes distinct.
proof idea
Unfold $\omega$ to $\exp(-i\pi/4)$. Rewrite the fourth power via $\exp(z)^n = \exp(nz)$. The angle identity $4\cdot(-i\pi/4) = -i\pi$ is a short push_cast/ring calculation. Then apply $\exp(-z) = (\exp z)^{-1}$, the standard value $\exp(i\pi) = -1$, and $1/(-1) = -1$ to finish.
why it matters
Feeds odd_mode_fourth_eigenvalue in the recognition-operator layer: on odd DFT modes $k$, four shifts act by $(\omega^k)^4 = -1$. That lemma is the spectral reason the odd-mode span is invariant under one-tick propagation with a clean sign structure.
In the RS forcing chain the eight-tick octave (T7) is the discrete time lattice; DFT-8 is its unique (up to phase/permutation) unitary eigenbasis for cyclic shift. Half-period $\omega^4=-1$ is the algebraic hinge between full period-8 closure and the even/odd mode dichotomy used when separating DC from neutral modes and when tracking φ-lattice phases on the cycle.
No scaffolding remains: the claim is fully proved from Mathlib complex exponential facts.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.