pos_entropy
plain-language theorem explainer
Positive entropy follows directly from the strict positivity of the J-cost for any positive real ratio not equal to one. Researchers formalizing information theory inside the Recognition Science setting cite this result to secure H ≥ 0 for uncertain outcomes. The proof is a one-line wrapper that invokes the core J-cost positivity lemma.
Claim. For every real number $r$ with $0 < r$ and $r ≠ 1$, the J-cost satisfies $0 < J(r)$.
background
The Information Theory from RS module identifies Shannon entropy with the average J-cost of a probability distribution. J-cost is the function that assigns a recognition cost to each ratio r, and the module equates Shannon's five axioms to a five-dimensional configuration space while deriving H ≥ 0 from J ≥ 0. The upstream lemma Jcost_pos_of_ne_one states that J(x) > 0 for x ≠ 1 and x > 0, proved by rewriting Jcost via its square 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 (with identical statements appearing in JcostCore and LocalCache).
why it matters
This theorem supplies the pos_H field inside the informationTheoryCert definition, which bundles the five Shannon axioms, minimum entropy, and positive entropy into a single certificate. It anchors nonnegativity of entropy in the RS framework where J-cost is the primitive cost measure and aligns with the interpretation of entropy as average J-cost. It completes the positivity requirement for the information-theory certification without new axioms.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.