sourceEntropy
The definition computes the Shannon entropy of a discrete source from its symbol probabilities as the negative sum of each probability times its base-2 logarithm. Information theorists and Recognition Science researchers cite it when establishing lower bounds on lossless compression rates via J-cost. It is implemented as a direct list fold that accumulates the weighted log terms using the module's log2 helper.
claimFor a list of probabilities $(p_i)$, the source entropy is $H = -∑ p_i log₂ p_i$.
background
The module derives data compression limits from J-cost, where information carries a cost measured by the shifted functional H(x) = J(x) + 1 and entropy bounds the minimum cost for faithful representation. Upstream, entropy of a configuration equals its total defect, with zero defect yielding the minimum-entropy state. The imported log2 supplies the base-2 logarithm, while H from CostAlgebra reparametrizes the Recognition Composition Law into the d'Alembert form H(xy) + H(x/y) = 2 H(x) H(y).
proof idea
One-line definition that folds the probability list to accumulate the sum of p * log2 p terms and negates the result.
why it matters in Recognition Science
This definition supplies the entropy measure that realizes the minimum J-cost bound for faithful representation in the module's source coding theorem. It directly supports the claim that compression equals J-cost minimization and links Shannon entropy to the Recognition Science mechanism of organized information having lower cost. The declaration closes the gap between classical information theory and the J-cost functional equation.
scope and limits
- Does not normalize input probabilities to sum to one.
- Does not extend to continuous or differential entropy.
- Does not embed explicit J-cost or defect terms in the formula.
- Does not enforce non-negativity or other probability axioms.
formal statement (Lean)
65noncomputable def sourceEntropy (probs : List ℝ) : ℝ :=
proof body
Definition body.
66 -probs.foldl (fun acc p => acc + p * log2 p) 0
67
68/-! ## Compression Examples -/
69
70/-- Example: Fair coin (entropy = 1 bit).
71
72 P(H) = 0.5, P(T) = 0.5
73 H = -0.5 log₂(0.5) - 0.5 log₂(0.5) = 0.5 + 0.5 = 1 bit
74
75 Can't compress below 1 bit per symbol! -/