ProbabilityCert
plain-language theorem explainer
ProbabilityCert packages the verification that the recognition cost J satisfies the five Kolmogorov axioms with J(1) equal to zero for certain events and strictly positive otherwise. Researchers deriving probability measures from Recognition Science cost functions would cite this structure to confirm the mapping P = exp(-J). The definition is a direct bundling of the axiom cardinality check and the two J-cost properties drawn from the same module.
Claim. A structure $ProbabilityCert$ consists of three fields: the finite cardinality of the set of Kolmogorov axioms equals 5; the recognition cost satisfies $J(1) = 0$; and for every real $r$ with $0 < r$ and $r ≠ 1$, the recognition cost satisfies $J(r) > 0$.
background
In Recognition Science, probability is defined as a recognition cost measure with $P(event) = exp(-J(event))$, where $J$ is the J-cost function. The module states that the five Kolmogorov axioms (non-negativity, normalisation, additivity, total probability, conditional probability) match configuration dimension 5. The upstream KolmogorovAxiom inductive type enumerates exactly these five constructors with DecidableEq and Fintype instances.
proof idea
This is a structure definition that directly encodes the three required properties. It uses the Fintype.card computation on the KolmogorovAxiom inductive type together with the two J-cost lemmas certain_event_zero_cost and uncertain_event_positive_cost.
why it matters
The structure supplies the type instantiated by the downstream probabilityCert definition, which assembles the five-axiom count and J-cost properties into a single certificate. It supports the module's claim that probability theory follows from the RS functional equation via the Boltzmann-like measure and the five-dimensional axiom space. It touches the open question of whether the full Kolmogorov axioms can be recovered from J alone without further scaffolding.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.