roots_of_unity_sum_zero
plain-language theorem explainer
When the frequency index is zero, the sum of eighth-root powers ω^{t·0} over all eight time bins equals 8. Spectral and DFT-8 unitarity arguments cite this as the DC (k=0) case of the geometric root-of-unity sum. The proof is a one-line simplification: every term is 1, and Finset.sum_const counts eight copies.
Claim. Let $\omega$ be a primitive eighth root of unity. Then $\sum_{t=0}^{7} \omega^{t\cdot 0} = 8$. Equivalently, summing the constant $1$ over the eight time indices of the DFT-8 grid yields $8$.
background
The DFT-8 module builds the canonical unitary basis for the Recognition Science eight-tick cycle (period $2^3$, forced at T7). The primitive root is $\omega = e^{-i\pi/4}$, written omega8, with $\omega^8=1$. Matrix entries are $\omega^{tk}/\sqrt{8}$ at time $t$ and frequency $k$.
The classical geometric identity for roots of unity splits on the frequency index: $\sum_t \omega^{tk}$ equals $N$ when $k\equiv 0\pmod N$ and $0$ otherwise. This lemma is exactly the DC case $k=0$ for $N=8$. Upstream, omega8 is the complex exponential fixed in both the cycle-operator and DFT-8 layers; dft8_entry packages the normalized powers that unitarity and shift-diagonalization later use.
Physically, the $k=0$ mode is the constant (mean) mode on the eight-tick octave; its un-normalized inner product against the all-ones vector is this sum.
proof idea
Term-mode via a single simp step using Finset.sum_const. For every $t:\mathrm{Fin},8$, the exponent $t\cdot 0$ vanishes, so $\omega^{t\cdot 0}=\omega^0=1$. The universe of Fin 8 has cardinality 8, hence the sum of the constant function $1$ is $8$. No root-of-unity algebra beyond the zero exponent is required.
why it matters
DFT-8 is the spectral backbone of the eight-tick recognition cycle: it diagonalizes cyclic shift, separates the DC mode from the neutral (mean-free) subspace spanned by $k=1..7$, and supplies the $\varphi$-lattice phases. This lemma is the $k=0$ half of the geometric sum that underwrites column norms and the DC projection in that basis.
The module targets dft8_unitary, shift diagonalization, and the neutral-subspace claim. Even with no recorded downstream edges yet, any proof that the zeroth DFT column has un-normalized mass 8 (hence normalized mass 1 after $/\sqrt{8}$) needs precisely this identity. Framework landmark: T7 eight-tick octave ($\tau_0=2^D$, $D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.