dft_coeff_zero_of_neutral
plain-language theorem explainer
Any mean-free 8-vector has vanishing DC Fourier coefficient. Spectral and eight-tick arguments cite this to drop the k=0 mode when expanding neutral signals. The proof is a one-line rewrite through the explicit DC formula (sum)/√8.
Claim. If $v:\mathbb{F}_8\to\mathbb{C}$ satisfies $\sum_{t} v(t)=0$, then its DFT coefficient at frequency $0$ vanishes: $c_0(v)=0$.
background
The DFT-8 module treats the eight-tick recognition cycle (period $2^3$, forced at T7 with $D=3$) as the domain of an 8-point unitary DFT. Modes are columns of the matrix with entries $\omega^{tk}/\sqrt{8}$, where $\omega=e^{-2\pi i/8}$. Coefficients are $c_k(v)=\sum_t \overline{\mathrm{mode}_k(t)},v(t)$.
Neutrality means vanishing total mass: $\sum_t v(t)=0$. The DC (zero-frequency) mode is the constant vector; its coefficient measures the mean. Upstream, dft_coeff_zero records the closed form $c_0(v)=(\sum v)/\sqrt{8}$. That identity is the only input needed here.
proof idea
One-line rewrite. Apply the DC formula $c_0(v)=(\sum v)/\sqrt{8}$, substitute the neutrality hypothesis $\sum v=0$, then use $0/\sqrt{8}=0$. No further spectral structure is used.
why it matters
Feeds dft8_neutral_subspace, which states that modes $k=1..7$ span the mean-free subspace: any neutral $v$ expands as $\sum_{k\neq 0} c_k,\mathrm{mode}_k$ once $c_0=0$ is known. That separation of DC from neutral modes is listed among the module's main results and is part of why DFT-8 is the canonical basis for the eight-tick cycle (diagonalizes cyclic shift, isolates mean-free dynamics). In the forcing chain this sits under T7 (eight-tick octave) and T8 ($D=3$).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.