dft_coefficients_mode
plain-language theorem explainer
The eight-point DFT of the j-th Fourier mode vector is the Kronecker delta at frequency k. Anyone working the RecognitionOperator sector projections or eight-tick spectral bookkeeping will cite this. The proof is a one-line reduction: unfold the coefficient and mode definitions, then apply column orthonormality of the DFT8 matrix.
Claim. For all indices $j,k \in \{0,\ldots,7\}$, the DFT coefficient of the $j$-th mode vector at frequency $k$ equals $1$ if $k=j$ and equals $0$ otherwise: $\widehat{e^{(j)}}_k = \delta_{jk}$.
background
The module builds the Recognition operator on eight-tick signals. The eight-point DFT is the spectral language for that discrete circle: each mode vector is a column of the unitary DFT8 matrix, and the coefficient map of a complex signal $v$ is the inner product against those columns, $c_k = \sum_t \overline{U_{t k}} v(t)$.
Upstream, dft8_column_orthonormal states the fundamental fact that those columns are orthonormal: $\langle \mathrm{col}k, \mathrm{col}{k'}\rangle = \delta_{k k'}$. The mode constructor simply exposes column $j$ as a function $\mathrm{Fin},8\to\mathbb{C}$. Together they make the coefficient-of-a-mode identity the discrete Fourier dual of orthonormality.
This sits in the Foundation layer that forces the eight-tick octave (T7 in the forcing chain): period $2^3$ is the discrete time lattice on which ledger channels and structured sectors are later projected.
proof idea
Term proof by definition chase. Unfold the coefficient functional and the mode vector so the left-hand side becomes exactly the inner product of DFT columns $k$ and $j$. Discharge with the already-proved column orthonormality theorem (arguments swapped to match the coefficient convention), which returns the Kronecker delta if k = j then 1 else 0.
why it matters
Sector projection on the Recognition operator needs to know that each pure DFT mode is an eigenvector of the keep/kill mask: either the mode is retained intact or it is sent to zero. The downstream lemma sectorProject_mode uses this identity inside a single-term sum argument to obtain that dichotomy.
In the broader framework this is bookkeeping for the eight-tick octave forced at T7: once modes are Kronecker-normalized, structured sectors (DC versus neutral register, active bonds, etc.) can be cut cleanly in the Fourier basis without cross-talk. It does not itself force dimension or the golden ratio; it supplies the spectral delta that later RecognitionOperator lemmas rely on when they classify channels.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.