sectorMeasure_compl
plain-language theorem explainer
On any 8-mode signal, the sector measure of a mode set plus the measure of its complement equals the total measure of all eight modes. Anyone deriving Born-rule probabilities on DFT-8 sectors cites this as the elementary complement identity. The proof is a one-line rewrite through disjoint-union additivity and the finset identity S ∪ Sᶜ = univ.
Claim. For every 8-mode signal $\psi$ and every finite mode set $S \subseteq \{0,\ldots,7\}$, if $\mu_\psi(S) := \sum_{k \in S} \|\psi_k\|^2$, then $\mu_\psi(S) + \mu_\psi(S^c) = \mu_\psi(\{0,\ldots,7\})$.
background
The module forces the Born rule on the eight-tick (DFT-8) mode lattice: the unique probability on mode sectors that is normalised, phase-invariant, additive on disjoint sets, and consistent with the two-branch exp(−C) calibration is $\mu(S) = \sum_{k \in S} |\psi_k|^2$. Signals live in Signal8 (complex 8-vectors) from the complex-structure forcing layer; the eight modes are the T7 octave.
The sector measure is defined pointwise as that sum of squared norms. Upstream, additivity is already proved: for disjoint mode sets $S,T$, $\mu(S \cup T) = \mu(S) + \mu(T)$, by ordinary finset sum-union. The present identity is the special case $T = S^c$, which is always disjoint from $S$ and whose union is the full mode universe.
proof idea
Rewrite the left-hand side via the disjoint-union theorem applied to $S$ and $S^c$ with the standard fact disjoint_compl_right. The resulting union $S \cup S^c$ is definitionally the universe of Fin 8, so Finset.union_compl finishes the equality with $\mu(\mathrm{univ})$. Pure algebraic rewrite; no analysis or DFT is used.
why it matters
This is a bookkeeping lemma inside Born-rule forcing: once total mass on the universe is fixed (normalisation / Parseval), complement additivity lets one read off the probability of the complementary sector without a second sum. It sits with the other elementary measure facts (nonnegativity, $\le 1$, singleton, total mass, phase invariance) that pin $\mu$ as the unique candidate before the two-outcome Born calibration is imposed.
Framework landmarks: T7 (eight-tick octave) supplies the mode set Fin 8; the module also depends on T5 and the measurement mechanism F-009. No downstream consumers are recorded yet; the identity is infrastructure for later uniqueness and Parseval corollaries in the same file. It closes part of the former Born-rule gap (trivial placeholders) by making sector probabilities a genuine finitely additive measure on the power set of modes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.