dft_coeff_zero
plain-language theorem explainer
The zero-frequency (DC) DFT-8 coefficient of any 8-vector equals the sum of its components divided by √8. Spectral and eight-tick analyses cite this to separate mean from neutral modes. The proof unfolds the coefficient definition, uses that √8 is real so conjugation is idle, and factors the constant out of the finite sum.
Claim. For every $v:\mathbb{Z}/8\mathbb{Z}\to\mathbb{C}$, the DC coefficient satisfies $c_0(v)=\bigl(\sum_{t=0}^{7}v(t)\bigr)/\sqrt{8}$, where $c_k(v)=\sum_t\overline{B_{t k}}\,v(t)$ and $B_{tk}=\omega^{tk}/\sqrt{8}$ with $\omega=e^{-2\pi i/8}$.
background
The DFT-8 module builds the canonical unitary basis for the eight-tick recognition cycle forced by $D=3$ (period $2^3$). Entries of the transform matrix are $B_{tk}=\omega^{tk}/\sqrt{8}$, with $\omega$ the primitive eighth root of unity. Coefficients of a vector $v$ are the inner products $c_k(v)=\sum_t\overline{B_{tk}},v(t)$ against the conjugated columns.
Mode $k=0$ is the constant (DC) column: every phase factor $\omega^{t\cdot 0}$ is $1$. The remaining modes $k=1..7$ span the mean-free (neutral) subspace, which the module later uses to diagonalize cyclic shift and separate conserved mean from oscillatory content.
Upstream, the entry and coefficient definitions fix the normalization $1/\sqrt{8}$ that makes the matrix unitary. Arithmetic facts such as multiplication by zero and the value of the zero quantity appear only as simp material when the frequency index is zero.
proof idea
Unfold the coefficient and entry definitions at frequency $0$. Simplification kills the phase ($t\cdot 0=0$, so $\omega^0=1$) and leaves a sum of $\overline{(\sqrt{8})^{-1}},v(t)$. A short complex-conjugation lemma shows $\overline{\sqrt{8}}=\sqrt{8}$ because the square root is real, so the star disappears. Commute the scalar past $v(t)$, pull $(\sqrt{8})^{-1}$ out of the finite sum via sum_mul, and finish by definitional equality with $(\sum v)/\sqrt{8}$.
why it matters
This identity is the DC half of the DFT-8 mean/neutral split. Downstream, dft_coeff_zero_of_neutral rewrites it under $\sum v=0$ to conclude that neutral vectors have vanishing DC coefficient, feeding the claim that modes $k=1..7$ span the mean-free subspace.
In the Recognition framework the eight-tick octave is landmark T7 (period $2^D$ with $D=3$ from T8). DFT-8 is the unique (up to phase/permutation) unitary basis that diagonalizes cyclic time translation and isolates the conserved mean. Without an explicit DC formula, neutrality and shift-eigenvalue arguments cannot separate $k=0$ cleanly from the oscillatory ladder.
The lemma is fully proved; it closes a routine but necessary algebraic step rather than an open scaffold.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.