Motivation

How short can a code for a data source be, if the code must still be uniquely decodable — if every string of concatenated codewords can be unambiguously split back into the original symbols? Shannon's 1948 source coding theorem answers this exactly: the entropy of the source is a hard lower bound on the average codeword length of any uniquely decodable code, and it is also achievable up to a one-symbol slack. Entropy is not just a measure of "average surprise" — it is the literal, tight answer to a combinatorial question about how densely symbols can be packed into strings without losing decodability. This is the theorem that gives Shannon's entropy its operational meaning, and it underlies every practical lossless compression scheme (Huffman coding, arithmetic coding, Lempel–Ziv) as the benchmark they approach.

Timeline.

• 1948 — Claude Shannon, "A Mathematical Theory of Communication" (Bell System Technical Journal), introduces entropy and proves the source coding theorem.
• 1949 — Leon Kraft's MIT master's thesis proves the combinatorial inequality (for prefix codes) that makes the theorem's achievability half constructive.
• 1956 — Brockway McMillan extends Kraft's inequality's necessity direction from prefix codes to the strictly larger class of uniquely decodable codes, giving the theorem its full generality.

Setting

A source has a finite alphabet of symbols $\iota$, with at least two symbols, and probability distribution $p:\iota\to\mathbb R$ ($p_i>0$, $\sum_i p_i=1$). A code assigns to each symbol $i$ a codeword $c(i)$, a finite string over a $D$-ary code alphabet $\alpha$ ($D=|\alpha|\ge 2$); the code is uniquely decodable if every finite sequence of codewords is determined by its concatenation. The entropy of $p$ in base $D$ is

$$H_D(p) = -\sum_i p_i \log_D p_i.$$

The expected codeword length of $c$ under $p$ is $L(c) = \sum_i p_i \, |c(i)|$.

Formalization targets

Goal — Shannon's source coding theorem

$$\forall \text{ injective, uniquely decodable } c,\quad H_D(p) \le L(c), \qquad \exists \text{ such } c,\quad L(c) < H_D(p) + 1.$$

(For a source with $|\iota| \ge 2$ symbols — see Formalization scope for why the single-symbol case must be excluded.)

Significance

The result itself. This theorem is the reason entropy is called entropy in an information-theoretic sense at all: it converts a quantity defined by an abstract formula ($-\sum p_i\log p_i$) into the exact answer to an operational question (minimum achievable expected code length), with a slack no worse than one symbol. It is the founding theorem of lossless source coding and the benchmark every practical compressor is measured against.

Formalizing it. Mathlib recently gained genuine information-theoretic coding content: InformationTheory.UniquelyDecodable and the necessity direction of the Kraft–McMillan inequality (McMillan's 1956 result: a uniquely decodable code's lengths satisfy $\sum_w D^{-|w|}\le 1$) are already proved, via a counting argument on concatenations of $r$ codewords. This mission builds directly on that foundation rather than duplicating it. What Mathlib does not have — and what this mission's milestones supply — is Kraft's original 1949 sufficiency direction (existence of a uniquely decodable code realizing any length assignment satisfying the Kraft sum bound), any notion of Shannon entropy for a general finite distribution, and the source coding theorem itself.

Difficulty

The lower bound ($H_D(p)\le L(c)$) is the easier half: it follows from the Kraft–McMillan inequality (already in Mathlib) via Gibbs'/Jensen's inequality applied to the two probability-like sequences $p_i$ and $D^{-\ell_i}/K$ (where $K=\sum_j D^{-\ell_j}\le1$ is the Kraft sum) — a short, self-contained convexity argument.

The achievability half is the genuine construction. Given the ideal (generally non-integer) lengths $-\log_D p_i$, one rounds up to $\ell_i=\lceil -\log_D p_i\rceil$ (Shannon–Fano–Elias lengths); a one-line estimate shows $D^{-\ell_i}\le p_i$, so the Kraft sum of the rounded lengths is still $\le\sum_i p_i=1$, and the bound $\ell_i<-\log_D p_i+1$ gives $L(c)<H_D(p)+1$ immediately once a code with exactly these lengths is shown to exist. Producing that code is Kraft's sufficiency direction, and it needs an explicit construction: order the lengths, and assign to symbol $i$ the first $\ell_i$ digits of the $D$-ary expansion of the cumulative sum $\sum_{j<i} D^{-\ell_j}$. Verifying this assignment is injective, has the prescribed lengths, and is uniquely decodable (indeed prefix-free) is a careful but standard combinatorial argument — the main open piece of this mission.

Formalization scope

The source alphabet $\iota$ must have at least two symbols ($|\iota|\ge 2$), not merely be nonempty. A single-symbol source forces $p\equiv 1$ and entropy $H_D(p)=0$, so the achievability conjunct would demand a codeword of length $0$ — but a uniquely decodable code can never contain the empty codeword (InformationTheory.UniquelyDecodable.epsilon_not_mem, provable from the definition: the empty string decodes ambiguously as zero or two copies of itself), so no admissible code exists and the theorem would be false, not merely hard, at $|\iota|=1$. The same defect breaks Kraft's sufficiency direction (Milestone 2) whenever any prescribed length is $0$, independent of $|\iota|$; that milestone accordingly requires every length strictly positive. With $|\iota|\ge2$ and full support, every $p_i<1$ strictly, so the Shannon–Fano lengths $\lceil-\log_D p_i\rceil$ are automatically all $\ge1$, and the achievability construction only ever needs Milestone 2 at positive lengths. The code alphabet $\alpha$ is likewise an arbitrary finite type (matching Mathlib's own Fintype/Nonempty conventions for the Kraft–McMillan file), with $|\alpha|\ge2$ required to keep Real.logb non-degenerate. The source distribution is required strictly positive ($p_i>0$) — the standard simplifying assumption (zero-probability symbols can always be dropped without loss). Unique decodability is stated exactly as Mathlib's InformationTheory.UniquelyDecodable, not re-derived from a "prefix code" definition, so the mission's results transport directly onto Mathlib's existing Kraft–McMillan file. A trivializing route to rule out: proving only the lower bound (citing Mathlib's inequality) while leaving the existential achievability half unaddressed would not be Shannon's theorem — the sandwich $H_D(p)\le L^*<H_D(p)+1$ is the theorem's actual content, and the lower bound alone (already essentially free from Mathlib) is not a novel contribution on its own.

Reusable output: the Kraft sufficiency construction (Milestone 2) is directly reusable for any future formalization of Huffman coding optimality, arithmetic coding, or the general "Kraft-inequality-achieving code exists" fact used throughout coding theory. Contributions are welcome starting from Milestone 2 (the open construction) or Milestone 3 (the Gibbs'-inequality lower bound, which only needs Milestone 1, already available via Mathlib).

Selected references

• C. E. Shannon, "A Mathematical Theory of Communication," The Bell System Technical Journal 27 (1948), 379–423, 623–656.
• T. M. Cover and J. A. Thomas, Elements of Information Theory, 2nd ed., Wiley, 2006, Chapter 5 ("Data Compression"), §5.2 ("Kraft Inequality") and §5.4 ("Bounds on the Optimal Code Length," Theorem 5.4.1).
• L. G. Kraft, A Device for Quantizing, Grouping, and Coding Amplitude-Modulated Pulses, M.S. thesis, MIT, 1949.
• B. McMillan, "Two Inequalities Implied by Unique Decipherability," IRE Transactions on Information Theory 2:4 (1956), 115–116.
• Mathlib, Mathlib.InformationTheory.Coding.UniquelyDecodable and Mathlib.InformationTheory.Coding.KraftMcMillan (2026).