dft_coefficients
plain-language theorem explainer
The unitary DFT-8 analysis map: each coefficient c_k is the inner product of an 8-vector against the conjugated k-th DFT mode. Spectral and RecognitionOperator developments cite it whenever signals are expanded in the eight-tick basis. The body is the standard analysis sum against dft8_entry.
Claim. For $v:\{0,\ldots,7\}\to\mathbb{C}$, the DFT-8 coefficients are $c_k=\sum_{t=0}^{7}\overline{B_{tk}}\,v_t$, where $B_{tk}=\omega^{tk}/\sqrt{8}$ and $\omega=e^{-2\pi i/8}$ is the primitive eighth root of unity.
background
The DFT8 module builds the canonical unitary basis for the eight-tick recognition cycle forced by the RS axioms (period $\tau_0=2^D$ with $D=3$). The primitive root $\omega_8=e^{-2\pi i/8}$ and the matrix entries $B_{tk}=\omega^{tk}/\sqrt{8}$ (time index $t$, frequency index $k$) are the raw ingredients.
Physically, DFT-8 is the unique (up to permutation and phase) unitary basis that diagonalizes cyclic time-translation, splits the DC mode $k=0$ from the seven neutral modes, and supplies $\varphi$-lattice phases via complex exponentials. The analysis map defined here is the dual of synthesis against those modes: coefficients are ordinary $\mathbb{C}^8$ inner products with conjugated columns of $B$.
proof idea
Pure definition, not a proved statement. For each frequency index $k$, sum over all time indices $t\in\mathrm{Fin},8$ the product of the conjugate of the DFT-8 entry $B_{tk}$ with the sample $v_t$. No lemmas are invoked; the body is exactly that finite sum.
why it matters
This is the analysis half of the eight-tick spectral calculus. Downstream, RecognitionOperator uses it for linearity of Fourier coefficients (additivity and scalar homogeneity), for the Kronecker identity on pure modes, and as the coefficient extractor inside the structured-sector projector that keeps a chosen set of Fourier modes. Inside DFT8 itself it feeds the neutral-subspace theorem: mean-free vectors have vanishing DC coefficient and therefore lie in the span of modes $1..7$. That separation of DC from neutral modes is the spectral counterpart of the eight-tick octave (forcing step T7) and underpins later recognition-operator constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.