probabilityCert
plain-language theorem explainer
This definition packages the five Kolmogorov axioms together with the recognition-cost properties J(1)=0 and J(r)>0 for uncertain r into a single certificate record. Workers deriving probability measures from the RS cost function would cite it to verify that the axiom count matches the five-dimensional configuration required by the framework. The construction is a direct record literal that substitutes the counting theorem and the two cost lemmas into the ProbabilityCert structure.
Claim. The probability certificate is the structure whose fields are: the cardinality of the Kolmogorov axioms equals 5, the recognition cost of the unit event satisfies $J(1)=0$, and the recognition cost of every uncertain event satisfies $J(r)>0$ whenever $0<r$ and $r≠1$.
background
In the module Probability Theory from RS, probability is identified with the exponential of the negative recognition cost: $P(event)=exp(-J(event))$. The structure ProbabilityCert records the five Kolmogorov axioms (non-negativity, normalisation, countable additivity, total probability, conditional probability) together with the two cost properties that make this identification consistent. The upstream lemma kolmogorovAxiomCount establishes the axiom count by direct enumeration. The lemmas certain_event_zero_cost and uncertain_event_positive_cost supply the required cost values J(1)=0 and J(r)>0 for r≠1, each obtained from the basic properties of the J-cost function.
proof idea
The definition is a one-line record construction that directly inserts the three upstream results: kolmogorovAxiomCount for the axiom cardinality, certain_event_zero_cost for the certain-event cost, and uncertain_event_positive_cost for the uncertain-event cost. No further tactics or reductions are applied.
why it matters
The declaration supplies the concrete witness that the five Kolmogorov axioms arise naturally once probability is re-expressed as a recognition-cost measure, thereby closing the link between the RS cost function and standard probability theory. It sits inside the module that derives probability axioms from the recognition framework and is available for any later development that needs a certified probability measure compatible with J-cost. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.