kolmogorovAxiomCount
plain-language theorem explainer
The theorem establishes that the inductive enumeration of Kolmogorov axioms contains exactly five cases. A researcher deriving probability as an exponential of recognition cost would cite the count to confirm alignment with configuration dimension five. The proof is a direct decision computation on the automatically derived finite type instance.
Claim. The cardinality of the set of Kolmogorov axioms is five: $|K| = 5$, where $K$ enumerates non-negativity, normalisation, additivity, total probability, and conditional probability.
background
In this module probability is the Boltzmann-like measure $P(event) = exp(-J(event))$, with $J$ the recognition cost. The KolmogorovAxiom inductive type enumerates the five standard axioms as constructors: non-negativity, normalisation, additivity, totalProbability, and conditional. The module states that this enumeration equals configuration dimension $D = 5$, and that $J(1) = 0$ recovers the certain event with probability one while $J(r) > 0$ for $r ≠ 1$ yields probability less than one.
proof idea
The proof is a one-line term that invokes the decide tactic on the Fintype instance derived from the inductive type with its five constructors.
why it matters
The result is referenced by the probabilityCert definition, which packages the axiom count with the zero-cost certain event and positive-cost uncertain events. It confirms that the recognition-cost interpretation of probability reproduces the classical five-axiom structure, consistent with the module claim that the axiom count equals configuration dimension five.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.