sectorMeasure_nonneg
plain-language theorem explainer
The DFT-8 sector measure is nonnegative for every eight-mode signal and every mode set: summing squared mode amplitudes cannot go negative. Anyone building the forced Born probability on 8-tick sectors cites this as the first positivity axiom. The proof is a one-line appeal to nonnegativity of finite sums of squares.
Claim. For every eight-mode complex signal $\psi$ and every finite set $S\subseteq\{0,\ldots,7\}$ of modes, the sector measure satisfies $0\le\mu_\psi(S)$, where $\mu_\psi(S)=\sum_{k\in S}\|\psi_k\|^2$.
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 calibrated to the two-branch $\exp(-C)$ rule is $\mu(S)=\sum_{k\in S}|\psi_k|^2$ (equivalently the same sum on DFT coefficients by Parseval).
A Signal8 is an eight-component complex amplitude vector on the T7 octave. The sector measure is defined exactly as that sum of squared norms over a Finset of modes in Fin 8. Nonnegativity is the first structural property any candidate probability must satisfy before normalisation, phase invariance, and two-outcome calibration are imposed.
Upstream, the definition of the sector measure is pure summation of $|\psi k|^2$; the surrounding development draws on complex structure forcing (inner product, DFT-8, Parseval) and the two-outcome Born certificate.
proof idea
Term-mode one-liner. Apply Finset.sum_nonneg to the sum defining the sector measure; each summand is a square of a real norm, hence nonnegative by sq_nonneg. No case split on the mode set and no appeal to Parseval or phase structure is required.
why it matters
Positivity is the opening axiom in the Born-rule forcing chain of this module: without $0\le\mu(S)$ one cannot promote the sector sum to a probability, nor match the two-branch $\exp(-C)$ calibration. The module doc states that the unique measure meeting normalisation, phase invariance, additivity, and two-outcome consistency is exactly this sum; the present lemma discharges the nonnegativity half of that package.
It sits on the T7 eight-tick octave and the complex structure forced earlier, and helps close the Born-rule gap flagged in the registry (replacing trivial placeholders). Sibling lemmas (sectorMeasure_le_one, sectorMeasure_total, phase invariance) complete the probability axioms; together they feed the uniqueness claim for $\mu(S)=\sum|\psi_k|^2$. No downstream dependents are recorded yet, but the lemma is load-bearing inside the local forcing argument.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.