shannon_entropy_equals_expected_jcost
plain-language theorem explainer
Shannon entropy for any discrete probability distribution over n outcomes equals the expected J-cost under the Recognition Science measure. Information theorists and physicists grounding entropy in physical cost would cite this unification. The proof is a direct one-line application of the preceding lemma that equates the entropy formula to the weighted J-cost sum.
Claim. For a probability distribution with probabilities $p_i$ ($i=1$ to $n$) where each $p_i$ is non-negative and sums to 1, the Shannon entropy $H$ equals the expected J-cost given by $H = sum p_i J(p_i)$, with $J$ the Recognition Science information cost function.
background
The module treats information as identical to the physical ledger, where every recognition event is a ratio carrying a definite J-cost. The J-cost vanishes only at perfect balance (ratio 1) and is strictly positive otherwise, with the total J-cost for a distribution defined as the probability-weighted sum of individual J values. A discrete probability distribution over n outcomes is any assignment of non-negative real numbers summing to one. The result rests on the upstream equality that identifies the classical entropy expression with this weighted sum.
proof idea
The proof is a one-line term-mode wrapper that applies the equality lemma between Shannon entropy and J-cost summation from the ShannonEntropy module.
why it matters
This occupies the IC-001.9 slot in the Information IS the Ledger sequence and shows that Shannon entropy is exactly the expected J-cost, unifying the classical definition with the Recognition Science ledger. It advances the claim that information constitutes physical reality and is consistent with J-uniqueness in the forcing chain. No open questions are resolved here and no downstream uses are recorded.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.