dft8_mode_neutral
plain-language theorem explainer
Nonzero DFT-8 modes (k = 1..7) are mean-free: their eight complex entries sum to zero, so they are orthogonal to the constant (DC) mode. Anyone building the eight-tick spectral basis or the neutral subspace cites this. The proof factors 1/√8 out of the sum and applies the geometric sum of nontrivial eighth roots of unity.
Claim. For every mode index $k \in \{0,\ldots,7\}$ with $k \neq 0$, if $m_k$ is the $k$-th DFT-8 basis vector with entries $m_k(t) = \omega^{tk}/\sqrt{8}$ ($\omega = e^{2\pi i/8}$, $t = 0,\ldots,7$), then $\sum_{t=0}^{7} m_k(t) = 0$.
background
The DFT-8 module supplies the canonical unitary basis for the forced eight-tick recognition cycle ($\tau_0 = 2^D$ with $D = 3$). The primitive root is $\omega = e^{2\pi i/8}$; matrix entries are $\omega^{tk}/\sqrt{8}$. The $k$-th mode is column $k$ of that matrix, viewed as an 8-vector in $\mathbb{C}^8$.
Physically and algebraically one splits the DC mode $k = 0$ (the constant vector) from the neutral modes $k = 1..7$. Neutrality means mean-free: the sum of coordinates vanishes, equivalently orthogonality to the all-ones vector. The module lists this separation among the three defining properties of the DFT-8 basis (diagonalize cyclic shift; separate DC from neutral; supply $\varphi$-lattice phases via complex exponentials).
The algebraic engine is the classical roots-of-unity filter: for $k \not\equiv 0 \pmod{8}$, $\sum_{t=0}^{7} \omega^{tk} = 0$. Scaling by the constant $1/\sqrt{8}$ preserves the vanishing.
proof idea
Unfold the mode and entry definitions so the claim is $\sum_t \omega^{t k}/\sqrt{8} = 0$. Invoke the roots-of-unity sum lemma to obtain $\sum_t \omega^{t k} = 0$ from $k \neq 0$. Pull the constant factor $(\sqrt{8})^{-1}$ out of the finite sum via Finset.sum_mul (in the reverse direction). Rewrite division as multiplication by the inverse and substitute the zero sum to finish. Purely algebraic; no analysis beyond the complex exponential definition of $\omega$.
why it matters
This lemma is the neutrality half of the standard DFT-8 basis instance: standardDFT8Basis packages modes, DC constancy, neutrality of $k\neq 0$, and column orthonormality into one EightTickBasis record. Downstream spectral arguments that need the mean-free subspace (the orthogonal complement of the constant mode) therefore rest on it.
In the Recognition framework this is the spectral face of the eight-tick octave (forcing step T7, period $2^3$). The DFT-8 basis is advertised as the unique (up to permutation/phase) unitary frame that diagonalizes cyclic time translation and cleanly splits DC from neutral modes; without mean-free modes that split fails. It also feeds the larger claim that modes $k=1..7$ span the neutral subspace, which is the natural home for oscillatory recognition content once the constant offset is removed.
No open scaffold: the lemma is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.