dft8_eq_mulVec
plain-language theorem explainer
The local eight-point DFT on the 8-tick signal space equals left-multiplication by the canonical DFT-8 matrix. Anyone proving unitarity or Parseval for the Recognition Science DFT cites this identification. The argument is a pointwise sum comparison: conjugate root powers become ω₈ powers, and the 1/√8 factor is rearranged to match the matrix entries.
Claim. For every signal $f:\{0,\ldots,7\}\to\mathbb{C}$, the DFT-8 transform $F(f)$ equals the matrix-vector product of the canonical DFT-8 matrix with $f$.
background
This module forces complex structure from the 8-tick cycle (T7): the cyclic shift $T$ on the ledger has $T^8=I$, its eigenvalues are the eighth roots of unity, and $\omega^2=i$ has no real square root, so diagonalization over $\mathbb{R}$ is impossible. The DFT-8 is the canonical unitary that diagonalizes $T$ over $\mathbb{C}$.
A signal is a map $f:\mathrm{Fin},8\to\mathbb{C}$. The local transform is $F(f)(k)=(1/\sqrt{8})\sum_j f(j),\overline{\zeta}^{kj}$. The spectral library supplies the matching matrix whose $(k,j)$-entry is $\omega_8^{kj}/\sqrt{8}$, with $\omega_8=e^{2\pi i/8}$.
The lemma star_ζ_pow_eq_omega8_pow identifies the conjugate powers in the local sum with the matrix phases, so the two presentations of DFT-8 can be compared entrywise.
proof idea
Apply function extensionality on the output index $k$. Unfold both sides to sums over $j\in\mathrm{Fin},8$. Factor $1/\sqrt{8}$ out of the left-hand sum, then compare summands. Rewrite the conjugate power via star_ζ_pow_eq_omega8_pow, unfold the spectral matrix entry, and clear the nonzero $\sqrt{8}$ denominator. The remaining equality is a short ring rearrangement (mul_assoc, mul_comm, mul_left_comm) matching $f(j)\cdot\omega_8^{kj}/\sqrt{8}$ on both sides.
why it matters
Parseval for DFT-8 (dft8_preserves_inner) opens by rewriting both transforms as matrix-vector products via this lemma, then invokes unitarity of the spectral DFT matrix. That unitarity step is the bridge from the 8-tick shift to a genuine complex Hilbert structure: inner-product preservation, phase invariance of $J$-cost (which depends only on moduli), and the claim that admissibility-preserving maps are unitary.
In the forcing chain this sits under T7 (eight-tick octave) and supports the module thesis that complexification is algebraically forced, not optional. It closes part of the registry gap "complex Hilbert space from cost," feeding the path from cost axioms to operator unitarity on the finite 8-tick register.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.