entropy_nonneg
plain-language theorem explainer
Entropy is non-negative for any probability distribution over a finite number of outcomes. Researchers working on the information-as-ledger equivalence cite this as IC-001.10 to ground non-negativity of information measures. The proof is a one-line wrapper that delegates directly to the non-negativity theorem in the imported ShannonEntropy module.
Claim. For any natural number $n$ and any probability distribution $d$ over $n$ outcomes, the Shannon entropy $H(d)$ satisfies $H(d) ≥ 0$.
background
The InformationIsLedger module treats information as the physical ledger: every recognition event is a ratio $x > 0$ carrying J-cost $J(x) = (x + x^{-1})/2 - 1$, with zero cost only at the balanced state $x = 1$. Shannon entropy is identified with expected J-cost over a distribution, per the module's core list of results. Upstream, InitialCondition defines configuration entropy as total defect (zero defect yields minimum entropy), while ObserverForcing and MultiplicativeRecognizerL4 supply the underlying cost functions. The ShannonEntropy module provides the base non-negativity result used here.
proof idea
The proof is a one-line wrapper that applies the entropy_nonneg theorem from the ShannonEntropy module to the input distribution $d$.
why it matters
This result completes the non-negativity step in the IC-001 series and is referenced by the ic001_certificate definition that lists all derived ledger properties. It is also invoked by the NoHairTheorem to bound Bekenstein-Hawking entropy by horizon area. In the Recognition framework it aligns with T5 J-uniqueness and the requirement that all costs on the phi-ladder are non-negative, supporting the claim that Shannon entropy equals expected J-cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.