sectorMeasure_total
plain-language theorem explainer
On a normalised 8-mode signal, the sector measure of the full mode set equals 1. Anyone citing DFT-8 Born-rule forcing or the quantum normalisation-from-J-cost result needs this identity. The proof is a one-line term: the normalisation hypothesis is definitionally the same statement as total sector mass one.
Claim. If $\psi$ is an $8$-mode complex signal with $\sum_{k=0}^{7}\|\psi_k\|^2 = 1$, then the sector measure of the full mode set equals one: $\mu_\psi(\{0,\ldots,7\}) = \sum_{k=0}^{7}\|\psi_k\|^2 = 1$.
background
The module forces the Born rule on eight-mode signals from the Recognition Science eight-tick structure (T7). A Signal8 assigns a complex amplitude to each of eight modes. The sector measure of a mode set $S$ is $\sum_{k\in S}|\psi_k|^2$; it is the candidate Born probability for that sector.
Normalisation means the sum of squared norms over all eight modes equals 1. By definition that is exactly the sector measure of the full universe of modes. The module theorem asserts that the unique probability measure on 8-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$.
proof idea
One-line term proof: the goal is definitionally identical to the hypothesis. By definition, the sector measure on Finset.univ expands to $\sum_{k:\mathrm{Fin},8}|\psi_k|^2$, and the normalisation predicate is precisely that sum equaling 1. No lemmas are applied; the proof term is the hypothesis itself.
why it matters
This is the normalisation clause in the DFT-8 sector forcing package. Downstream, dft8_sector_forcing packages it with phase invariance, disjoint additivity, and two-branch calibration into the uniqueness statement for the Born measure. Quantum.BornRule.normalization_from_jcost is a thin wrapper that re-exports the same fact under a J-cost conservation reading: "Normalisation follows from J-cost conservation: the total sector measure of a normalised state is 1."
In the Recognition framework this closes the Born-rule gap noted in the module registry (replacing trivial placeholders). It depends on T5 (J-uniqueness), T7 (eight-tick octave), and T8 ($D=3$), and supplies the total-mass half of the claim that $\mu$ is a probability measure on the eight DFT modes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.