dft8_mode
plain-language theorem explainer
The k-th eight-point DFT mode is the complex function on the eight-tick cycle equal to column k of the normalized DFT-8 matrix. Spectral and gap-weight arguments cite it as the canonical eigenbasis vector for frequency k. The definition simply reindexes the matrix entry ω^{t k}/√8 as a map in the time index t.
Claim. For each frequency index $k \in \{0,\ldots,7\}$, the $k$-th DFT-8 mode is the map $t \mapsto \omega^{t k}/\sqrt{8}$ from the eight-tick cycle into $\mathbb{C}$, where $\omega = e^{-2\pi i/8}$ is the primitive eighth root of unity.
background
The module builds the eight-point Discrete Fourier Transform as the canonical unitary basis for the eight-tick recognition cycle. Recognition Science forces period $2^3$ (T7), so signals live on $\mathrm{Fin},8$ and the natural time-translation is the cyclic shift.
The primitive root $\omega_8 = e^{-2\pi i/8}$ generates the phases. Matrix entries are $\omega_8^{t k}/\sqrt{8}$ (time index $t$, frequency $k$), which already include the unitary normalization. The cyclic shift on eight-tick signals advances the reading index by one tick mod 8; it is the discrete time-evolution generator used throughout the foundation and eight-tick Weyl layers.
Packaging column $k$ as a standalone mode lets later lemmas treat eigenvectors, difference energies, and gap weights as functions of a single frequency label rather than as matrix slices.
proof idea
Definitional one-liner: fix frequency $k$ and send each time index $t$ to the already-defined DFT-8 entry at $(t,k)$. No proof obligations beyond the noncomputable complex arithmetic in the entry formula.
why it matters
This mode is the workhorse object for the spectral side of Recognition Science. Downstream, the difference energy of mode $k$ equals $|\omega_8^k-1|^2$, which is the trig identity $4\sin^2(k\pi/8)$; that spectrum identity feeds the spectral-forcing factorization of geometric gap weight as (difference spectrum)/4 times the T9 lattice measure. The SpectralForcingCert bundles those closures.
On the operator side, every iterate of the cyclic shift acts on mode $k$ by the scalar $(\omega_8^k)^n$, and the modes sit in the neutral register used by the recognition operator. Column orthonormality (unit $\ell^2$ norm of each mode) is the projection lemma behind gap-weight normalizations. Together these place DFT-8 as the unique (up to phase/permutation) unitary basis that diagonalizes eight-tick time translation and separates DC from the mean-free subspace, matching the physical motivation of the module and the forced eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.