omega8_inv_eq_pow7

The DFT-8 module builds the canonical unitary basis for the Recognition Science eight-tick cycle (period $2^3$, forced at T7). Its generator is the primitive root $\omega = e^{-\pi i/4}$, defined so that powers of $\omega$ label the discrete Fourier modes on an 8-vector register.

Periodicity $\omega^8 = 1$ is already recorded as a sibling fact. On the unit circle this forces the multiplicative inverse to sit at the complementary power: multiplying by $\omega^7$ walks one full turn back to 1. The same identity is the algebraic engine behind conjugating DFT entries, since $\overline{\omega} = \omega^{-1}$ on the circle.

Upstream, the local omega8 definition and omega8_pow_8 supply the root and its order; Mathlib supplies the field arithmetic on $\mathbb{C}$.

Start from the sibling lemma $\omega^8 = 1$. A short calc rewrites $\omega^7 \cdot \omega$ as $\omega^{7+1} = \omega^8 = 1$ via pow_add and norm_num. Non-vanishing of $\omega$ is Complex.exp_ne_zero. After mul_comm, Mathlib's eq_inv_of_mul_eq_one_right yields $\omega^{-1} = \omega^7$.

This is the elementary group-law fact that lets conjugation on DFT-8 modes become pure power arithmetic. Downstream, star_omega8_pow_mul_pow rewrites $\overline{\omega^n},\omega^m = \omega^{7n+m}$ by substituting this inverse identity; that lemma is the workhorse for unitary inner-product calculations on the eight-tick register.

It is also pulled into w8_dft_candidate_pos in the gap-weight formula stack, where positivity of a DFT-based candidate weight needs controlled powers of $\omega$. In the broader framework this sits under the T7 eight-tick octave and the spectral backbone that diagonalizes the cyclic shift on the recognition cycle.