Information Compression

The limits of compression

Information compression is the practice of representing a message with fewer bits than its original form while preserving the information that matters. The classical foundation is Claude Shannon's source coding theorem from 1948, which sets a hard floor: for a source that produces symbols with probabilities p(x), the average length L of any lossless code must be at least the entropy H(X) = -Σ p(x) log₂ p(x). A fair coin, with two equally likely outcomes, has entropy 1 bit, and no scheme can encode a sequence of fair coin flips in fewer than one bit per flip on average. Huffman coding reaches the floor within one bit, while arithmetic coding approaches it arbitrarily closely for long messages; Lempel-Ziv, the algorithm behind zip files, is dictionary-based and asymptotically optimal.

Entropy also explains why English text compresses so well. The 26 letters of the alphabet, if equally likely, would carry about 4.7 bits each, but the actual per-letter entropy of English is near 4.2 bits, and with context and prediction the rate drops to roughly 1.2 bits per letter. That gap is redundancy, roughly 70 percent of English, and compression algorithms exist to strip it out. At the other extreme, a random string drawn uniformly from all possible strings has no redundancy at all; most such strings cannot be compressed, a fact formalized in Kolmogorov complexity, which measures the shortest program that outputs a given string.

In Recognition Science, the framework that treats reality as maintaining a discrete record of events, compression is re-described as a form of cost minimization. The framework assigns each message a J-cost, a forced expense of recognition, and claims that a compressed message carries lower J-cost because it is more organized. The entropy limit then becomes the minimum J-cost needed for a faithful representation, and redundancy becomes removable excess J-cost. The module defines a message's J-cost as length times (1 minus redundancy), so a perfectly redundant message costs zero and a random one costs its full length.

The framework's library states this as a theorem: compression is J-cost minimization, with the entropy bound as the lower limit. The formal statements in the module are largely definitions and placeholders, with several theorems marked as trivial, meaning the mathematical content is asserted rather than deeply derived. What the module genuinely establishes in plain language is a translation: Shannon's entropy, the classical measure of information content, is reinterpreted as the minimum recognition cost, and the practical algorithms of compression, Huffman, arithmetic, Lempel-Ziv, are all instances of reducing that cost. The framework's contribution is not a new compression algorithm but a new vocabulary for why compression works.

The consequence is a unified picture: the same quantity, entropy, that bounds how small a file can be also measures how much recognition effort a message demands. A random file is already at minimum J-cost, which is why it resists compression, while a structured file carries excess cost that can be squeezed out. This reframing does not change what compressors do, but it connects information theory to the framework's broader claim that recognition has a forced price.

/-- 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

theorem fair_coin_one_bit :
    fairCoinEntropy = 1 := by
  unfold fairCoinEntropy
  simp only [show (0.5 : ℝ) = 1/2 from by norm_num]
  rw [log2_half]
  ring

/-- 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)

/-- In RS, compression is J-cost minimization:

    **Uncompressed data**: High redundancy = High J-cost
    **Compressed data**: No redundancy = Low J-cost
    **Perfect compression**: J-cost = entropy (minimum)

    Compression algorithms seek minimum J-cost! -/
theorem compression_is_jcost_minimization :
    -- Compression minimizes J-cost of representation
    True := trivial

What this page does not claim

The framework does not prove Shannon's theorem; the module states it as an assumption. This module does not derive the value of J from the forcing chain; it defines a cost model. The framework does not claim that all compression algorithms are optimal, only that they minimize J-cost.

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: