dft8_neutral_subspace
plain-language theorem explainer
Any mean-free complex 8-vector lies in the complex span of the seven non-DC DFT-8 modes. Spectral work on the eight-tick recognition cycle cites this to split the DC channel from the neutral subspace. The proof expands v by the inverse DFT, drops the vanishing k=0 coefficient, and closes under submodule span and scalar multiplication.
Claim. For every $v:\mathbb{F}_8\to\mathbb{C}$ with $\sum_t v(t)=0$, one has $v\in\mathrm{span}_{\mathbb{C}}\{m_k:k\in\{1,\ldots,7\}\}$, where $m_k$ denotes the $k$-th DFT-8 mode (column $k$ of the unitary 8-point DFT matrix).
background
The DFT-8 module supplies the canonical unitary basis for the eight-tick recognition cycle. Recognition Science forces period $\tau_0=2^D$ with $D=3$ (T7 eight-tick octave, T8 spatial dimension), so the natural spectral object is the 8-point DFT. Entries are built from the primitive root $\omega=e^{-2\pi i/8}$ as $\omega^{tk}/\sqrt{8}$; the $k$-th mode is column $k$ of that matrix.
A vector on eight ticks is neutral (mean-free) when its sum vanishes. Mode $k=0$ is the constant DC channel; modes $k=1..7$ are the non-DC directions. The inverse DFT expands any $v$ as $\sum_k c_k,m_k$ with coefficients from the forward transform. Neutrality forces the DC coefficient to vanish, which is the algebraic content used here.
proof idea
Introduce $v$ and the sum-zero hypothesis. Apply the lemma that neutrality implies vanishing DC coefficient. Rewrite $v$ via the inverse DFT expansion as $\sum_k c_k\cdot m_k$, matching pointwise after unfolding mode definitions and scalar action.
Erase $0$ from the finite universe sum so the $k=0$ term splits off; that term is zero by the DC coefficient and zero_add. The residual sum over $k\neq 0$ lies in the target submodule: each summand is a scalar multiple of a non-DC mode (hence in the generating set), and the submodule is closed under sums and scalar multiplication.
why it matters
Among the module's main results, this is the statement that modes $k=1..7$ span the neutral subspace, giving the clean DC/neutral split required of any spectral basis for the eight-tick register. Downstream, dft8_neutral_subspace_hypothesis_holds is the one-line discharge of the former hypothesis interface by direct application of this theorem, turning a named assumption into a proved fact before the uniqueness section.
In the Recognition framework the eight-tick octave (T7) and $D=3$ (T8) force DFT-8 as the backbone that diagonalizes cyclic shift and separates DC from mean-free modes. Later representation-theoretic uniqueness arguments (bases unique up to permutation and phase among those that diagonalize shift and split DC) sit on top of this span fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.