star_omega8
plain-language theorem explainer
Complex conjugation of the primitive eighth root of unity equals its multiplicative inverse: conj(ω)=ω^{-1}. Spectral and gap-weight arguments that need |ω|=1 or star(ω^n)=ω^{-n} cite this. The proof unfolds ω=exp(-iπ/4), applies conj∘exp=exp∘conj, and reduces to exp(-z)=exp(z)^{-1} by a short ring identity.
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}$ in $\mathbb{C}$.
background
The DFT-8 module builds the canonical unitary basis for the eight-tick recognition cycle. The period $\tau_0=2^D$ with $D=3$ is forced by the Recognition Science chain (T7/T8), so the spectral backbone is the 8-point discrete Fourier transform on $\mathbb{C}^8$.
The generator is the primitive root $\omega=e^{-i\pi/4}=e^{-2\pi i/8}$. Matrix entries are $\omega^{tk}/\sqrt{8}$; columns are the DFT modes. Unitarity of that matrix, diagonalization of the cyclic shift, and separation of the DC mode from the neutral subspace all rest on algebraic identities for $\omega$.
Complex star on $\mathbb{C}$ is conjugation. For any pure phase $e^{i\theta}$ one expects $\overline{e^{i\theta}}=e^{-i\theta}=(e^{i\theta})^{-1}$. This lemma records that fact for the concrete eighth root used throughout the module.
proof idea
Unfold the local definition $\omega=\exp(-I\pi/4)$ and the definition of complex star. Rewrite conjugation through the exponential via $\mathrm{conj}(\exp z)=\exp(\mathrm{conj},z)$, then simplify the conjugated argument with the usual maps on division, negation, multiplication, and $\overline{I}=-I$. The goal becomes $\exp(I\pi/4)=\exp(-I\pi/4)^{-1}$. Apply $\exp(z)^{-1}=\exp(-z)$ and finish by a one-line ring congruence on the exponents.
why it matters
This is the base conjugation identity for the DFT-8 root. Downstream it discharges $\mathrm{star}(\omega)\cdot\omega=1$ (unit modulus) and $\mathrm{star}(\omega^n)=\omega^{-n}$, which are the bookkeeping steps needed whenever Hermitian adjoints of DFT modes or powers of $\omega$ appear.
It is also used in the positivity proof for the DFT-based eight-tick gap-weight candidate, tying the spectral backbone to the constants layer. In the broader framework it supports the eight-tick octave (T7): the DFT-8 basis is the unique (up to phase/permutation) unitary frame that diagonalizes time-translation on the forced period-$8$ register and separates mean from neutral modes. Without conj(ω)=ω^{-1}, unitarity and mode-norm arguments do not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.