shannon_equals_jcost
plain-language theorem explainer
Shannon entropy of a discrete probability distribution equals its total J-cost. Information theorists and Recognition Science researchers cite this to derive entropy directly from cost minimization over distributions. The proof is a direct algebraic verification: unfold the definitions, rewrite the negated sum, then apply congr and case analysis on positive probabilities to confirm pointwise equality.
Claim. For a probability distribution $d$ over $n$ outcomes with probabilities $p_i$, the Shannon entropy $H(d) = -∑ p_i log p_i$ equals the total J-cost $∑ p_i (-log p_i)$.
background
The module derives Shannon entropy from Recognition Science's J-cost structure. A ProbDist n is a structure with probs : Fin n → ℝ, nonnegativity for all i, and normalization (Finset.univ.sum probs = 1). J-cost measures recognition effort via J(x) = ½(x + 1/x) - 1 applied to probability ratios, with totalJCost d defined as the sum of probJCost terms over the support. The local theoretical setting is INFO-001, whose core insight is that entropy quantifies uncertainty as total recognition cost over distributions, emerging from deviation from uniformity.
proof idea
The term proof unfolds shannonEntropy, totalJCost, and probJCost. It rewrites the left-hand side via sum_neg_distrib, applies congr 1 and funext to reduce to pointwise comparison, then uses by_cases on d.probs i > 0 followed by simp with neg_mul and neg_neg to equate the branches.
why it matters
This establishes the direct link between Shannon entropy and total J-cost, feeding directly into shannon_entropy_equals_expected_jcost (IC-001.9: H(X) = Σ p_i · J(p_i) equals expected information cost) and entropy_is_expected_surprisal. It fills the key connection cited in the paper Foundation of physics - Information theory from RS, tying information measures to J-uniqueness (T5) and the forcing chain in the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.