born_weight_forced
plain-language theorem explainer
Any real weight calibrated on angles by the two-branch Born rule, w(cos θ)=cos²θ for θ∈(0,π/2), must equal r² on the open unit interval. Cited by anyone deriving Gleason-type uniqueness of the DFT-8 sector measure from RS axioms. Proof is a short arccos reduction: set θ=arccos r and apply the calibration hypothesis.
Claim. Let $w:\mathbb{R}\to\mathbb{R}$ satisfy $w(\cos\theta)=(\cos\theta)^2$ for every $\theta\in(0,\pi/2)$. Then $w(r)=r^2$ for all $r\in(0,1)$.
background
The module forces the Born rule from the DFT-8 sector measure. The target uniqueness theorem states that the only probability measure on 8-mode sectors that is normalised on unit states, phase-invariant (depends only on moduli), additive on disjoint mode sets, and consistent with the two-branch exp(−C) calibration is μ(S)=Σ_{k∈S}‖ψ_k‖² (equivalently, by Parseval, the same sum in the DFT-8 frequency basis).
Two-branch calibration is imported from the two-outcome Born certificate (P_cos_eq / P_sin_eq): on a pure cosine or sine branch the Gibbs weight collapses to cos²θ or sin²θ. Complex-structure forcing supplies Signal8, the inner product, dft8, and phase invariance. The present lemma is the scalar core of that story: once a weight agrees with cos² on the open first quadrant of angles, it is forced to be the square map on (0,1).
proof idea
Fix r∈(0,1). Let θ:=arccos r. The standard identity cos(arccos r)=r holds because 0<r≤1. Positivity of θ and the bound θ<π/2 are read off the definition arccos r=π/2−arcsin r together with the elementary facts arcsin r>0 (since r>0) and arcsin r<π/2 (since r<1). Rewrite w(r)=w(cos θ), apply the calibration hypothesis at this θ, then substitute cos θ=r to obtain w(r)=r². The argument is pure real analysis; no sector or DFT structure is used.
why it matters
Direct parent is gleason_from_rs in Quantum.BornRule, whose doc-comment records a Gleason-style uniqueness claim: the sector measure is the unique probability assignment forced by RS axioms (phase invariance, additivity, two-branch exp(−C) calibration), and "the weight function is forced to be r↦r²". That theorem is literally a one-line application of the present result.
In the module registry this closes the Born-rule gap (replacing trivial True placeholders) and sits on the chain T5 (J-uniqueness), T7 (eight-tick octave), T8 (D=3), and F-009 (measurement mechanism). It is the scalar hinge of the DFT-8 sector forcing theorem stated later in the same file: once the weight is r², the unique measure satisfying the four axioms is Σ‖ψ_k‖².
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.