dft8_preserves_norm
plain-language theorem explainer
DFT-8 preserves the squared Euclidean norm of any 8-tick complex signal: ‖F(f)‖² = ‖f‖². Cite this for Parseval unitarity of the eight-mode transform, Born-rule sector totals, or the T7-to-canonical-carrier bridge. The proof is a one-line specialization of full inner-product preservation to the diagonal case g = f.
Claim. For every signal $f:\mathrm{Fin}\,8\to\mathbb{C}$, the DFT-8 transform $F$ satisfies $\langle F(f),F(f)\rangle=\langle f,f\rangle$, equivalently $\|F(f)\|^2=\|f\|^2$, where the inner product is $\langle u,v\rangle=\sum_{k}\overline{u(k)}\,v(k)$.
background
The module Complex Structure Forcing shows that the T7 eight-tick shift on the ledger cannot be diagonalized over $\mathbb{R}$: its spectrum includes the 8th roots of unity, and $\omega^2=i$ has no real representative. Complexification is therefore forced, and the DFT-8 is the canonical unitary diagonalization of the cyclic shift.
A signal is a map $f:\mathrm{Fin},8\to\mathbb{C}$. The standard inner product is $\langle f,g\rangle=\sum_k\overline{f(k)},g(k)$. The DFT-8 is $F(f)(k)=(1/\sqrt{8})\sum_j f(j),\overline{\zeta}^{kj}$ with $\zeta=e^{2\pi i/8}$. The parent result is Parseval/Plancherel for DFT-8: $\langle F(f),F(g)\rangle=\langle f,g\rangle$ for all pairs, proved from orthogonality of roots of unity $\sum_j\zeta^{(m-n)j}=8\delta_{mn}$.
proof idea
One-line wrapper: instantiate the full inner-product preservation theorem at the pair $(f,f)$. No extra algebra is needed; the squared-norm identity is exactly the diagonal case of unitarity of DFT-8.
why it matters
Norm preservation is the concrete unitarity statement used downstream. Born-rule forcing applies it to show the total sector measure is DFT-invariant: $\mathrm{sectorMeasure}(F(\psi))=\mathrm{sectorMeasure}(\psi)$, via rewriting the self-inner-product as a real squared norm. In the unified forcing chain it appears in the T7-to-canonical-carrier bridge, which names $\mathrm{Signal8}=\mathrm{Fin},8\to\mathbb{C}$ as the carrier supporting a faithful 8-tick representation with $i$ in the spectrum and DFT-8 as the unitary diagonalization.
Framework landmarks: T7 (eight-tick octave, period $2^3$) forces the cyclic shift; this corollary closes the Parseval step in the module argument that cost axioms plus T7 yield complex Hilbert structure and genuine unitarity. It sits between full Plancherel and the later claim that the recognition operator preserves admissibility iff it is unitary, and that $J$-cost depends only on moduli (phase invariance).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.