normalization_from_jcost

Module QF-002 derives the Born rule $P=|\psi|^2$ as the unique probability on 8-mode sectors that is normalised, phase-invariant, additive on disjoint mode-sets, and calibrated by the two-branch $\exp(-C)$ Gibbs weight. The DFT-8 splits any ledger state into eight orthogonal modes; probability is forced to depend only on moduli.

A signal $\psi:\mathrm{Fin},8\to\mathbb{C}$ is normalised when $\sum_k|\psi_k|^2=1$. The sector measure of a mode-set $S$ is $\mu_\psi(S)=\sum_{k\in S}|\psi_k|^2$, the candidate Born probability of that sector. Upstream, sectorMeasure_total already records that normalisation is exactly $\mu_\psi$ of the universe equalling 1. Related cost-side IsNormalized predicates ($F(1)=0$) appear in the J-cost functional equation and d'Alembert inevitability, but here the signal-level normalisation is the operative hypothesis.

One-line term wrapper: apply sectorMeasure_total to $\psi$ and the normalisation hypothesis $h$. That upstream theorem is definitionally the same statement (sectorMeasure ψ Finset.univ = 1 unfolds to the sum-of-squares condition), so the goal closes by direct application with no further rewriting.

This is the normalisation half of the RS Born-rule package in Quantum.BornRule. The module claims uniqueness of the sector measure under phase invariance, Finset additivity, and two-branch $\exp(-C)$ calibration to $r\mapsto r^2$; without total mass 1 the measure is not a probability. It sits beside siblings such as born_rule_from_jcost, born_rule_phase_independent, and gleason_from_rs, and rests on the forcing developed in Foundation.BornRuleForcing (and ultimately the eight-tick octave T7). No downstream dependents are recorded yet; the declaration is the thin Quantum-layer re-export of the total-measure fact under the J-cost narrative of the doc-comment.