prob_nonneg
plain-language theorem explainer
For any real recognition costs, the two-outcome cost-to-probability weight is nonnegative. Cited by the probability-normalization certificate and by parallel nonnegativity lemmas in the delta-probability, quantum-ledger, and Boltzmann layers. Proof unfolds the weight as a quotient and applies nonnegativity of division once both the numerator exponential and the exponential sum are known positive.
Claim. For all real recognition costs $C_1,C_2$, the two-outcome recognition weight $p(C_1,C_2)=\frac{e^{-C_1}}{e^{-C_1}+e^{-C_2}}$ satisfies $0\le p(C_1,C_2)$.
background
The Probability Normalization Certificate module records a pure algebraic fact: recognition-weighted two-outcome probabilities built from real costs are a valid distribution. The weight for the first outcome is the softmax-style map sending $(C_1,C_2)$ to $e^{-C_1}/(e^{-C_1}+e^{-C_2})$. The module stresses that only positivity of the real exponential, division algebra, and $x/x=1$ for $x\neq 0$ are used; no physical hypotheses enter.
The immediate upstream lemma is positivity of the denominator sum: $e^{-C_1}+e^{-C_2}>0$ for all real costs, obtained by adding two instances of Mathlib's exp_pos. Parallel nonnegativity statements appear elsewhere in the stack (finite distinction counting probabilities, Born-rule squared norms on the quantum ledger, and Boltzmann factors), each with its own construction but the same role: every named probability channel must land in $[0,1]$ before normalization is certified.
proof idea
Short tactic proof. Unfold the cost-to-probability definition to expose the quotient $e^{-C_1}/(e^{-C_1}+e^{-C_2})$. Apply the standard nonnegativity-of-division lemma. The numerator goal is discharged by nonnegativity of a positive exponential (exp_pos). The denominator goal is discharged by nonnegativity of the already-proved strict positivity of the exponential sum. No case splits and no analysis beyond Mathlib exponential positivity.
why it matters
This lemma is one of the three elementary pillars of the normalization certificate (nonnegativity, upper bound one, and exact sum-to-one). It is consumed directly by the ProbabilityNormalizationCert structure that packages the verification predicate for recognition-weighted probabilities. Downstream, the same nonnegativity obligation appears in the delta-probability headline (every finite distinction event has probability in $[0,1]$), in the quantum-ledger Born channel, and in the Boltzmann distribution layer; those siblings are independent constructions, but this certificate is the pure two-cost algebraic core the measurement model relies on.
In the broader Recognition Science stack the result underwrites the two-outcome measurement model used wherever recognition costs feed probabilities (Born-rule light, ledger readouts). It is deliberately non-circular: elementary real analysis only, so it does not borrow from the forcing chain (T5–T8), the Recognition Composition Law, or the phi-ladder mass formula.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.