prob_normalization
plain-language theorem explainer
Two-outcome probabilities built from recognition costs always sum to one: the softmax weights of exp(-C₁) and exp(-C₂) form a partition of unity. Anyone checking the Born-rule-light measurement model or the probability-normalization certificate cites this. The proof is a short real-analysis reduction: unfold the weights, combine over a common denominator, and cancel using positivity of the exponential sum.
Claim. For any real recognition costs $C_1,C_2$, the normalized two-outcome weights sum to one: $\frac{e^{-C_1}}{e^{-C_1}+e^{-C_2}}+\frac{e^{-C_2}}{e^{-C_1}+e^{-C_2}}=1$.
background
The module certifies that recognition-weighted two-outcome probabilities are a genuine probability distribution. A recognition cost is any real number $C$; the associated unnormalized weight is $e^{-C}$. The two-outcome probability of cost $C_1$ relative to $C_2$ is the normalized weight
$$\mathrm{prob}(C_1\mid C_2)=\frac{e^{-C_1}}{e^{-C_1}+e^{-C_2}}.$$
The only analytic input is positivity of the real exponential: $e^x>0$ for all $x$, so the denominator sum is strictly positive and in particular nonzero (the local lemma exp_sum_ne_zero). No physical hypothesis enters; the identity is pure real arithmetic on Mathlib's Real.exp.
This sits under the light Born-rule measurement layer imported by the module, where measurement outcomes are scored by recognition cost and turned into probabilities by the same exponential weights.
proof idea
Unfold the definition of each probability to the explicit ratio of exponentials. Commute the two summands in the second denominator so both fractions share the ordered denominator $e^{-C_1}+e^{-C_2}$. Apply the common-denominator identity $a/d+b/d=(a+b)/d$, which collapses the left-hand side to $(e^{-C_1}+e^{-C_2})/(e^{-C_1}+e^{-C_2})$. Finish with div_self, justified by the local lemma that the exponential sum is nonzero (itself from strict positivity of each exponential).
why it matters
This is the core algebraic fact named in the module doc: recognition-cost probabilities conserve probability, leave no missing mass, and introduce no excess mass. It is the sole theorem field consumed by the structure ProbabilityNormalizationCert, which packages the certificate that the two-outcome measurement model is normalized.
In the broader Recognition Science stack it underwrites the light Born-rule measurement path: once outcomes are scored by recognition cost, the exponential map produces a valid probability simplex without extra postulates. The argument is deliberately non-circular (only exp_pos and field arithmetic), so later physical claims that quote normalized recognition probabilities rest on elementary analysis rather than on a hidden measurement axiom.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.