dft8_preserves_inner
plain-language theorem explainer
Parseval identity for the eight-point DFT: the standard Hermitian product on signals Fin 8 → ℂ is invariant under the normalized DFT-8. Cited wherever unitarity of the recognition carrier's Fourier diagonalization is needed (complex-structure certificate, admissible evolution). Proof rewrites the local DFT as multiplication by the spectral DFT-8 matrix and applies that matrix's unitarity.
Claim. For all signals $f,g:\{0,\ldots,7\}\to\mathbb{C}$, writing $F$ for the normalized DFT-8, $F(f)(k)=8^{-1/2}\sum_j f(j)\,\overline{\zeta}^{kj}$, one has $\langle F(f),F(g)\rangle=\langle f,g\rangle$, where $\langle f,g\rangle=\sum_k\overline{f(k)}\,g(k)$.
background
The module Complex Structure Forcing shows that the T7 eight-tick shift $T$ on the ledger carrier cannot be diagonalized over $\mathbb{R}$: its spectrum is the 8th roots of unity, and $\omega^2=i$ has no real representative. Complexification is forced; the DFT-8 is the canonical unitary diagonalization.
A signal is a map $\mathrm{Fin},8\to\mathbb{C}$. The inner product is the standard Hermitian form $\langle f,g\rangle=\sum_k\overline{f(k)},g(k)$. The local DFT-8 is $F(f)(k)=(1/\sqrt{8})\sum_j f(j),\overline{\zeta}^{kj}$. An upstream lemma identifies this pointwise sum with multiplication by the spectral DFT-8 matrix, so matrix unitarity becomes available.
The doc-comment frames the claim as Parseval/Plancherel and notes the classical root-of-unity orthogonality $\sum_j\zeta^{(m-n)j}=8\delta_{mn}$ underlying the matrix fact.
proof idea
Tactic proof, not a one-line wrapper. Rewrite both sides' DFTs via the identification of the local transform with Matrix.mulVec against the spectral DFT-8 matrix. Change the goal into the equivalent star-dotProduct form of the Hermitian product. Then chain matrix identities: star of a mulVec, dotProduct through mulVec, and vecMul composition. The key algebraic step is the spectral lemma that the DFT-8 matrix is unitary, after which mulVec by the identity collapses the left-hand side to the original inner product.
why it matters
This is step 6 of the module argument: Parseval for DFT-8, the fact that makes the forced complex diagonalization unitary rather than merely algebraic. It is the dft_unitary field of the complex-structure certificate, which packages periodicity, the imaginary eigenvalue $i$, non-reality of $x^2+1$, DFT unitarity, and phase invariance of mode cost.
The immediate corollary is norm preservation $|F(f)|^2=|f|^2$. Downstream, admissible evolution is defined to preserve this inner product (and not increase total mode cost), so unitarity of recognition dynamics rests here. In the unified forcing chain it supports the T7-to-canonical-carrier bridge. Framework landmarks: T7 (eight-tick octave), closing the registry gap "complex Hilbert space from cost" between the J-cost axioms and genuine unitary structure on the carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.