dft8_entry
plain-language theorem explainer
Defines the normalized DFT-8 matrix entry at time index t and frequency index k as ω^{tk}/√8, with ω the primitive eighth root of unity. Anyone working the eight-tick spectral basis, gap-weight DFT coefficients, or sector projectors cites this. The body is a direct one-line formula in terms of the local root of unity.
Claim. For indices $t,k\in\{0,\ldots,7\}$, the DFT-8 matrix entry is $B_{t k}=\omega^{t k}/\sqrt{8}$, where $\omega=e^{-2\pi i/8}$ is the primitive eighth root of unity used in this module.
background
The module builds the eight-point discrete Fourier transform as the canonical unitary basis for the Recognition Science eight-tick cycle. That period is forced as $\tau_0=2^D$ with $D=3$ (T7–T8 in the forcing chain), so the natural spectral window is length 8.
The local primitive root is $\omega=e^{-\pi i/4}=e^{-2\pi i/8}$. (A sibling foundation definition uses the opposite phase convention $e^{+2\pi i/8}$; this module standardizes on the negative-frequency DFT convention.) Entries are indexed by a time (row) index $t$ and a frequency (column) index $k$ on $\mathrm{Fin},8$.
Normalization by $\sqrt{8}$ makes the full matrix unitary, so columns are orthonormal modes: DC ($k=0$) versus the mean-free neutral modes ($k=1..7$). Those modes diagonalize the cyclic shift and supply the spectral coordinates used throughout the recognition operator and gap-weight calculus.
proof idea
Pure definition: evaluate $\omega^{t\cdot k}/\sqrt{8}$ using the module's omega8 and the natural numbers underlying the two Fin 8 indices. No proof obligations beyond the ambient complex arithmetic.
why it matters
This is the atomic building block of the DFT-8 backbone. Downstream, the full matrix, its columns (dft8_mode), and column orthonormality are assembled from these entries; complex-structure forcing equates the abstract DFT map to multiplication by that matrix.
Gap-weight work uses the entries to form $\varphi$-pattern DFT coefficients and to prove the DFT-based candidate weight is positive. The recognition operator uses them for neutral-register membership of non-DC modes and for sector projectors that keep chosen Fourier modes.
In framework terms it realizes the unique (up to permutation/phase) unitary basis that diagonalizes time-translation on the forced eight-tick octave and separates DC from neutral modes, enabling $\varphi$-lattice spectral quantization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.