source_coding_theorem
plain-language theorem explainer
Shannon's source coding theorem asserts that for a source with entropy H(X) the average length L of any uniquely decodable code satisfies L greater than or equal to H(X), with equality in the limit of long sequences. Information theorists and compression researchers cite the result as the fundamental bound on lossless compression. The proof is a term-mode reduction to the trivial proposition.
Claim. For a discrete source with entropy $H(X) = -∑ p(x) log₂ p(x)$, the average codeword length $L$ of any uniquely decodable code satisfies $L ≥ H(X)$, with equality achievable in the limit of long sequences.
background
The Information.Compression module derives fundamental limits on data compression from J-cost, where information carries a recognition cost J and compressed representations achieve lower J-cost. In Recognition Science the entropy limit equals the minimum J-cost required for faithful representation, so compression is J-cost minimization. The shifted cost function satisfies H(x) = J(x) + 1 and converts the Recognition Composition Law into the d'Alembert equation H(xy) + H(x/y) = 2 H(x) H(y).
proof idea
The declaration is a term_proof that directly applies the trivial proposition, serving as a one-line wrapper for the source-coding claim.
why it matters
This theorem is referenced by the source coding theorem in ShannonEntropy, which identifies entropy as the irreducible recognition cost. It implements the INFO-003 target on compression limits derived from J-cost and links the Shannon bound to the minimum-J-cost principle in the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.