sectorMeasure_le_one
plain-language theorem explainer
For any normalized 8-mode signal, the Born-rule sector measure of an arbitrary mode subset is at most 1. Anyone treating that measure as a probability mass needs this bound. The proof is a short calc: the partial sum is dominated by the full sum over all eight modes, which equals 1 by normalization.
Claim. Let $\psi$ be an 8-mode complex signal with $\sum_{k=0}^{7}\|\psi_k\|^2=1$. For every finite mode set $S\subseteq\{0,\ldots,7\}$, the sector measure $\mu_\psi(S):=\sum_{k\in S}\|\psi_k\|^2$ satisfies $\mu_\psi(S)\le 1$.
background
The module forces the Born rule on the DFT-8 mode lattice that Recognition Science inherits from the eight-tick octave (T7) and $D=3$ (T8). A Signal8 is a map from Fin 8 into $\mathbb{C}$. Normalization means the $\ell^2$ mass of all eight mode amplitudes equals one: $\sum_k|\psi_k|^2=1$.
The sector measure of a mode set $S$ is the partial sum $\mu_\psi(S)=\sum_{k\in S}|\psi_k|^2$. The module theorem states that the unique measure on 8-mode sectors that is normalized, phase-invariant, additive on disjoint sets, and consistent with the two-branch $\exp(-C)$ calibration is exactly this sum (equivalently, by Parseval, the same sum in the DFT-8 frequency basis).
Nonnegativity of each squared norm is elementary analysis; the sibling sectorMeasure_nonneg records it. The present bound is the complementary upper estimate needed before one can call $\mu_\psi$ a probability.
proof idea
A three-line calc. First apply Finset.sum_le_sum_of_subset_of_nonneg to the inclusion $S\subseteq\mathrm{univ}$, using $t\mapsto t^2\ge 0$ on each term, to get $\mu_\psi(S)\le\mu_\psi(\mathrm{univ})$. Second, rewrite the full sum as $1$ by the normalization hypothesis. No other lemmas are required.
why it matters
This is a basic sanity check inside Born-rule forcing: without $\mu_\psi(S)\le 1$, the candidate sector measure cannot be a probability. The module doc frames the parent result as closing the Born-rule gap (replacing trivial placeholders) and depending on T5 (J-uniqueness), T7 (eight-tick octave), T8 ($D=3$), and the measurement mechanism F-009, together with two-outcome calibration from TwoOutcomeBornCert.
Together with nonnegativity, the singleton evaluation, the total-mass identity, and phase invariance of the sector measure, the bound lets later uniqueness arguments treat $\mu_\psi$ as a genuine probability on mode sectors. No downstream consumers are wired yet in the graph; the lemma is infrastructure for that uniqueness package rather than an end-user theorem.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.