born_rule_normalized
plain-language theorem explainer
The theorem shows that if recognition-cost probabilities for a two-outcome measurement equal the squared moduli of the amplitudes, then those moduli sum to one. Quantum measurement modelers and Recognition Science developers cite it to close the normalization step after introducing the amplitude bridge from J-cost. The proof is a direct algebraic cancellation: substitute the hypotheses, combine the fractions over the common denominator, and apply division by a nonzero quantity.
Claim. Let $C_1, C_2$ be real numbers and let $α_1, α_2$ be complex numbers. If $e^{-C_1}/(e^{-C_1}+e^{-C_2})=‖α_1‖^2$ and $e^{-C_2}/(e^{-C_1}+e^{-C_2})=‖α_2‖^2$, then $‖α_1‖^2 + ‖α_2‖^2 = 1$.
background
The module derives Born's rule P(I) = |α_I|² from the recognition cost functional J and the amplitude bridge 𝒜 = exp(-C/2)·exp(iφ). Recognition cost J supplies the real damping that converts path weights into probabilities via the exponential map; the bridge then identifies those weights with squared moduli. Upstream results supply parallel normalization statements: the light version in BornRuleLight, the path-sum version in Modal.Actualization that uses Z as total weight, and the quantum-state version in WavefunctionCollapse that invokes normalization of the state vector.
proof idea
Tactic-mode calculation. First a positivity lemma shows the common denominator is nonzero. The hypotheses are substituted into the target sum, the two fractions are added via the add_div identity, and the resulting expression simplifies to the denominator over itself, which equals 1 by div_self.
why it matters
The result supplies the final normalization step in the recognition-cost derivation of the Born rule and is invoked by the corresponding statements in BornRuleLight, Modal.Actualization, and WavefunctionCollapse. It confirms consistency between the J-cost functional and the requirement that probabilities sum to unity, supporting the framework's passage from T5 J-uniqueness through the amplitude bridge to measurement. No scaffolding remains; the theorem is fully proved.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.