Information Compression Source Coding Theorem

The Entropy Limit

In information theory, the source coding theorem, proved by Claude Shannon in 1948, sets the hard floor for lossless data compression. For any source that emits symbols with probabilities p(x), the average length L of a uniquely decodable code must be at least the entropy H(X) = -Σ p(x) log₂ p(x). The entropy is measured in bits, and log base 2 means a fair coin toss carries exactly one bit of information. No clever scheme, however elaborate, can pack the data into fewer bits on average without losing information. Huffman coding reaches L ≤ H + 1, while arithmetic coding approaches the limit L → H for long messages. The theorem is why zip files cannot shrink random data: a fair coin's output has entropy 1 bit per toss, so its compressed form is already at the floor.

The classical theorem also has a companion in algorithmic information theory. Kolmogorov complexity, defined independently by Solomonoff, Kolmogorov, and Chaitin in the 1960s, measures the shortest program that outputs a given string. Most strings are incompressible: their shortest description is about as long as the string itself. This is not a practical limitation but a logical one, since a shorter description would itself be a shorter string, and counting arguments show only a tiny fraction of strings can have short programs. The two limits, Shannon's statistical entropy and Kolmogorov's algorithmic complexity, capture the same intuition from different directions: structure is compressible, randomness is not.

In Recognition Science, the framework models compression as a form of cost, a forced penalty on representation. Its library, a machine-checked collection of formal theorems, defines messageJCost as length times (1 - redundancy), so a redundant message costs less than its raw length suggests. The framework's source_coding_theorem restates the classical bound: L ≥ H for any uniquely decodable code. The entropy limit appears as the minimum cost for a faithful representation, and compression becomes the act of minimizing that cost. The library also records that English text carries about 70 percent redundancy, meaning its letter entropy of 4.2 bits per character is far below the 5 bits a uniform alphabet would need.

The framework's contribution is a change of vocabulary, not a new bound. It does not derive a tighter compression limit than Shannon's, nor does it prove that entropy equals cost in any measurable physical sense. The declarations that connect compression to J-cost are marked as trivial theorems, placeholders that assert the intended statement without a substantive proof. The honest reading is that the framework re-describes a known result in its own terms, and the empirical content, such as English redundancy, comes from standard measurements, not from the framework's axioms.

/-- Shannon's source coding theorem (noiseless coding theorem):

    For a source with entropy H(X):
    - Average code length L ≥ H(X)
    - Equality achievable in the limit of long sequences

    This is the fundamental compression limit! -/
theorem source_coding_theorem :
    -- L ≥ H for any uniquely decodable code
    True := trivial

/-- Shannon's source coding theorem (noiseless coding theorem):

    For a source with entropy H(X):
    - Average code length L ≥ H(X)
    - Equality achievable in the limit of long sequences

    This is the fundamental compression limit! -/
theorem source_coding_theorem :
    -- L ≥ H for any uniquely decodable code
    True := trivial

/-- The J-cost of a message:

    J(message) = length × (1 - redundancy)

    Maximum compression: J = entropy (no redundancy left).

    This explains why you can't compress random data:
    Random data already has minimum J-cost for its entropy! -/
noncomputable def messageJCost (length redundancy : ℝ) : ℝ :=
  length * (1 - redundancy)

theorem english_is_redundant :
    -- English has ~70% redundancy
    True := trivial

What this page does not claim

The framework derives a new compression limit tighter than Shannon's entropy bound. The framework proves that entropy equals a measurable physical cost in actual data systems. The trivial theorems connecting compression to J-cost constitute substantive proofs.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Information/Compression.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: