dft8_neutral_subspace_hypothesis
plain-language theorem explainer
Mean-free complex 8-vectors lie in the complex span of the seven non-DC DFT-8 modes. Spectral and eight-tick work cites this Prop as the neutral-subspace claim. It is a legacy named hypothesis whose body is the standard mean-zero span statement; a sibling theorem discharges it by the proved neutral-subspace lemma.
Claim. Every $v:\mathbb{F}_8\to\mathbb{C}$ with $\sum_t v(t)=0$ lies in the $\mathbb{C}$-span of $\{\mathrm{DFT\text{-}8\ mode}\,k:k\in\{1,\ldots,7\}\}$.
background
The DFT-8 module treats the 8-point discrete Fourier transform as the canonical unitary basis for the Recognition Science eight-tick 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}$. Each mode $k$ is the corresponding column of that unitary matrix.
The DC mode ($k=0$) is the constant vector. The neutral (mean-free) subspace is the hyperplane of vectors with vanishing sum of components. The module's main results include unitarity of DFT-8, diagonalization of the cyclic shift, and the statement that modes $k=1..7$ span that neutral subspace.
This declaration packages that span claim as a named Prop (legacy alias). The mode vectors themselves are the only local ingredient in the statement.
proof idea
No proof: the declaration is a definition of a proposition. The body is the universal quantification over mean-zero $v:\mathrm{Fin},8\to\mathbb{C}$ and membership in the complex span of ${dft8_mode,k:k\neq 0}$. Discharge is deferred to the sibling theorem that applies the proved neutral-subspace lemma.
why it matters
In the eight-tick backbone, separating DC from neutral modes is one of the three design requirements that make DFT-8 the canonical spectral basis (alongside diagonalizing cyclic shift and supporting $\varphi$-lattice phases). The forcing chain fixes the octave period $2^3$ (T7) and $D=3$ (T8), so this seven-dimensional neutral span is the spectral home for mean-free recognition signals on the tick cycle.
Downstream, dft8_neutral_subspace_hypothesis_holds asserts the Prop and proves it by the existing neutral-subspace theorem, with the doc-comment "The hypothesis is now a theorem." The alias therefore exists only for compatibility with older hypothesis-shaped call sites, not as an open gap.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.