uncertain_event_positive_cost
plain-language theorem explainer
The theorem establishes that for positive real r not equal to 1 the J-cost is strictly positive. Researchers deriving Kolmogorov axioms from recognition cost would cite it to confirm that uncertain events carry positive cost and thus probability strictly below 1. The proof is a one-line wrapper applying the core positivity lemma Jcost_pos_of_ne_one.
Claim. For every real number $r > 0$ with $r ≠ 1$, the J-cost satisfies $0 < J(r)$.
background
In this module probability is introduced as the Boltzmann-like measure $P = exp(-J)$, where $J$ is the recognition cost function. The five Kolmogorov axioms are recovered when the configuration dimension equals 5, with the special case $J(1) = 0$ giving $P = 1$ for certain events. The upstream lemma Jcost_pos_of_ne_one states that $J(x) > 0$ whenever $x > 0$ and $x ≠ 1$, proved by rewriting $Jcost$ via its squared form and applying positivity of squares and division.
proof idea
The proof is a one-line wrapper that applies the lemma Jcost_pos_of_ne_one from the Cost module (and its duplicates in JcostCore and LocalCache) directly to the hypotheses hr and hne.
why it matters
This result supplies the uncertain_positive field inside the ProbabilityCert record, which bundles the five axioms with the cost interpretations for certain and uncertain events. It thereby closes the link between positive J-cost for $r ≠ 1$ and $P < 1$, supporting the module claim that probability theory emerges from the J-cost structure. The construction aligns with the J-uniqueness step in the forcing chain and the overall RS derivation of probability as exp(-J).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.