sourceEntropy
plain-language theorem explainer
sourceEntropy defines the Shannon entropy H = -∑ p_i log₂ p_i for a discrete source given as a list of probabilities. Workers on information limits in Recognition Science cite it when linking entropy to minimum J-cost for faithful representations. The definition is a direct foldl implementation of the standard formula using the module's log2.
Claim. The entropy of a source with symbol probabilities $p_1, p_2, ..., p_n$ is given by $H = -∑_{i=1}^n p_i log_2 p_i$.
background
The Information.Compression module targets INFO-003, deriving fundamental limits on data compression from J-cost. Shannon's source coding theorem states that average code length is at least the entropy H(X) = -Σ p(x) log₂ p(x), and no scheme can beat this bound. In Recognition Science, entropy equals the minimum J-cost for faithful representation, so compression is J-cost minimization.
proof idea
The definition is a direct one-line wrapper that negates the foldl accumulation of p * log2 p over the input list, relying on the sibling log2 definition.
why it matters
This definition supplies the entropy measure required by INFO-003 to connect information theory to the J-functional. It supports the sibling source_coding_theorem and positions entropy as the J-cost floor arising from CostAlgebra.H and the Recognition Composition Law. It advances the claim that compression bounds follow from the same functional equation that forces phi and D=3.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.