isNormalized_dft8
plain-language theorem explainer
The eight-mode discrete Fourier transform preserves unit total mass: if a signal has sum of squared mode norms equal to one, so does its DFT-8 image. Anyone citing Parseval-based Born-rule forcing on the eight-tick octave needs this fact. The proof is a one-line rewrite through the total-sector Parseval corollary, then the normalisation hypothesis.
Claim. If $\psi$ is an eight-mode complex signal with $\sum_{k=0}^{7}\|\psi_k\|^2=1$, then its DFT-8 transform $F\psi$ is likewise normalised: $\sum_{k=0}^{7}\|(F\psi)_k\|^2=1$.
background
The module forces the Born probability measure on eight-mode sectors. A signal on eight modes is normalised when the sum of squared complex norms equals one. The sector measure of a mode set $S$ is the sum of those squared norms over $S$; on the full universe it recovers the normalisation constant, and is the candidate Born probability for that sector.
The DFT-8 is the unitary discrete Fourier transform $F(f)(k)=8^{-1/2}\sum_j f(j)\bar\zeta^{kj}$. Upstream, the Parseval corollary equates total sector measure before and after DFT-8. The local setting depends on the complex-structure forcing layer (eight-mode signals, inner product, DFT-8, Parseval) and on two-outcome Born calibration, aiming to close the Born-rule gap linked to T5, T7, and T8.
proof idea
Normalisation is rewritten as total sector measure equal to one. The total measure of the transformed signal is replaced by the total measure of the original via the Parseval corollary that DFT-8 preserves total sector mass. The hypothesis that the original signal is normalised then finishes the goal. Term-mode, two steps: rewrite then exact.
why it matters
Feeds the frequency-domain sector forcing theorem, which asserts that normalisation, phase invariance, additivity, and two-branch calibration all hold for DFT modes of a normalised signal. That parent needs the transformed signal to remain normalised as its first conjunct. Within Recognition Science this supports Born-rule forcing on the eight-tick octave (T7), replacing trivial placeholders for measurement probabilities by the unique measure $\mu(S)=\sum_{k\in S}|\psi_k|^2$, with the same form in the frequency basis by Parseval.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.