dft8_sector_forcing
plain-language theorem explainer
On any normalised eight-mode signal, the sector measure μ(S)=Σ_{k∈S}‖ψ_k‖² simultaneously obeys total mass 1, phase invariance, disjoint additivity, and two-branch Gibbs calibration. Anyone deriving the Born rule from J-cost structure cites this packaging result. The proof is a term-mode four-way conjunction of the already-proved component lemmas.
Claim. For every normalised eight-mode signal $\psi$ ($\sum_k \|\psi_k\|^2=1$) and every mode set $S\subseteq\{0,\ldots,7\}$, the sector measure $\mu_\psi(S)=\sum_{k\in S}\|\psi_k\|^2$ satisfies: (i) $\mu_\psi(\{0,\ldots,7\})=1$; (ii) $\mu$ is unchanged under pointwise phase rotations $\psi_k\mapsto e^{i\theta_k}\psi_k$; (iii) $\mu_\psi(S\cup T)=\mu_\psi(S)+\mu_\psi(T)$ whenever $S$ and $T$ are disjoint; (iv) on every two-branch rotation signal, $\mu(\{0\})=P_{\cos}$ and $\mu(\{1\})=P_{\sin}$.
background
The module forces the Born rule from the DFT-8 sector measure on eight-mode complex signals. A signal $\psi$ is normalised when $\sum_{k:0\ldots7}|\psi_k|^2=1$. The sector measure assigns to each mode set $S$ the sum of squared norms over modes in $S$; that sum is the candidate Born probability of the sector.
Pointwise phase rotation multiplies each mode by $e^{i\theta_k}$. The two-branch calibration lemma states that on every two-branch rotation signal the sector measure on ${0}$ and ${1}$ recovers the Gibbs probabilities $P_{\cos}$ and $P_{\sin}$ already certified by the two-outcome Born certificate (exp$(-C)$ structure).
The module depends on complex-structure forcing (Signal8, inner product, DFT-8, Parseval, phase invariance) and on the two-outcome Born certificate. The uniqueness claim in the module header is: the unique probability measure on 8-mode sectors that is normalised, phase-invariant, additive on disjoint sets, and consistent with two-branch exp$(-C)$ is exactly $\mu(S)=\sum_{k\in S}|\psi_k|^2$.
proof idea
Term-mode proof: a single 4-tuple constructor. First component is total-mass normalisation of the sector measure on a normalised signal. Second is the phase-invariance lemma applied to the given phase map and sector. Third is disjoint-union additivity of the sector measure. Fourth is the two-branch calibration theorem, which rewrites the sector values on a two-branch rotation signal into $P_{\cos}$ and $P_{\sin}$ via the cos/sin branch matching lemmas and the two-outcome certificate equalities. No new algebra is done here; the declaration only packages the four properties.
why it matters
This is the packaging step that the quantum Born-rule theorem consumes. Downstream, born_rule_from_jcost states that on any normalised Signal8 the sector measure is the unique probability assignment satisfying normalisation, phase invariance, additivity, and two-branch calibration; its proof body is essentially this conjunction.
In the Recognition framework the result closes the Born-rule gap that previously held trivial placeholders. It sits on T5 (J-uniqueness of the cost), T7 (eight-tick octave, hence the 8-mode lattice), and T8 ($D=3$), together with the measurement-mechanism registry item. By Parseval the same measure in the DFT-8 frequency basis equals $\sum_{k\in S}|(F\psi)_k|^2$, so the forcing is basis-independent between time and frequency sectors.
Anyone tracing how the Born rule is forced from J-cost structure, rather than postulated, lands on this declaration as the concrete four-axiom certificate for $\mu(S)=\sum|\psi_k|^2$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.