sectorMeasure_disjoint_union
plain-language theorem explainer
Sector measure is additive on disjoint mode-sets of an 8-mode signal: μ(S ∪ T) = μ(S) + μ(T) whenever S ∩ T = ∅. Anyone assembling the DFT-8 Born-rule uniqueness argument cites this as the additivity axiom. The proof is a one-line appeal to Finset sum-union.
Claim. Let $\psi$ be an 8-mode complex signal and let $S,T \subseteq \{0,\ldots,7\}$ be finite mode-sets with $S \cap T = \emptyset$. Then $\mu_\psi(S \cup T) = \mu_\psi(S) + \mu_\psi(T)$, where $\mu_\psi(U) := \sum_{k \in U} \|\psi_k\|^2$.
background
The module forces the Born rule on the eight-tick mode lattice: the unique probability on mode-sets 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.
The sector measure is defined pointwise as that sum of squared norms over the chosen modes. Signal8 is the 8-component complex amplitude space coming from ComplexStructureForcing (inner product, DFT-8, Parseval, phase rotation). The eight-mode index is the T7 octave $2^3$.
Additivity is one of the four characterizing axioms listed in the module theorem. Sibling facts already record non-negativity, the bound $\mu \le 1$, singleton evaluation, total mass on the universe, and phase invariance.
proof idea
One-line term proof. Unfolding the definition, both sides are finite sums of $|\psi_k|^2$ over mode indices. The hypothesis Disjoint S T is exactly the side condition of Finset.sum_union, which rewrites the sum over the union as the sum of the two separate sums. No further algebraic work is required.
why it matters
This is the additivity leg of the DFT-8 sector forcing package. Downstream, dft8_sector_forcing packages normalisation, phase invariance, disjoint additivity, and two-branch calibration into one conjunction; the frequency-domain twin dft8_sector_forcing_freq does the same after DFT-8. The immediate corollary sectorMeasure_compl obtains $\mu(S) + \mu(S^c) = \mu(\mathrm{univ})$ by applying this lemma to $S$ and its complement.
In the Recognition chain the result sits under T7 (eight-tick octave) and the measurement mechanism (F-009): it closes the former Born-rule gap that had been stubbed by trivial placeholders. Without disjoint additivity the uniqueness claim for $\mu(S) = \sum |\psi_k|^2$ does not go through.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.