prob_le_one
plain-language theorem explainer
For any real recognition costs, the two-outcome weight exp(-C₁)/(exp(-C₁)+exp(-C₂)) is at most one. Anyone building or citing the probability-normalization certificate needs this bound. The proof unfolds the cost-to-probability map, reduces via positivity of the exponential sum, and finishes with nonnegativity of exp.
Claim. For all real costs $C_1,C_2$, the recognition-weighted probability $\frac{e^{-C_1}}{e^{-C_1}+e^{-C_2}}$ satisfies $\frac{e^{-C_1}}{e^{-C_1}+e^{-C_2}}\le 1$.
background
The module certifies that recognition-weighted two-outcome probabilities are a genuine probability distribution. Costs $C_1,C_2\in\mathbb{R}$ are mapped to a softmax-style weight
$$\mathrm{prob_from_cost}(C_1,C_2)=\frac{e^{-C_1}}{e^{-C_1}+e^{-C_2}}.$$
The companion lemma exp_sum_pos records that the denominator is strictly positive: $e^{-C_1}+e^{-C_2}>0$, which follows from Mathlib's exp_pos. That positivity licenses division inequalities and later self-division in the sum-to-one identity.
Locally this is pure real analysis: no ledger axioms, no forcing-chain steps, and no physical hypotheses. The same bound appears at the finite-distinction layer (counting measure over events), but here the object is the continuous cost-to-probability map used by the measurement model.
proof idea
Unfold the definition of the cost-to-probability map. Rewrite the goal with div_le_one, justified by exp_sum_pos C₁ C₂ (the denominator is positive). The resulting inequality $e^{-C_1}\le e^{-C_1}+e^{-C_2}$ is immediate from le_add_of_nonneg_right applied to (exp_pos _).le. Three short steps; no induction or case split.
why it matters
This bound is one of the three elementary facts assembled into ProbabilityNormalizationCert: nonnegativity, upper bound one, and exact sum-to-one. Downstream, the finite-layer headline delta_probability_headline packages the analogous $[0,1]$ sandwich for counting probabilities over distinction events, and the sibling prob_le_one at that layer cites the same normalization story.
In the Recognition framework the certificate guarantees that the two-outcome measurement model built from recognition costs is probabilistically complete and consistent (no missing or excess mass). It is deliberately non-circular: only positivity of exp and field arithmetic. It does not itself invoke the forcing chain (T5–T8), the RCL, or the mass ladder; it sits under the Born-rule-light measurement layer as algebraic hygiene.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.