deterministic_has_zero_entropy
plain-language theorem explainer
A discrete probability distribution with one outcome of probability 1 and all others zero has Shannon entropy exactly zero. Recognition Science researchers cite this to identify the deterministic state with the balanced ledger of zero information cost. The proof is a direct one-line application of the zero_entropy_deterministic lemma in the ShannonEntropy module.
Claim. Let $d$ be a probability distribution over $n$ outcomes with $d_i=1$ for a fixed index $i$ and $d_j=0$ for all $j≠i$. Then the Shannon entropy satisfies $H(d)=0$.
background
The module InformationIsLedger treats information as the physical ledger in Recognition Science. Every recognition event carries a J-cost given by the cost function on positive ratios, with J(x)=0 precisely when x=1 (balanced state) and J(x)>0 otherwise. Shannon entropy is defined as the expected J-cost over a discrete distribution, unifying the two measures. ProbDist n is the structure of n non-negative probabilities summing to 1. The upstream zero_entropy_deterministic lemma in ShannonEntropy states that any distribution with a single probability 1 and the rest zero has entropy zero.
proof idea
One-line wrapper that applies ShannonEntropy.zero_entropy_deterministic d i hdet hother.
why it matters
This theorem supplies IC-001.11, confirming the deterministic state has zero entropy and therefore zero information cost. It closes one of the core claims in the Information IS the Ledger module: perfect knowledge equals the balanced ledger. The result anchors the equivalence between Shannon entropy and expected J-cost, supporting the framework claim that information is the physical substrate rather than an abstraction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.