Rothvoß Discrepancy Notes I: Spencer's Theorem via the Entropy MethodTextbook
## Motivation
**Discrepancy theory** asks how unbalanced a two-coloring of a combinatorial structure must be in the worst case. Concretely: given $n$ sets over an $n$-element ground set, color each element $+1$ or $-1$ so that every set is as close to balanced as possible. The question is classical (Beck–Fiala 1981; Spencer 1985) and the answer for general (dense) set systems is one of the sharpest gaps between a naive probabilistic bound and the truth known in combinatorics: assigning colors uniformly at random only guarantees discrepancy $\Theta(\sqrt{n\log n})$, yet a coloring with discrepancy $O(\sqrt n)$ always exists — the logarithmic factor is an artifact of the naive argument, not of the problem. This mission formalizes that removal, following T. Rothvoß's lecture-note exposition of J. Spencer's **entropy method** ([MIT 18.095, "Discrepancy theory"](https://math.mit.edu/classes/18.095/lect6/notes.pdf)), the standard modern presentation of the technique (see also Matoušek, *Geometric Discrepancy*, Ch. 4). The entropy method is the ancestor of the whole "partial coloring" family of arguments used throughout discrepancy theory and combinatorial algorithm design, so a machine-checked account of its base case is reusable well beyond this one theorem.
## Setting
Fix $n\ge 1$ and an $n\times n$ matrix $A$ with entries in $\{0,1\}$, thought of as the incidence matrix of $n$ sets $S_1,\dots,S_n$ over an $n$-element ground set: $A_{ij}=1$ iff element $j$ lies in set $S_i$. A **coloring** is a map $\varepsilon:\{1,\dots,n\}\to\{-1,+1\}$, and the **discrepancy of row $i$ under $\varepsilon$** is $\bigl|\sum_j A_{ij}\varepsilon_j\bigr|$, the signed imbalance of set $S_i$. The **discrepancy of the matrix** is the value achieved by the best coloring, minimizing the worst row.
The entropy method bounds this via the **partial coloring lemma**: rather than coloring all $n$ elements at once, one repeatedly colors a constant fraction of the *currently uncolored* elements while keeping every row's contribution small, then recurses on what remains. Each round is itself produced by an entropy/pigeonhole argument: quantize each row's signed sum (under a uniformly random coloring) into $O(1)$ "shells" of width $\Theta(\sqrt m)$ (where $m$ is the number of active elements); a short computation shows this quantization carries very little **Shannon entropy** $H(Z)=\sum_x \Pr[Z=x]\log_2\frac{1}{\Pr[Z=x]}$ once the shell width exceeds a threshold; subadditivity of entropy across the $n$ rows then bounds the *joint* quantization entropy, which by pigeonhole forces an exponentially large set of colorings landing in the same joint shell; Kleitman's theorem on the diameter of a large subset of the Hamming cube then extracts two such colorings that are far apart in Hamming distance, and their difference is the sought partial coloring.
## Formalization targets
**Goal.**
$$
\exists\, C\in\mathbb R,\ \forall n\ge 1,\ \forall A\in\{0,1\}^{n\times n},\ \exists\,\varepsilon\in\{-1,1\}^n,\ \forall i,\ \Bigl|\sum_{j=1}^n A_{ij}\varepsilon_j\Bigr|\le C\sqrt n.
$$
This is the qualitative, constant-suppressed form of Spencer's theorem: it asserts $O(\sqrt n)$ discrepancy with a single universal constant, and deliberately leaves that constant unspecified. This is the right goal for this mission because it is the weakest statement that is still stable: any future improvement to the constant (down to Spencer's sharp $6$, or beyond) refines this theorem rather than invalidating it.
## Significance
The removal of the $\sqrt{\log n}$ factor is the entire content of Spencer's theorem: it is what separates discrepancy theory from a corollary of concentration inequalities, and the partial-coloring/entropy method it introduced underlies later results throughout the field (Beck–Fiala-type bounds, the Komlós conjecture literature, and constructive/algorithmic discrepancy minimization). Formalizing it is formalizing the base case that every later partial-coloring argument specializes.
This mission's goal theorem, `spencer_discrepancy_sqrt_n_bound`, is **already proved** (zero `sorry`s), by a from-scratch entropy-method development: the per-row shell-entropy bound, the joint pigeonhole-and-Kleitman assembly for one round, and the outer geometric iteration and induction combining rounds into a full coloring. What remains open in this mission is `shannonEntropy_shellFin_le` (Lemma 9 in Rothvoß's notes) — the per-row entropy bound is currently imported as an assumption by the one-round lemma `lemma8_partial_coloring_round`, which is therefore only conditionally proved pending it. A separate, harder mission on this platform (`Komlos.spencer_six_deviations`) targets Spencer's *sharp* constant $6$ via a tighter, non-standard numeric derivation; that is a distinct, substantially harder target and this mission does not duplicate it.
## Difficulty
The obvious argument is: fix a target bound $t=\lambda\sqrt n$, use a Chernoff/Hoeffding bound to show each row fails with probability at most $2e^{-\lambda^2/2}$, union-bound over the $n$ rows, and take a coloring outside the bad event. This works to prove a *single* good coloring exists — but it is not strong enough to survive being iterated to remove the entire uncolored set, because a per-row union bound loses a factor of $n$ that a fixed $\lambda$ cannot always absorb once the active column count $m$ is close to $n$: for the *scaling family* where the row count and the active set shrink together, the naive union bound's failure probability grows *linearly* in $m$, not exponentially, exactly canceling the exponential decay one is trying to exploit. The fix is to bound the *joint* entropy of all $n$ rows' quantizations at once (subadditivity of Shannon entropy), rather than union-bounding row-by-row failure events; this is genuinely a different technique, not a tightening of the same one, and it is the reason the entropy method is presented as its own tool rather than a Chernoff-bound corollary.
## Formalization scope
Matrices are `Fin n → Fin n → ℝ` with an explicit `∀ i j, A i j = 0 ∨ A i j = 1` hypothesis; colorings are represented two ways in this development — `Fin m → Bool` internally (via the platform definition `RSign` converting to $\pm1$) during the entropy/Kleitman argument, and directly as `Fin n → ℝ` constrained to $\{-1,1\}$ pointwise in the goal theorem's statement, matching the usual $\{\pm1\}$-coloring convention. The row-sum shell quantization is the platform definitions `rowSumB`, `shellIdx`, `shellFin` (an integer-valued "round to nearest shell" construction, packaged into a fixed `Fin (2m+3)` type for entropy purposes). The active column set during the outer iteration is tracked as a shrinking `Finset (Fin n)` of the *original* index type throughout, rather than moving between different `Fin m` types round to round, which keeps the induction free of type-level bookkeeping.
Reusable, already-Proved infrastructure this development builds on: `shannonEntropy_pi_le` (subadditivity across independent rows), `shannonEntropy_pigeonhole`, `choose_sum_le_exp_mul_binEntropy`, and `kleitman_diameter`, all already Proved on the platform independent of this mission. The one genuinely open piece — and the mission's standing invitation — is `shannonEntropy_shellFin_le` (Lemma 9): a self-contained Shannon-entropy computation about the `shellFin` quantization that does not depend on anything else in this mission and can be attempted independently.
## Selected references
- J. Spencer, *Six standard deviations suffice*, Trans. Amer. Math. Soc. 289 (1985), 679–706. [DOI](https://doi.org/10.1090/S0002-9947-1985-0784009-0)
- T. Rothvoß, *Discrepancy theory, or: how much balance is possible?*, MIT 18.095 lecture notes. [PDF](https://math.mit.edu/classes/18.095/lect6/notes.pdf)
- J. Matoušek, *Geometric Discrepancy: An Illustrated Guide*, Algorithms and Combinatorics 18, Springer, 1999.
- J. Beck, T. Fiala, *"Integer-making" theorems*, Discrete Appl. Math. 3(1) (1981), 1–8.
7 thms1 active userReviewed
🏆Completed
Captain: Rui Chao
Higher-Dimensional Quantum Hypergraph-Product Codes with Finite RatesResearch Paper
## Motivation
Quantum low-density parity-check codes encode quantum information using sparse
parity constraints. A standard way to construct them is to translate binary
chain complexes into Calderbank--Shor--Steane codes and to combine complexes by
tensor product. Homology identifies the logical operators of the resulting
code, while the smallest Hamming weight of a nontrivial homology class controls
one of its distances. Determining how this distance behaves under a tensor
product is therefore a basic structural question, not merely a parameter
calculation.
Weilei Zeng and Leonid P. Pryadko studied products in which one factor is an
arbitrary finite binary chain complex and the other is the one-complex induced
by a binary matrix. Their paper was published as [“Higher-Dimensional Quantum
Hypergraph-Product Codes with Finite Rates,” *Physical Review Letters* 122,
230501 (2019)](https://doi.org/10.1103/PhysRevLett.122.230501). Its main
distance result is Eq. (13) in the [arXiv version](https://arxiv.org/abs/1810.01519):
for this particular tensor factor, the usual product upper bound is always
exact. The result extends the familiar two-complex setting of quantum
hypergraph-product codes to the local structure occurring in complexes of any
dimension.
## Setting
A **based binary chain complex** consists of finite-dimensional vector spaces
$A_i$ over $\mathbb F_2$, each equipped with a specified coordinate basis, and
linear boundary maps
$$
\cdots\longrightarrow A_{i+1}\xrightarrow{\partial_{i+1}}A_i
\xrightarrow{\partial_i}A_{i-1}\longrightarrow\cdots
$$
such that $\partial_i\partial_{i+1}=0$. Its degree-$i$ homology is
$H_i(\mathcal A)=\ker\partial_i/\operatorname{im}\partial_{i+1}$. The
**homological distance** is measured in the chosen basis:
$$
d_i(\mathcal A)=
\min\{\operatorname{wt}(x):x\in\ker\partial_i\setminus
\operatorname{im}\partial_{i+1}\}.
$$
Following the paper, the minimum of an empty set is $\infty$. Thus
$d_i(\mathcal A)=\infty$ when $H_i(\mathcal A)$ is trivial.
The endpoint convention is also the one stated explicitly after Eq. (1). For
an $m$-complex, $\partial_0:A_0\to\{0\}$ is the zero $0\times n_0$ matrix and
$\partial_{m+1}:\{0\}\to A_m$ is the zero $n_m\times0$ matrix. Consequently
$$
d_0(\mathcal A)=\min\{\operatorname{wt}(x):
x\in A_0\setminus\operatorname{im}\partial_1\}
$$
and
$$
d_m(\mathcal A)=\min\{\operatorname{wt}(x):
0\ne x\in\ker\partial_m\}.
$$
For an $r\times c$ binary matrix $P$, the **one-complex**
$\mathcal K(P)$ has $\mathbb F_2^c$ in degree one,
$\mathbb F_2^r$ in degree zero, and boundary $P$. Its two distances are
$$
d_1(\mathcal K(P))=
\min\{\operatorname{wt}(x):Px=0,\ x\ne0\}
$$
and
$$
d_0(\mathcal K(P))=
\min\{\operatorname{wt}(y):y\notin\operatorname{im}P\}.
$$
In particular, $d_0=1$ unless $P$ has full row rank, in which case
$d_0=\infty$. The degree-$j$ chain group of
$\mathcal A\times\mathcal K(P)$ is
$$
(A_j\otimes\mathbb F_2^r)\oplus
(A_{j-1}\otimes\mathbb F_2^c),
$$
with the standard tensor-product boundary. Over $\mathbb F_2$ the usual sign
in that boundary has no effect.
## Formalization targets
### Tensor-product upper bound for arbitrary complexes
The first milestone is Eq. (11) for two arbitrary finite-length based binary
chain complexes:
$$
d_j(\mathcal A\times\mathcal B)\le
\min_i d_i(\mathcal A)d_{j-i}(\mathcal B).
$$
### Rank-sensitive lower bound
Let $u=\operatorname{rank}P$ and
$\delta=d_1(\mathcal K(P))$. The second milestone is Theorem 1, including
both of its cases:
$$
u<r\Longrightarrow
d_j(\mathcal A\times\mathcal K(P))\ge
\min\!\left(d_j(\mathcal A),d_{j-1}(\mathcal A)\delta\right),
$$
and
$$
u=r\Longrightarrow
d_j(\mathcal A\times\mathcal K(P))\ge
d_{j-1}(\mathcal A)\delta.
$$
### Exact distance with a one-complex
The goal is Eq. (13):
$$
d_j(\mathcal A\times\mathcal K(P))=
\min\!\left(
d_{j-1}(\mathcal A)d_1(\mathcal K(P)),
d_j(\mathcal A)d_0(\mathcal K(P))
\right).
$$
No full-rank hypothesis is imposed on $P$.
## Significance
The equality determines the product distance exactly from four component
distances. General tensor-product arguments immediately provide the upper
bound, but an exact formula requires ruling out lower-weight homology classes
that mix the two direct-sum blocks. Once established, the formula can be
applied repeatedly to tensor products of one-complexes, which is the step used
in the paper to obtain higher-dimensional quantum hypergraph-product code
families and to compute their distances.
For formalization, the mission contributes reusable definitions of finite
based binary chain data, homological distance valued in
$\mathbb N\cup\{\infty\}$, the one-complex of a binary matrix, and the relevant
tensor-product boundary maps. Mathlib contains Hamming weight and general
homological-algebra infrastructure, while QECLean contains a closely related
based length-three homological-code interface. Neither the selected Mathlib
environment nor the inspected QECLean development currently supplies this
rank-sensitive exact distance theorem.
## Difficulty
The central issue is that Hamming weight depends on the chosen bases and is not
preserved by arbitrary homological isomorphisms. A Künneth isomorphism
describes the product homology and readily produces low-weight representatives,
which is enough for the upper bound, but it does not by itself exclude a still
lighter representative obtained by cancellation between the two tensor
blocks. The lower bound must also remain valid at the endpoints of the complex
and in singular cases where one or more homology groups vanish and the relevant
distance is $\infty$.
The theorem cannot be reduced to a dimension calculation. It must reason
about supports and Hamming weights of based representatives while respecting
the quotient by boundaries, and it must cover both $\operatorname{rank}P<r$
and $\operatorname{rank}P=r$.
## Formalization scope
The Lean development works over `ZMod 2`. A finite basis in degree $i$ is
represented by `Fin (dimension i)`, and a chain group is the function space
from that coordinate type to `ZMod 2`. `BasedBinaryChainComplex` stores the
dimension and boundary in every nonnegative degree, the chain condition, and a
finite length above which all dimensions are zero. Thus the first milestone
quantifies over genuinely arbitrary finite lengths for both $\mathcal A$ and
$\mathcal B$, rather than over a local window or a one-complex specialization.
If the stored length is $m$, the zero-dimensional source in degree $m+1$
makes $\partial_{m+1}:\{0\}\to A_m$ the unique zero map, just as the
zero-dimensional target below degree zero makes
$\partial_0:A_0\to\{0\}$ the unique zero map. Hence both singular endpoint
cases in Eqs. (1) and (4) are represented directly.
Distances use `WithTop ℕ`. Their definitions are actual minima of Hamming
weights of nontrivial representatives, with `⊤` produced by the empty-set
case; infinite distance is not an extra hypothesis or a separately hard-coded
branch. Coordinate types may be empty, which covers missing endpoint blocks.
The binary matrix $P$ is represented as a linear map between two finite based
function spaces. Its row and column coordinate types need not be nonempty,
and no injectivity or surjectivity assumption is added.
The degree-$j$ product group is indexed by the disjoint union of all coordinate
products $A_i\times B_{j-i}$ for $0\le i\le j$. Consequently its Hamming norm
is the sum of the weights of all tensor-degree blocks. The product boundary is
the standard signed tensor boundary; its sign disappears over $\mathbb F_2$.
A formal proof verifies that every pair of consecutive product boundaries
composes to zero; the cancellation of the two mixed terms uses characteristic
two. Thus the product distance is taken from an actual chain complex, rather
than from unrelated adjacent linear maps.
A basis-free tensor product or an abstract homology group alone is insufficient
for the target, because either would discard the weight data on which the
statement depends.
The mission does not formalize the asymptotic code-family construction later
in the paper, the transposed cohomological distance, or the CSS-code parameter
translation. Those are natural downstream missions; they should reuse rather
than alter the present based-chain definitions.
## Selected references
- Weilei Zeng and Leonid P. Pryadko, [“Higher-Dimensional Quantum Hypergraph-Product Codes with Finite Rates,”](https://doi.org/10.1103/PhysRevLett.122.230501) *Physical Review Letters* 122, 230501 (2019). [arXiv:1810.01519](https://arxiv.org/abs/1810.01519).
- Benjamin Audoux and Alain Couvreur, [“On Tensor Products of CSS Codes,”](https://arxiv.org/abs/1512.07081) arXiv:1512.07081 (2015), especially Proposition 1.13 and Corollary 2.14 as cited by Zeng--Pryadko.
- Jean-Pierre Tillich and Gilles Zémor, [“Quantum LDPC Codes With Positive Rate and Minimum Distance Proportional to the Square Root of the Blocklength,”](https://doi.org/10.1109/TIT.2013.2292061) *IEEE Transactions on Information Theory* 60 (2014), 1193--1202.
4 thms1 active userReviewed
🏆Completed
Captain: Rui Chao
The Theory of Error-Correcting Codes I: The MacWilliams IdentityTextbook
## Motivation
Error-correcting codes protect information against corruption by adding controlled redundancy. For a code, the distribution of Hamming weights records how its words are spread across possible distances from the zero word and determines basic quantities such as its minimum distance. Linear codes also carry an algebraic duality: every linear code $C$ over a finite field has a dual code $C^\perp$ consisting of the words orthogonal to all words of $C$ under the standard coordinatewise bilinear form.
The MacWilliams identity states that the full Hamming-weight distribution of $C^\perp$ is determined by that of $C$ through one linear change of variables. It is the principal result of Chapter 5 of F. J. MacWilliams and N. J. A. Sloane's [*The Theory of Error-Correcting Codes*](https://books.google.com/books?id=nv6WCJgcjxcC). The binary identity appears there as Theorem 1, while the arbitrary-finite-field Hamming-weight-enumerator identity formalized here is Theorem 13 on p. 146. The surrounding chapter develops related transformations for complete, Lee, exact, joint, and split weight enumerators, nonlinear-code distance distributions, orthogonal arrays, and Krawtchouk polynomials.
This development isolates the arbitrary-$q$ Hamming identity as a first reusable result. Its declarations are designed to support later formalizations drawn from the same chapter and, more broadly, from the book, without enlarging the present target beyond the MacWilliams identity.
## Setting
Let $F$ be a finite field of cardinality $q$, let $\iota$ be a finite coordinate type, and let a **word** be a function $c:\iota\to F$. A **linear code** $C$ is an $F$-linear subspace of the word space. The standard bilinear form is
$$
\langle c,v\rangle=\sum_{i\in\iota}c_i v_i,
$$
and the **dual code** is
$$
C^\perp=\{v:\iota\to F:\langle c,v\rangle=0\text{ for every }c\in C\}.
$$
The **Hamming weight** $\operatorname{wt}(c)$ is the number of coordinates at which $c$ is nonzero. Writing $n=|\iota|$, the homogeneous Hamming weight enumerator of $C$ is the integer-coefficient polynomial
$$
W_C(X,Y)=\sum_{c\in C}X^{n-\operatorname{wt}(c)}Y^{\operatorname{wt}(c)}.
$$
Thus the coefficient of $X^{n-j}Y^j$ is the number of codewords of weight $j$. The Lean development represents this object symbolically in `MvPolynomial (Fin 2) ℤ`; its complex-valued form is obtained by evaluation, so the symbolic and evaluated presentations share a single definition.
## Formalization targets
### Character orthogonality over a code
For a primitive complex additive character $\psi$ of $F$, define
$$
S_C(v)=\sum_{c\in C}\psi(\langle c,v\rangle).
$$
The first milestone states that $S_C(v)=|C|$ when $v\in C^\perp$ and $S_C(v)=0$ otherwise. The binary statement occurs as Problem 13 on p. 134 of MacWilliams--Sloane; Lemmas 9 and 11 on pp. 143--145 give the finite-field character and Fourier formulation.
### Coordinatewise Hamming transform
For every word $c$ and all $X,Y\in\mathbb C$, the second milestone records the full character-weighted transform of the Hamming monomial:
$$
\sum_{v\in F^\iota}
X^{n-\operatorname{wt}(v)}Y^{\operatorname{wt}(v)}
\psi(\langle c,v\rangle)
=
\bigl(X+(q-1)Y\bigr)^{n-\operatorname{wt}(c)}
(X-Y)^{\operatorname{wt}(c)}.
$$
This is a separately reusable formulation of the coordinate calculation appearing in the proofs of Theorems 10 and 13 on pp. 144--146.
### MacWilliams identity
The capstone is the following equality of integer polynomials:
$$
|C|\,W_{C^\perp}(X,Y)
=
W_C\bigl(X+(q-1)Y,\,X-Y\bigr).
$$
This is the denominator-free form of Chapter 5, Theorem 13. After evaluation over a characteristic-zero field it is equivalent to the normalized textbook formula
$$
W_{C^\perp}(X,Y)
=
\frac{1}{|C|}W_C\bigl(X+(q-1)Y,\,X-Y\bigr).
$$
## Significance
The identity turns duality into an enumerative operation: knowing the weight enumerator of a linear code determines the weight enumerator of its dual. It supplies immediate consistency restrictions on possible weight distributions and is a basic input to the study of self-dual codes, Krawtchouk transforms, association schemes, invariant-theoretic properties of enumerators, and linear-programming bounds.
The formalization contributes a small common interface for finite-field words, linear codes, standard duals, and homogeneous Hamming weight enumerators. These declarations are absent from the selected Mathlib environment even though Mathlib already provides Hamming weight, finite-field algebra, additive characters, finite sums, bilinear-form orthogonals, and multivariate polynomials. Establishing the interface and its first central theorem makes those general libraries directly usable for subsequent coding-theory developments.
## Difficulty
The paper statement is short, but its formal representations live in several different layers. Codes are submodules whose elements are subtypes; Hamming weight is a natural-number count; duality is expressed through a bilinear form; character identities take values in $\mathbb C$; and the final result is most reusable as an equality of symbolic polynomials over $\mathbb Z$. The central formalization burden is maintaining exact agreement while transporting the same enumerative data among these layers, including finite instances for codeword subtypes and the natural-number exponents of the homogeneous monomials.
The theorem must also retain the genuine finite-field statement. Replacing the code by an arbitrary finite set, hard-coding the binary field, defining the dual by its expected cardinality, or proving only equality at one chosen pair of evaluation points would not establish the target.
## Formalization scope
The coordinate type is an arbitrary finite type rather than only `Fin n`; its cardinality plays the role of the code length. A word is `CodingTheory.Word F ι := ι → F`, and a linear code is a submodule of this common word space. This representation provides the linear structure and canonical orthogonal dual required here while leaving room for a future nonlinear-code type built from finite sets of the same words.
The polynomial `CodingTheory.hammingWeightEnumeratorPolynomial` has coefficients in $\mathbb Z$ and variables indexed by `Fin 2`. Variable $0$ records zero coordinates and variable $1$ records nonzero coordinates. Its name explicitly identifies the Hamming enumerator, leaving separate stable names available for future complete, Lee, exact, joint, and split weight enumerators. Those later enumerators should be added as new declarations and connected to this one by specialization theorems rather than replacing it.
The standard dual is bilinear, not Hermitian. The code alphabet may be any finite field. The zero code, full code, and empty coordinate type are included; in the empty-coordinate case there is one word of weight zero and the identity reduces to $1=1$. The present mission does not formalize nonlinear codes, complete or other generalized enumerators, orthogonal arrays, or Krawtchouk-polynomial theory. It establishes only the definitions and two character-sum milestones required for the Hamming MacWilliams identity, with a namespace and module boundary intended for reuse by later missions in the textbook series.
## Selected references
- F. J. MacWilliams and N. J. A. Sloane, [*The Theory of Error-Correcting Codes*](https://books.google.com/books?id=nv6WCJgcjxcC), North-Holland, 1977, Chapter 5, pp. 125--154; especially Problem 13 (p. 134), Lemmas 9 and 11 (pp. 143--145), and Theorem 13 (p. 146). [Publisher chapter record](https://doi.org/10.1016/S0924-6509(08)70530-0).
- Violetta Weger, [*Coding Theory*](https://home.cit.tum.de/~wvi/CT.pdf), Technical University of Munich lecture notes, 2025, Theorem 11.2 and Lemma 11.8, pp. 154--159.
- F. J. MacWilliams, [“A Theorem on the Distribution of Weights in a Systematic Code”](https://doi.org/10.1002/j.1538-7305.1963.tb04003.x), *Bell System Technical Journal* 42 (1963), 79--94.
4 thms2 active usersReviewed
🏆Completed
Captain: Elsie66
Shannon's Source Coding TheoremResearch Paper
## 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).