KolmogorovAxiom
plain-language theorem explainer
KolmogorovAxiom encodes the five Kolmogorov axioms as constructors of an inductive type, where probability arises as exp(-J) for the recognition cost J. A researcher deriving probability measures from the J-functional would cite it to fix the axiom count at the configuration dimension D=5. The declaration is a direct inductive enumeration of non-negativity, normalisation, additivity, total probability, and conditional probability.
Claim. The five Kolmogorov axioms (non-negativity, normalisation, additivity, total probability, conditional probability) form an inductive type whose constructors label the properties satisfied by $P(r) = e^{-J(r)}$ with $J$ the recognition cost function.
background
In Recognition Science, probability is the recognition cost measure $P(event) = exp(-J(event))$. The module states that the five Kolmogorov axioms equal the configuration dimension D=5. The certain event has J(1)=0 so P=1, while uncertain events r≠1 have J(r)>0 and thus P<1. This builds directly on the Cost module for the definition of Jcost.
proof idea
The declaration is an inductive definition that introduces exactly five constructors: nonNegativity, normalisation, additivity, totalProbability, and conditional. No lemmas are invoked and no tactics are applied; it is a direct enumeration.
why it matters
KolmogorovAxiom is the axiom set used by kolmogorovAxiomCount (which proves Fintype.card = 5) and by ProbabilityCert (which pairs the five axioms with Jcost 1 = 0 and positive Jcost for r≠1). It supplies the precise link from the J-functional to classical probability axioms, matching the RS configuration dimension D=5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.