zero_entropy_deterministic
plain-language theorem explainer
A probability distribution with one outcome of probability 1 and all others zero has Shannon entropy exactly zero. Recognition Science researchers cite it to show that perfect certainty produces zero information cost under the J-cost structure. The proof is a direct term-mode reduction that unfolds the entropy sum and applies case analysis to make every term vanish.
Claim. Let $d$ be a discrete probability distribution over $n$ outcomes with $d(i)=1$ for some index $i$ and $d(j)=0$ for all $j≠i$. Then the Shannon entropy $H(d)=-∑_k d(k)log d(k)$ equals zero.
background
ProbDist is the structure of a function probs: Fin n → ℝ together with proofs that every value is nonnegative and the values sum to one. Shannon entropy is the negative sum of p log p over those probabilities. The module derives this entropy from Recognition Science's J-cost, where J(x)=½(x+1/x)-1 quantifies recognition effort on probability ratios and total cost minimization recovers the classical formula.
proof idea
The proof unfolds shannonEntropy, simplifies the outer negation, and invokes Finset.sum_eq_zero. It then splits on whether the summation index equals the deterministic index i: the matching case reduces to Real.log_one while the non-matching case uses the hypothesis that the probability is zero.
why it matters
The result is invoked by deterministic_has_zero_entropy in InformationIsLedger, which records it as IC-001.11: the deterministic distribution has zero entropy, so perfect knowledge equals zero information cost and a balanced ledger. It supplies the minimum-entropy case in the derivation of Shannon entropy from J-cost over distributions, closing the lower bound in the information-theory portion of the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.