star_omega8_mul_self
plain-language theorem explainer
The conjugate of the primitive eighth root of unity multiplies back to 1, i.e. |ω|² = 1 on the unit circle. Anyone clearing conjugate factors in the DFT-8 basis or proving mode normalizations cites this. Proof rewrites the conjugate as the inverse, then cancels by nonvanishing of the complex exponential.
Claim. Let $\omega = e^{-i\pi/4}$ be the primitive eighth root of unity used by the eight-point DFT. Then $\overline{\omega}\,\omega = 1$, equivalently $|\omega|^2 = 1$.
background
The DFT-8 module supplies the canonical unitary basis for the eight-tick recognition cycle. That period $\tau_0 = 2^D$ with $D = 3$ is forced by the Recognition axioms (T7/T8). The spectral generator is the primitive root $\omega = \exp(-i\pi/4)$, so $\omega^8 = 1$, and DFT entries are the normalized powers $\omega^{tk}/\sqrt{8}$.
Complex conjugation on $\mathbb{C}$ is the involution written as star. An upstream lemma already records that $\overline{\omega} = \omega^{-1}$: conjugating the exponential flips the sign of the phase and recovers the multiplicative inverse on the circle. The present statement is the immediate unit-modulus consequence $\overline{\omega},\omega = 1$.
This is the elementary algebraic step before power identities and before the full DFT unitarity argument that diagonalizes the cyclic shift.
proof idea
Rewrite $\overline{\omega}$ as $\omega^{-1}$ via the conjugate-inverse lemma. The goal collapses to $\omega^{-1}\omega = 1$, which is left-inverse cancellation once $\omega\neq 0$. Nonvanishing is immediate: $\omega$ is a complex exponential, and $\exp(z)\neq 0$ for every $z\in\mathbb{C}$.
why it matters
Direct parent is the power form $(\overline{\omega})^n\omega^n = 1$, obtained by raising this identity and using $(ab)^n = a^n b^n$. That power form clears conjugate factors when normalizing DFT modes and when proving $B^H B = I$ for the eight-point transform.
In the Recognition framework this sits inside the eight-tick spectral backbone: DFT-8 is the unique (up to permutation/phase) unitary basis that diagonalizes the cyclic shift on the forced period $2^3$, separates the DC mode from the neutral subspace $k=1..7$, and supplies $\varphi$-lattice phases via complex exponentials. Without $|\omega|=1$ the normalized entries would not yield a unitary change of basis.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.