dft8_column_orthonormal
plain-language theorem explainer
Columns of the 8-point DFT matrix are orthonormal: their Hermitian inner product equals the Kronecker delta. Anyone building unitary spectral bases for the eight-tick recognition cycle cites this. The proof expands entries in powers of the primitive eighth root of unity, factors the 1/8 normalization, and splits into diagonal (eight ones) versus off-diagonal (vanishing geometric sum of a nontrivial root of unity).
Claim. For all mode indices $k,k'\in\{0,\ldots,7\}$, $\sum_{t=0}^{7}\overline{B_{tk}}\,B_{tk'}=\delta_{k,k'}$, where $B_{tk}=\omega^{tk}/\sqrt{8}$ is the DFT-8 matrix entry and $\omega=e^{2\pi i/8}$ is a primitive eighth root of unity.
background
The module formalizes the 8-point Discrete Fourier Transform as the canonical unitary basis for the 8-tick recognition cycle. Recognition Science forces period $\tau_0=2^D$ with $D=3$ (T7 eight-tick octave, T8), so the natural spectral window has length 8.
The primitive root $\omega_8=e^{2\pi i/8}$ satisfies $\omega_8^8=1$. Matrix entries are $B_{tk}=\omega_8^{tk}/\sqrt{8}$. Columns of $B$ are the DFT modes; the claim is that these eight complex vectors form an orthonormal set under the standard Hermitian product on $\mathbb{C}^8$.
Upstream facts include $\omega_8^8=1$ and product identities for conjugated powers of $\omega_8$. The same root appears in the cycle operator encoding time-translation on the eight-tick lattice. The module doc states DFT-8 is the unique (up to permutation/phase) unitary basis that diagonalizes cyclic shift and separates DC from neutral modes.
proof idea
Expand each summand by the entry formula: $\overline{B_{tk}}B_{tk'}=\overline{\omega^{tk}}\omega^{tk'}/8$. Factor the constant $1/8$ out of the finite sum over $\mathrm{Fin},8$.
Diagonal case $k=k'$: each term equals $|\omega^{tk}|^2=1$ (star-power times same power), so the unnormalized sum is 8 and the normalized value is 1.
Off-diagonal: rewrite $\sum_t\overline{\omega^{tk}}\omega^{tk'}=\sum_t\omega^{t(7k+k')}$ via the conjugate identity $\overline{\omega^m}=\omega^{7m}$. Reduce the frequency modulo 8 to a $\mathrm{Fin},8$ residue; that residue is nonzero precisely when $k\neq k'$ (since $7k+k'\equiv -k+k'\pmod 8$). The geometric sum of a nontrivial eighth root of unity over a full period vanishes, so the normalized sum is 0.
why it matters
This is the column half of unitarity for the DFT-8 matrix. The unitarity theorem assembles $B^H B=I$ entrywise from it; row orthonormality follows by the symmetry $B_{tk}=B_{kt}$. The standard eight-tick basis instance records column orthonormality as its modes-orthonormal field.
Gap-weight projection uses the diagonal case to prove each mode has unit squared-norm sum. The recognition operator uses it to show DFT coefficients of a pure mode are Kronecker-normalized. A related shift-conjugation identity also consumes the same inner-product structure.
Together with diagonalization of the cyclic shift, this pins DFT-8 as the spectral backbone of the forced eight-tick octave (T7, period $2^3$). It separates the DC mode from the seven-dimensional neutral subspace that carries mean-free recognition dynamics.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.