dft8_neutral_subspace_hypothesis_holds
plain-language theorem explainer
The DFT-8 neutral-subspace claim is fully proved: Fourier modes k=1..7 span the mean-free subspace of C^8, orthogonal to the DC mode. Spectral and eight-tick analyses cite this to separate conserved mean from fluctuating content on the recognition cycle. The proof is a one-line term that discharges the former hypothesis by the existing neutral-subspace theorem.
Claim. The DFT-8 neutral-subspace hypothesis holds: the modes $k=1,\ldots,7$ of the eight-point discrete Fourier transform span the mean-free (neutral) subspace of $\mathbb{C}^8$, i.e., the orthogonal complement of the constant (DC) mode.
background
The module builds the eight-point DFT as the canonical unitary basis for the Recognition Science eight-tick cycle. The primitive root is $\omega=e^{-2\pi i/8}$; matrix entries are $\omega^{tk}/\sqrt{8}$. Columns are the DFT modes, and the cyclic shift on eight-vectors is diagonalized by this basis, with eigenvalue $\omega^k$ on mode $k$.
Neutral means mean-free: the seven modes $k=1,\ldots,7$ are exactly the subspace orthogonal to the constant $k=0$ (DC) mode. Module motivation ties the period $\tau_0=2^D$ with $D=3$ to the forced eight-tick octave, so separating DC from neutral modes is the spectral split between conserved mean and fluctuating recognition content.
The named hypothesis was the Prop-shaped stand-in for that spanning statement; the sibling theorem already proves modes $k=1..7$ span the neutral subspace. This declaration simply records that the hypothesis is now a theorem.
proof idea
One-line term proof. The goal is the neutral-subspace hypothesis Prop; the term is the existing theorem that modes $k=1,\ldots,7$ span the mean-free subspace. No extra tactics, rewrites, or side conditions: the proved spanning statement is definitionally the content of the hypothesis, so supplying it closes the goal.
why it matters
Closes a hypothesis interface inside the DFT-8 backbone: the spectral split between DC and neutral modes is no longer conditional scaffolding. That split is part of what makes DFT-8 the canonical basis for the eight-tick recognition cycle (primer T7: period $2^3$; T8: $D=3$), alongside unitarity and diagonalization of the cyclic shift.
No downstream consumers are wired yet in the graph, so this is a local discharge rather than a leaf of a larger proved chain. It still removes an open hypothesis from the spectral layer that any later eight-tick mode analysis, mean-free projection, or $\varphi$-lattice quantization via complex exponentials would need. The nearby uniqueness discussion (DFT-8 unique up to permutation and phase among shift-diagonalizing bases) remains separate and is not settled here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.