sectorMeasure_singleton
plain-language theorem explainer
On an 8-mode complex signal, the sector measure of a singleton mode set equals the squared modulus of that mode's amplitude. Anyone matching sector probabilities to two-branch cos²/sin² Born weights cites this reduction. The proof is a one-line simp that unfolds the finite-sum definition of the measure.
Claim. For any 8-mode signal $\psi$ and any mode index $k \in \{0,\ldots,7\}$, the sector measure of the singleton $\{k\}$ equals $\|\psi_k\|^2$.
background
The module forces the Born rule on DFT-8 sectors: the unique probability on mode sets 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 the eight-tick complex structure (Signal8) from ComplexStructureForcing; the eight modes are the T7 octave.
The sector measure is defined by summing squared moduli over a Finset of modes. On a singleton the sum collapses to one term. Downstream, two-branch rotations embed a cos/sin pair into modes 0 and 1, so singleton evaluation is the bridge from the abstract measure to the calibrated amplitudes $P_{\cos}$ and $P_{\sin}$.
proof idea
One-line wrapper: simp [sectorMeasure] unfolds the definition
$\mathrm{sectorMeasure}(\psi,S)=\sum_{k\in S}|\psi_k|^2$
and reduces the sum over ${k}$ to the single summand $|\psi_k|^2$. No further lemmas are required.
why it matters
This is the atomic evaluation step for the forced Born measure. It is applied directly by sector_matches_cos_branch (mode 0 equals complement amplitude squared) and sector_matches_sin_branch (mode 1 equals initial amplitude squared), which pin the two-branch calibration from TwoOutcomeBornCert onto the sector measure.
In the Recognition chain the result sits under T7 (eight-tick octave) and the measurement mechanism (F-009): once singletons match $|\psi_k|^2$, additivity and Parseval extend the same law to arbitrary sectors and to the DFT-8 frequency basis. The module registry marks this path as closing the Born-rule gap that previously held only trivial placeholders.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.