sectorMeasure
plain-language theorem explainer
The sector measure of an eight-mode signal on a mode set is the sum of squared moduli over those modes, read as the Born-rule probability of the sector. Anyone proving uniqueness of the DFT-8 Born measure cites this as the candidate μ. The body is a direct finite sum of squared norms; no lemmas are needed.
Claim. For an eight-mode complex signal $\psi$ and a finite set $S \subseteq \{0,\ldots,7\}$ of modes, the sector measure is $\mu_\psi(S) := \sum_{k \in S} \|\psi_k\|^2$.
background
The module forces the Born rule from DFT-8 structure on eight-mode signals. A signal $\psi$ assigns a complex amplitude to each mode in $\mathrm{Fin},8$, matching the T7 eight-tick octave. The natural candidate for the probability of a mode sector $S$ is the sum of squared moduli over $S$.
Upstream infrastructure from ComplexStructureForcing supplies Signal8, the eight-mode inner product, DFT-8, Parseval, and phase rotation. TwoOutcomeBornCert supplies the two-branch $\exp(-C)$ calibration ($P_{\cos}$, $P_{\sin}$). The module theorem then asserts that this sector sum is the unique measure that is normalised on unit signals, phase-invariant, additive on disjoint mode sets, and consistent with that two-branch Born rule.
proof idea
Pure definition: the right-hand side is the Finset sum of squared Euclidean norms of the mode amplitudes. No lemmas or tactics are applied; the declaration simply names that sum.
why it matters
This is the measure whose uniqueness is the module's main result. Downstream, dft8_sector_forcing shows it simultaneously satisfies normalisation, phase invariance, disjoint additivity, and two-branch calibration; the frequency-domain twin dft8_sector_forcing_freq does the same after DFT-8. Parseval corollaries (dft_sector_total_eq, isNormalized_dft8) show total mass is preserved under the transform. Calibration lemmas equate singleton sectors on the two-branch signal to $\cos^2\theta$ / $\sin^2\theta$ and thence to the Gibbs probabilities from TwoOutcomeBornCert.
In the registry it closes the Born-rule gap (replacing trivial placeholders) and sits on T5, T7, T8, and the measurement mechanism F-009: the unique sector probability forced by the eight-mode DFT structure is $\mu(S)=\sum_{k\in S}|\psi_k|^2$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.