dft8_preserves_inner
plain-language theorem explainer
Parseval identity for the length-8 discrete Fourier transform: the DFT-8 map preserves the Hermitian inner product on eight-tick signals, so it is unitary. Anyone building the complex-structure certificate or admissible evolution operators cites this fact. The OperatorCore copy is a pure re-export abbrev of the Foundation theorem proved via roots-of-unity orthogonality.
Claim. For any two length-8 complex signals $f,g$, the DFT-8 satisfies $\langle \widehat{f},\widehat{g}\rangle = \langle f,g\rangle$. Equivalently, DFT-8 is a unitary operator on the eight-tick carrier.
background
In the complex-structure forcing module, an eight-tick signal is a map from the cyclic index set of size 8 into $\mathbb{C}$. The DFT-8 is the standard discrete Fourier transform on that carrier; its matrix entries are powers of a primitive 8th root of unity. The Hermitian inner product inner8 is the usual $\ell^2$ pairing $\langle f,g\rangle = \sum_j \overline{f_j} g_j$.
The upstream theorem states the Plancherel identity $\langle F(f),F(g)\rangle=\langle f,g\rangle$ and notes that the proof rests on the geometric-sum orthogonality $\sum_j \zeta^{(m-n)j}=8\delta_{mn}$. This OperatorCore declaration simply aliases that theorem so the operator-core layer can name the unitary property without importing the full proof body.
Local siblings include the shift operator of period 8, the mode-cost functional built from the complexified $J$-cost, and the UnitaryEvolution structure that packages inner-product preservation with cost non-increase.
proof idea
No independent proof: the declaration is an abbrev that points at the Foundation theorem of the same name. That theorem rewrites both sides via the matrix form of DFT-8, reduces the claim to a star-mulVec identity for the DFT matrix, and discharges it from roots-of-unity orthogonality (the classical Plancherel argument for finite cyclic groups).
why it matters
Unitary of DFT-8 is one of the five fields of complex_structure_certificate (dft_unitary := dft8_preserves_inner). The norm-preservation corollary is the diagonal case, and UnitaryEvolution requires exactly this inner-product identity for admissible evolve maps. Downstream, the T7-to-canonical-carrier bridge in the unified forcing chain consumes the eight-tick periodicity that sits beside this fact; together they lock the complex structure forced by the eight-tick octave (T7) into a unitary spectral picture. Without Plancherel, mode-cost phase invariance and Hamiltonian emergence in the small-deviation limit would lack a unitary carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.