exp_sum_ne_zero
plain-language theorem explainer
For any real recognition costs C₁ and C₂, exp(-C₁)+exp(-C₂) is nonzero. Cited by anyone discharging the denominator in two-outcome recognition-weighted probabilities. Proof is a one-line extraction of nonzeroness from the strict positivity of that sum.
Claim. For all real numbers $C_1,C_2$, $e^{-C_1}+e^{-C_2}\neq 0$.
background
The module certifies that recognition-weighted two-outcome probabilities are properly normalized: any pair of real costs $C_1,C_2$ yields probabilities that sum to one. The model uses the softmax-style weights $e^{-C}/(e^{-C_1}+e^{-C_2})$, so the common denominator must be nonzero before one can invoke $x/x=1$.
Upstream, the sibling positivity lemma states that $0<e^{-C_1}+e^{-C_2}$ for all real costs, proved by adding Mathlib's exp_pos twice. Strict positivity immediately implies the sum cannot vanish. The certificate is pure real analysis: no Recognition-Science physical hypotheses enter.
proof idea
One-line term proof. Apply the nonzeroness projection (.ne') to the upstream positivity lemma that $0<e^{-C_1}+e^{-C_2}$. No further rewriting or case splits.
why it matters
Feeds the core normalization theorem in the same module: after unfolding the cost-to-probability map and rewriting the sum of fractions as a single fraction, that theorem finishes by div_self on this nonzero denominator. Without it, the algebraic identity
$e^{-C_1}/(e^{-C_1}+e^{-C_2})+e^{-C_2}/(e^{-C_1}+e^{-C_2})=1$
cannot be discharged in Lean.
In the broader Recognition framework this is the elementary gate ensuring the two-outcome measurement model is a genuine probability distribution (conservation, completeness, consistency). The module stresses non-circularity: only positivity of exp and field arithmetic, so the certificate sits under any later Born-rule or measurement claims that import it.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.