dft_sector_total_eq
plain-language theorem explainer
The total Born-sector mass of an 8-mode signal is unchanged by the unitary DFT-8: summing ‖ψ_k‖² over all eight modes equals the same sum on Fψ. Anyone proving that frequency-basis normalisation follows from time-basis normalisation cites this Parseval corollary. The proof rewrites both totals as complex inner products and applies DFT-8 norm preservation.
Claim. For every 8-mode complex signal $\psi$, if $\mu(\psi,S)=\sum_{k\in S}\|\psi_k\|^2$ is the sector measure and $F$ is the unitary DFT-8, then $\mu(F\psi,\{0,\ldots,7\})=\mu(\psi,\{0,\ldots,7\})$.
background
The module forces the Born rule on eight-tick modes: the unique probability on mode sectors that is normalised, phase-invariant, additive on disjoint sets, and matched to the two-branch exp(−C) calibration is $\mu(S)=\sum_{k\in S}|\psi_k|^2$. By Parseval the same formula holds in the DFT-8 frequency basis.
A Signal8 is a map Fin 8 → ℂ. The sector measure is exactly that sum of squared moduli. The DFT-8 is $F(f)(k)=(1/\sqrt{8})\sum_j f(j),\overline{\zeta}^{kj}$. Upstream, dft8_preserves_norm states the complex inner-product identity $\langle Ff,Ff\rangle=\langle f,f\rangle$, and inner8_self_eq expands $\langle f,f\rangle$ to $\sum_k|f_k|^2$ (as a complex of a real). The real identity $\mathrm{normSq},z=|z|^2$ bridges the two presentations of the squared modulus.
Local setting depends on T5 (J-cost), T7 (eight-tick octave), and T8 ($D=3$), plus the complex-structure forcing that supplies DFT-8 and Parseval.
proof idea
Unfold sectorMeasure and replace each $|\cdot|^2$ by Complex.normSq via normSq_eq_norm_sq. Invoke dft8_preserves_norm ψ, which equates the complex inner products $\langle F\psi,F\psi\rangle=\langle\psi,\psi\rangle$. Rewrite both sides with inner8_self_eq so each inner product becomes a sum of normSq values. The resulting real equality is the claimed total-sector identity; finish by exact_mod_cast.
why it matters
This is the Parseval bridge that lets the Born sector measure be written indifferently in the time or frequency basis of the eight-tick octave (T7). Downstream, isNormalized_dft8 is a one-line rewrite: if $\mu(\psi,\mathrm{univ})=1$ then $\mu(F\psi,\mathrm{univ})=1$, so DFT-8 preserves the normalisation predicate used throughout Born-rule forcing.
Without total-mass preservation, frequency-sector probabilities would not automatically sum to one on normalised states, breaking the uniqueness claim that $\mu(S)=\sum_{k\in S}|\psi_k|^2$ is the only measure satisfying the four axioms (normalisation, phase invariance, additivity, two-branch calibration). The module registry marks this chain as closing the Born-rule gap that previously held trivial placeholders. Framework landmarks: T7 eight-tick structure, DFT-8 from complex-structure forcing, and the measurement mechanism (F-009) that needs a basis-independent probability.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.