entropy_nonneg
plain-language theorem explainer
Shannon entropy is non-negative for every discrete probability distribution over finitely many outcomes. Researchers deriving information measures from Recognition Science's J-cost structure would cite this bound when establishing information content as a ledger quantity. The proof unfolds the entropy definition to a negated sum and shows each term p log p is non-positive via case analysis on whether the probability exceeds zero, using log non-positivity for p in (0,1] together with the normalization and non-negativity axioms of ProbDist.
Claim. For any natural number $n$ and any discrete probability distribution $d$ over $n$ outcomes (non-negative probabilities summing to 1), the Shannon entropy satisfies $H(d) = -∑ p_i log p_i ≥ 0$.
background
The module derives Shannon entropy from Recognition Science's J-cost, where J(x) = ½(x + 1/x) - 1 measures recognition effort on probability ratios. ProbDist is the structure of a discrete distribution: a map probs : Fin n → ℝ that is non-negative and sums to 1 over the finite set of outcomes. The local setting is INFO-001, which shows H = -Σ p_i log(p_i) emerges as total J-cost minimization over probability distributions, with uniform distributions maximizing entropy and deviations from uniformity lowering it. Upstream, entropy in InitialCondition is defined as total_defect of a configuration, providing the zero-entropy minimum state that this non-negativity result extends to the information setting.
proof idea
The tactic proof unfolds shannonEntropy, reduces via simp to a negated sum that must be shown non-positive, then applies Finset.sum_nonpos. For each index it performs by_cases on whether probs i > 0: when positive it proves probs i ≤ 1 from normalization and single_le_sum, invokes Real.log_nonpos to obtain log(probs i) ≤ 0, and concludes with mul_nonpos_of_nonneg_of_nonpos; when zero the term vanishes by simp.
why it matters
This theorem supplies the base non-negativity for IC-001.10 in InformationIsLedger, which certifies that information content is non-negative and feeds the ic001_certificate establishing Information IS the Ledger. It is also invoked by the NoHairTheorem to bound entropy by area. In the Recognition framework it closes the information-measure non-negativity step that follows from J-cost (T5 J-uniqueness) and the forcing chain, confirming entropy as a ledger quantity without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.