star_omega8_pow
plain-language theorem explainer
Complex conjugation sends every natural power of the primitive eighth root of unity to the same power of its inverse: conjugate(ω^n)=(ω^{-1})^n. Cited by anyone computing DFT-8 adjoints, mode inner products, or shift eigenvalues on the eight-tick cycle. Proof is a two-step rewrite: the star-power homomorphism, then the base identity conjugate(ω)=ω^{-1}.
Claim. Let $\omega=e^{-i\pi/4}$ be the primitive eighth root of unity in $\mathbb{C}$. For every $n\in\mathbb{N}$, $\overline{\omega^n}=(\omega^{-1})^n$.
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$ (forcing chain T7–T8), so the spectral backbone is the 8-point DFT. Its generator is the primitive root $\omega=e^{-i\pi/4}$, and matrix entries are $\omega^{tk}/\sqrt{8}$.
On $\mathbb{C}$, Lean star is complex conjugation. The base fact already on record is $\overline{\omega}=\omega^{-1}$, proved by conjugating the exponential: $\overline{\exp(-i\pi/4)}=\exp(i\pi/4)=\omega^{-1}$. DFT entries are powers of $\omega$, so conjugation must lift from the generator to $\omega^n$ before one can form adjoints or mode inner products.
The local setting is exactly that bookkeeping: identities needed to show the DFT-8 matrix is unitary and diagonalizes the cyclic shift.
proof idea
Short term-mode proof by two rewrites. Apply the general monoid homomorphism law $\overline{z^n}=\overline{z}^n$ (star_pow), then substitute the base lemma $\overline{\omega}=\omega^{-1}$. The goal is then definitionally the right-hand side $(\omega^{-1})^n$. No case split, induction, or analytic estimate is required.
why it matters
Parent lemmas that consume this identity are the product rules star(ω^n)·ω^m = ω^{7n+m} and the diagonal cancellation star(ω^{tk})·ω^{tk}=1. Those are the algebraic steps that turn conjugate-transpose products of DFT entries into Kronecker deltas, feeding dft8_unitary and the orthonormality of the eight modes.
In the framework this is infrastructure for the eight-tick spectral backbone: the unique (up to phase/permutation) unitary basis that diagonalizes time-translation on the forced period-8 cycle, separates the DC mode from the neutral subspace, and supplies the complex-exponential φ-lattice quantization. Without the power-lift of conjugation, the adjoint computation does not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.