dft8_mode_mem_neutralRegister
plain-language theorem explainer
Every non-DC length-8 DFT mode has vanishing sum over the eight ticks, hence lies in the neutral (mean-free) register of the 8-tick carrier. Anyone embedding Fourier modes into the recognition operator cites this. The proof factors out the DFT normalization and invokes the geometric-sum vanishing of non-trivial 8th roots of unity.
Claim. For every frequency index $k \in \{0,\ldots,7\}$ with $k \neq 0$, the corresponding length-8 DFT mode vector belongs to the neutral register: the sum of its eight complex samples is zero.
background
The 8-tick carrier is the complex vector space of signals indexed by $\mathrm{Fin},8$, the discrete octave forced by the Recognition chain (T7). The neutral register is the mean-free subspace: those signals whose sum over all eight ticks vanishes. It is the natural home for oscillatory content once the DC (global mean) channel has been split off.
DFT-8 modes are the standard Fourier basis on this carrier. Mode $k$ has samples proportional to $\omega^{t k}$, where $\omega = e^{2\pi i/8}$ is the primitive eighth root of unity. The DC mode ($k=0$) is the constant vector and sits outside the neutral register; every other mode is a non-trivial character of the cyclic group of order 8.
Upstream, the geometric sum of a non-trivial power of $\omega$ over a full period is zero. That classical roots-of-unity identity is the only analytic input needed here.
proof idea
Membership in the neutral register is definitionally the claim that the sum of the eight DFT entries for fixed $k$ equals zero. Unfold the DFT entry formula, rewrite the normalization factor as a reciprocal, and pull the common scalar $(\sqrt{8})^{-1}$ out of the sum. What remains is $\sum_t \omega^{t k}$. The hypothesis $k\neq 0$ makes this a non-trivial geometric sum of eighth roots of unity, which vanishes by the standard roots-of-unity sum lemma. Scaling the zero sum by the DFT factor keeps it zero.
why it matters
This lemma is the mode-wise step that feeds quarterTurnCore_le_neutralRegister: the odd Fourier span (the quarter-turn core) sits inside the neutral register. That inclusion keeps the recognition operator's oscillatory sector mean-free, so global phase and DC bookkeeping stay cleanly separated from the eight-tick dynamics.
In the broader framework it is a concrete instance of the T7 eight-tick octave: the DFT basis on period $2^3$ is compatible with the mean-free ledger subspace used by the recognition operator. Without non-DC modes living in the neutral register, later bounds that compare quarter-turn cores to neutral content would not type-check.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.