dft8_sector_forcing_freq
plain-language theorem explainer
For any unit-norm 8-mode signal, its DFT-8 transform carries a sector measure that is total-mass one, invariant under modewise phase rotations, and additive on disjoint frequency sets. Anyone citing the frequency-domain Born measure on the eight-tick lattice needs this packaging. The proof is a three-field term that reuses normalisation preservation, phase invariance, and disjoint-union additivity already proved for the time-domain sector measure.
Claim. Let $\psi$ be an $8$-mode complex signal with $\sum_{k=0}^{7}\|\psi_k\|^2=1$, and let $F\psi$ be its length-$8$ discrete Fourier transform. Then the sector measure $\mu_{F\psi}(S)=\sum_{k\in S}\|(F\psi)_k\|^2$ satisfies: (i) $\mu_{F\psi}(\{0,\ldots,7\})=1$; (ii) for every real phase assignment $\theta$, $\mu_{e^{i\theta}\cdot(F\psi)}(S)=\mu_{F\psi}(S)$; (iii) if $S,T$ are disjoint mode sets, $\mu_{F\psi}(S\cup T)=\mu_{F\psi}(S)+\mu_{F\psi}(T)$.
background
The module forces the Born rule on the eight-tick lattice: the unique probability on mode sectors that is normalised, phase-invariant, additive on disjoint sets, and calibrated to the two-branch $\exp(-C)$ rule is $\mu(S)=\sum_{k\in S}|\psi_k|^2$. By Parseval the same formula holds in the DFT-8 frequency basis.
A signal is normalised when the sum of squared mode norms equals one. The sector measure of a set $S$ is exactly that sum restricted to $S$. Phase rotation multiplies each mode by $e^{i\theta_k}$ and leaves every $|\psi_k|$ unchanged, so the measure is blind to arguments. The DFT-8 map (from ComplexStructureForcing) is unitary on this inner product, hence preserves total mass one.
Upstream, isNormalized_dft8 records that DFT-8 sends normalised signals to normalised signals; sectorMeasure_phase_invariant and sectorMeasure_disjoint_union already give phase invariance and Finset additivity for an arbitrary signal. This declaration simply specialises those three facts to the frequency-domain vector $F\psi$.
proof idea
Pure term-mode packaging. The triple is assembled as:
- first conjunct: apply
isNormalized_dft8to $\psi$ and the normalisation hypothesis (which rewrites total sector mass of $F\psi$ to one via the DFT Parseval identity already used there); - second conjunct: for each phase map $\theta$, invoke
sectorMeasure_phase_invarianton $F\psi$; - third conjunct: for each disjoint $T$, invoke
sectorMeasure_disjoint_unionon $F\psi$. No new algebra is performed; the frequency-domain claim is the time-domain trio evaluated atdft8 ψ.
why it matters
Closes the frequency half of the Born-rule forcing statement in this module: once the unique sector measure is identified as $\sum|\psi_k|^2$ in the time basis, Parseval plus this lemma give the identical measure on DFT modes, $\sum|(F\psi)_k|^2$. The module registry ties the result to T5 (J-cost uniqueness), T7 (eight-tick octave), T8 ($D=3$), and the measurement mechanism F-009; the eight-mode lattice is exactly the $2^3$ tick structure forced upstream.
No downstream consumers are wired yet (used_by is empty), so the lemma presently stands as the frequency-domain interface for any later uniqueness or certification theorem that must quote the three Born axioms on DFT sectors rather than on the original signal. It replaces the former trivial placeholders that left the Born-rule gap open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.