star_omega8_pow_mul_same
plain-language theorem explainer
On the unit circle, conjugating an eighth root of unity power cancels it: star(ω^{tk})·ω^{tk}=1 for all tick and mode indices in Fin 8. Spectral and DFT-8 proofs cite this when the diagonal (k=k') inner-product terms collapse to 1. The argument rewrites conjugation via star_omega8_pow, folds into a single power, and cancels by invertibility of ω.
Claim. For all tick and mode indices $t,k\in\{0,\ldots,7\}$, if $\omega=e^{-i\pi/4}$ is the primitive eighth root of unity, then $\overline{\omega^{t k}}\,\omega^{t k}=1$.
background
The DFT-8 module builds the canonical unitary basis for the eight-tick recognition cycle forced by T7 (period $2^3$) and T8 ($D=3$). The primitive root is $\omega:=e^{-i\pi/4}$, so $\omega^8=1$ and $|\omega|=1$. Matrix entries are $B_{t k}=\omega^{tk}/\sqrt{8}$; columns are the DFT modes.
Because $\omega$ lies on the unit circle, complex conjugation acts as inversion: $\overline{\omega^n}=\omega^{-n}$. That identity is recorded upstream as star_omega8_pow. The present lemma is the immediate cancellation $\overline{\omega^{tk}},\omega^{tk}=1$, i.e. each diagonal summand in a column inner product is exactly 1 before the $1/8$ normalization is restored.
Local setting: DFT-8 is the unique (up to phase/permutation) unitary basis that diagonalizes the cyclic shift, separates the DC mode from the neutral subspace, and supplies $\varphi$-lattice phases via complex exponentials.
proof idea
Rewrite the conjugate via star_omega8_pow, obtaining $\omega^{-(tk)},\omega^{tk}$. Fold the product into a single power with ← mul_pow, then apply inv_mul_cancel₀. The nonzero side-condition is discharged by unfolding omega8 to a complex exponential and using Complex.exp_ne_zero. The remaining goal is 1^{tk}=1, finished by one_pow. Short algebraic cancellation; no induction or case split on Fin 8.
why it matters
Feeds directly into dft8_column_orthonormal, the fundamental column orthonormality $\langle\mathrm{col}k,\mathrm{col}{k'}\rangle=\delta_{kk'}$. On the diagonal $k=k'$, every summand reduces to this identity (times the $1/8$ factor from the two $\sqrt{8}$ normalizations), so the sum is 1. Off-diagonal terms use geometric-sum vanishing of nontrivial powers of $\omega$.
Orthonormality is half of unitarity of the DFT-8 matrix (dft8_unitary), which in turn underwrites diagonalization of the cyclic shift and the split into DC versus neutral modes. In the Recognition chain this is the spectral backbone of the eight-tick octave (T7): time-translation eigenmodes on the forced period $2^D$ with $D=3$. Without the unit-modulus cancellation, the diagonal of the Gram matrix would not be identity.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.