roots_of_unity_sum
plain-language theorem explainer
For any nonzero frequency index k mod 8, the sum of the eight powers ω^{tk} vanishes. Spectral and recognition-operator arguments cite this to separate DC from mean-free DFT modes on the eight-tick cycle. The proof rewrites the sum as a geometric series in ζ=ω^k, uses ζ^8=1 and ζ≠1, then cancels via the telescoping identity (sum)·(ζ−1)=ζ^8−1.
Claim. Let $\omega=e^{2\pi i/8}$ be a primitive eighth root of unity. For every $k\in\{0,\ldots,7\}$ with $k\neq 0$, $$\sum_{t=0}^{7}\omega^{tk}=0.$$
background
The DFT-8 module builds the canonical unitary basis for the eight-tick recognition cycle forced by T7 (period $2^3$ with $D=3$). The primitive root is $\omega_8=e^{2\pi i/8}$, written omega8 in the codebase; the DFT matrix entries are $\omega^{tk}/\sqrt{8}$.
Modes of the transform split into the DC column ($k=0$) and the seven neutral (mean-free) columns. Vanishing of $\sum_t\omega^{tk}$ for $k\neq 0$ is the elementary roots-of-unity fact that makes those columns orthogonal to the constant vector.
Upstream, $\omega^8=1$ is recorded as omega8_pow_8, and non-triviality $\omega^m\neq 1$ for $0<m<8$ is supplied by omega8_pow_ne_one_axiom. The geometric-series cancellation then lives entirely in $\mathbb{C}$.
proof idea
Set $\zeta:=\omega^k$. Commutativity of multiplication and pow_mul rewrite the target sum as $\sum_{t=0}^{7}\zeta^t$. From $\omega^8=1$ one gets $\zeta^8=1$. Positivity of $k.val$ plus omega8_pow_ne_one_axiom give $\zeta\neq 1$, hence $\zeta-1\neq 0$.
Expand the finite sum via Fin.sum_univ_eight and apply ring to obtain the telescoping identity
$(\sum_{t=0}^{7}\zeta^t)\cdot(\zeta-1)=\zeta^8-1$.
Substitute $\zeta^8=1$ so the right-hand side is $0$, then use mul_eq_zero and discard the $\zeta-1$ factor to conclude the sum is zero.
why it matters
This is the algebraic engine behind mean-free DFT modes on the eight-tick octave. Downstream, dft8_mode_neutral quotes it directly to show $\sum_t(\mathrm{dft8_mode},k)_t=0$ for $k\neq 0$; dft8_mode_mem_neutralRegister lifts the same identity into the recognition-operator neutral register; and dft8_column_orthonormal uses the same geometric cancellation in the off-diagonal inner products that prove unitarity of the DFT-8 matrix.
In the Recognition Science chain this sits under T7 (eight-tick period $2^3$) and the spectral backbone that diagonalizes cyclic time translation. Without the vanishing sum, DC cannot be cleanly split from the neutral subspace that carries the nontrivial recognition dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.