prob_from_cost
plain-language theorem explainer
Maps a pair of real recognition costs to the two-outcome probability of the first cost via a normalized Boltzmann weight. Measurement and Born-rule verifiers in Recognition Science cite this as the elementary cost-to-probability map. It is a direct noncomputable definition: exp of minus cost over the sum of both exp weights; no proof obligations.
Claim. For real recognition costs $C_1,C_2$, the probability assigned to the first outcome is $p(C_1,C_2)=\frac{e^{-C_1}}{e^{-C_1}+e^{-C_2}}$.
background
The Probability Normalization Certificate module records that recognition-weighted two-outcome probabilities are a valid distribution: they are nonnegative, at most one, and sum to one. The only ingredients are positivity of the real exponential, the additivity of fractions with a common denominator, and self-division for a nonzero real.
Recognition cost enters as a real scalar $C$. Lower cost is preferred; the weight is $e^{-C}$. For a binary alternative the natural probability is that weight divided by the sum of both weights. The present definition is exactly that map. Downstream lemmas then check the three distribution axioms from elementary real analysis alone, with no physical hypotheses.
The module imports Mathlib and the light Born-rule measurement layer. The certificate is deliberately non-circular: pure algebra of exponentials.
proof idea
Definition, not a theorem. The body is the single term $\mathrm{Real.exp}(-C_1)/(\mathrm{Real.exp}(-C_1)+\mathrm{Real.exp}(-C_2))$. No tactics, no lemmas applied at the definition site. Later lemmas unfold this abbreviation and invoke Mathlib facts such as $\exp_\mathrm{pos}$ and $\mathrm{div_self}$.
why it matters
This is the atomic cost-to-probability map for the two-outcome recognition measurement model. The core theorem prob_normalization unfolds it twice (once for each ordering of the costs) and obtains sum-to-one by add-div and self-division. The companion lemmas prob_nonneg and prob_le_one likewise unfold it to get $0\le p\le 1$. Those three facts feed the structure ProbabilityNormalizationCert, which packages the verification predicate that recognition-weighted probabilities are normalized.
In the broader framework this is the algebraic backbone of the light Born-rule layer: once costs are assigned, probabilities are forced and automatically conserve. It does not itself derive the Born rule or the J-cost; it only certifies that the exponential weighting of any two real costs yields a genuine probability pair.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.