dft8_matrix
plain-language theorem explainer
Packages the eight-point DFT into a single 8×8 complex matrix whose (t,k) entry is ω^{tk}/√8. Anyone citing the DFT-8 unitary basis, shift diagonalization, or Parseval identity for the eight-tick cycle uses this object. The body is a one-line pointwise wrapper around the entry formula.
Claim. Let $\omega = e^{-2\pi i/8}$. Define the $8\times 8$ matrix $B$ over $\mathbb{C}$ by $B_{t,k} = \omega^{tk}/\sqrt{8}$ for time index $t\in\{0,\ldots,7\}$ and frequency index $k\in\{0,\ldots,7\}$.
background
The module builds the DFT-8 backbone for the eight-tick recognition cycle. Recognition Science forces period $\tau_0 = 2^D$ with $D=3$ (T7/T8), so the natural spectral window is length 8. The primitive root is $\omega = e^{-2\pi i/8}$; matrix entries are the normalized characters $\omega^{tk}/\sqrt{8}$.
Upstream, dft8_entry supplies exactly that scalar: entry $(t,k)$ equals $\omega^{t\cdot k}/\sqrt{8}$. The matrix definition lifts the scalar family to Mathlib's Matrix (Fin 8) (Fin 8) ℂ, so conjugation, multiplication, and mulVec apply directly. Columns are the DFT modes; the cyclic shift on 8-vectors is the time-translation generator that DFT is meant to diagonalize.
proof idea
Definition only: the matrix is the function $(t,k)\mapsto$ the already-defined DFT-8 entry at $(t,k)$. No proof obligations beyond noncomputability inherited from complex exponentials and real square root.
why it matters
This is the canonical unitary object for the eight-tick octave (T7). Downstream, unitarity ($B^H B = I$) and shift diagonalization ($B^H S B = \mathrm{diag}(1,\omega,\ldots,\omega^7)$) are stated directly in terms of it; the conjugate-transpose identity that feeds those proofs multiplies against this matrix. In ComplexStructureForcing, the abstract DFT on signals is identified with mulVec by this matrix, and Parseval/Plancherel is reduced to that identification. The uniqueness-up-to-phase hypothesis also quantifies over unitary matrices that diagonalize the same shift, with this matrix as the reference basis. Without a single matrix object, the spectral claims stay entrywise and cannot use Mathlib matrix algebra.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.