exp_sum_pos
plain-language theorem explainer
For any real recognition costs, the sum of the two Boltzmann weights exp(-C₁) and exp(-C₂) is strictly positive. Anyone citing the two-outcome probability normalization certificate needs this positivity gate. The proof is a one-line term application of Mathlib's exp positivity and sum-of-positives.
Claim. For all real numbers $C_1, C_2$, one has $0 < e^{-C_1} + e^{-C_2}$.
background
The module certifies that recognition-weighted two-outcome probabilities are a genuine probability distribution: for costs $C_1, C_2 \in \mathbb{R}$, the weights $e^{-C_i}$ yield
$$\frac{e^{-C_1}}{e^{-C_1}+e^{-C_2}} + \frac{e^{-C_2}}{e^{-C_1}+e^{-C_2}} = 1.$$
That identity needs a strictly positive denominator. The only analytic ingredients are Mathlib's exp_pos ($e^x > 0$ for every real $x$) and the elementary fact that the sum of two positive reals is positive. No physical hypothesis enters; the module doc stresses this is pure real analysis.
Sibling definitions package the normalized weight as prob_from_cost, the two-outcome Born-style map used throughout the measurement layer imported from BornRuleLight.
proof idea
Term-mode one-liner. Apply Mathlib's sum-of-positives lemma to the pair exp_pos (-C₁) and exp_pos (-C₂). Each exponential is strictly positive, so their sum is strictly positive. No case splits, no rewriting.
why it matters
This is the positivity hinge for the whole Probability Normalization Certificate. Three immediate clients depend on it:
exp_sum_ne_zero: upgrades strict positivity to a nonzero denominator so division is legal.prob_nonneg: feeds the positive denominator intodiv_nonnegto get $0 \le$ probability.prob_le_one: rewrites the bound viadiv_le_oneat this positive sum, then uses nonnegativity of the complementary exponential.
Together those lemmas discharge the key theorem that two recognition costs produce probabilities summing to 1, the algebraic backbone of RS two-outcome measurement. The module frames this as non-circular: only exp positivity, division algebra, and self-division. It sits in the Verification domain as a certificate, not a physical derivation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.