probabilities_normalized
plain-language theorem explainer
Normalization of two-outcome probabilities follows from the exponential weights on recognition costs. A physicist deriving the Born rule from the J-cost would cite this to confirm the probabilities form a valid distribution before equating them to squared amplitudes. The tactic proof unfolds the definitions, verifies the common denominator is nonzero via positivity of exp, rewrites the sum as a single fraction, and concludes with the division identity.
Claim. For a two-outcome measurement with recognition costs $C_1, C_2 : ℝ$ where $C_1, C_2 ≥ 0$, let $p_1 = e^{-C_1}/(e^{-C_1} + e^{-C_2})$ and $p_2 = e^{-C_2}/(e^{-C_1} + e^{-C_2})$. Then $p_1 + p_2 = 1$.
background
The module derives Born's rule $P(I) = |α_I|^2$ from the recognition cost functional J and the amplitude bridge $𝒜 = exp(-C/2)·exp(iφ). A TwoOutcomeMeasurement is the structure carrying two non-negative recognition costs C₁ and C₂ for the two outcomes; the probabilities are the normalized exponentials of the negative costs. Upstream results include the amplitude definitions in SMatrixUnitarity (S-matrix element for transition i to j) and DoubleSlit (sum of complex path amplitudes), which supply the quantum side of the correspondence.
proof idea
The proof unfolds prob₁ and prob₂ to their explicit forms. It establishes the denominator is nonzero because both Real.exp(-C_i) are positive. It rewrites the sum of the two fractions as a single fraction via add_div, then applies div_self on the nonzero denominator.
why it matters
This theorem supplies the normalization step required for the Born-rule derivation in Measurement.BornRule. It ensures the recognition-cost weights define a probability measure before any link to |amplitude|² is made. The result is a prerequisite for any downstream claim that equates the normalized exponentials to squared quantum amplitudes.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.