certain_event_zero_cost
plain-language theorem explainer
The result shows that the recognition cost J of the certain event equals zero. Probability theorists deriving Kolmogorov axioms from recognition science would reference this to anchor the normalization condition P=1. The proof reduces immediately to the unit lemma for the J-cost function.
Claim. The recognition cost of the certain event satisfies $J(1)=0$, which implies probability one via the Boltzmann-like measure $P=exp(-J)$.
background
J-cost is defined by the squared-ratio formula $J(x)=(x-1)^2/(2x)$, which vanishes exactly at the unit element. The module treats probability as the exponential of negative recognition cost, so $P(event)=exp(-J(event))$, and maps the five Kolmogorov axioms to a configuration dimension of five. The upstream Jcost_unit0 lemma establishes the same identity by direct simplification of the J-cost definition.
proof idea
The proof is a one-line wrapper that directly invokes the Jcost_unit0 lemma from the Cost module.
why it matters
This theorem supplies the certain_zero field inside the ProbabilityCert definition that assembles the five Kolmogorov axioms from recognition cost. It confirms the zero-cost certain event required for normalization in the RS probability measure, consistent with the forcing chain that begins from J-uniqueness and leads to the phi-ladder and dimensional constraints.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.