dft8_mode_zero_constant
plain-language theorem explainer
The zero-frequency DFT-8 mode is the constant (DC) vector: every time slot equals $1/\sqrt{8}$. Spectral constructions that split mean from mean-free eight-tick modes cite this. The proof unfolds the mode and matrix-entry definitions, then simplifies with $t\cdot 0=0$ and $\omega^0=1$.
Claim. For every time index $t\in\{0,\ldots,7\}$, the DFT-8 basis mode at frequency $k=0$ satisfies $(\mathrm{mode}_0)_t = 1/\sqrt{8}$.
background
The module builds the 8-point Discrete Fourier Transform as the canonical unitary basis for the Recognition Science eight-tick cycle (period $2^3$, forced at T7). The primitive root is $\omega=e^{-2\pi i/8}$. Matrix entries are
$$\mathrm{dft8_entry}(t,k)=\omega^{tk}/\sqrt{8},$$
and the $k$-th mode is column $k$ of that matrix (a vector in $\mathbb{C}^8$ indexed by time $t\in\mathrm{Fin},8$).
Frequency $k=0$ is the DC channel: the phase factor collapses because the exponent is $t\cdot 0$. Downstream, modes $k=1..7$ are required to be orthogonal to this constant mode (mean-free / neutral subspace). The physical motivation is that DFT-8 uniquely (up to permutation and phase) diagonalizes cyclic time shift and separates DC from neutral content on the eight-tick octave.
proof idea
Term-style tactic proof. Introduce the time index $t$. Unfold the mode as the corresponding column of entries, then unfold the entry formula $\omega^{t\cdot k}/\sqrt{8}$ at $k=0$. Simplify: $t\cdot 0=0$ (mul_zero) and $\omega^0=1$ (pow_zero), leaving the constant $1/\sqrt{8}$ independent of $t$. No external spectral lemmas are required.
why it matters
This is the DC half of the DFT-8 mean/neutral split. It is wired directly into standardDFT8Basis as the field mode_zero_dc, which packages modes, DC constancy, neutrality of $k=1..7$, and column orthonormality into the EightTickBasis interface.
In the framework, the eight-tick period is the T7 landmark ($\tau_0=2^D$ with $D=3$ from T8). A unitary basis that diagonalizes cyclic shift and isolates the constant mode is the spectral backbone for recognition-cycle analysis: conserved mean versus fluctuating neutral content, and later $\varphi$-lattice quantization via complex exponentials. Without an explicit constant zero-mode, the neutral-subspace theorems and shift-diagonalization story do not close.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.