Kraft's inequality (sufficiency), corrected

Proved

SourceCoding.kraft_inequality_sufficiency_v2

by Elsie66 · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

information-theorykraft-mcmillan

Given integer lengths $\ell_i>0$ with $\sum_i D^{-\ell_i}\le 1$ , a uniquely decodable code with exactly those lengths exists.

Formal statement

import Mathlib

namespace SourceCoding

/-- **Kraft's inequality, sufficiency direction** (Kraft, 1949) — corrected, superseding
`SourceCoding.kraft_inequality_sufficiency`, which omitted the hypothesis that lengths are
positive: since a uniquely decodable code can never contain the empty codeword
(`InformationTheory.UniquelyDecodable.epsilon_not_mem`), the original statement is false
whenever some `ℓ i = 0` (e.g. a singleton `ι` with `ℓ = 0` satisfies the Kraft sum bound
vacuously but admits no valid code). If `D = Fintype.card α ≥ 2` and integer lengths
`ℓ : ι → ℕ`, all strictly positive, satisfy the Kraft sum bound `∑ i, D^{-ℓ i} ≤ 1`, there is
an injective assignment `c : ι → List α` of distinct codewords with `(c i).length = ℓ i` for
every `i`, whose codeword set is uniquely decodable. -/
theorem kraft_inequality_sufficiency_v2
    {α : Type} [Fintype α] [Nonempty α] {ι : Type} [Fintype ι]
    (ℓ : ι → ℕ) (hℓ_pos : ∀ i, 0 < ℓ i) (hK : ∑ i, (1 / (Fintype.card α : ℝ)) ^ ℓ i ≤ 1) :
    ∃ c : ι → List α, Function.Injective c ∧ (∀ i, (c i).length = ℓ i) ∧
      InformationTheory.UniquelyDecodable (Set.range c) := by
  sorry

end SourceCoding

Source

C. E. Shannon, "A Mathematical Theory of Communication," Bell System Technical Journal 27 (1948); T. M. Cover & J. A. Thomas, Elements of Information Theory, 2nd ed., Ch. 5.

Read-back

What the Lean code literally says, in plain math · claude-sonnet-5

This declaration is a theorem named kraft_inequality_sufficiency_v2 (its proof is left as sorry, so no actual argument is given). It has an implicit type α : Type equipped with a Fintype α instance (so α is a finite type) and a Nonempty α instance (so α has at least one element). It has a second implicit type ι : Type equipped with a Fintype ι instance (so ι is also a finite type, with no assumption that it is nonempty — ι could be empty). There is an explicit function ℓ : ι → ℕ, assigning a natural number to each element of ι.

Two hypotheses are then assumed. First, hℓ_pos : ∀ i, 0 < ℓ i asserts that for every i : ι, the value ℓ i is strictly positive; equivalently, ℓ i ≥ 1 for every single i, with no exceptions — this rules out ℓ i = 0 for any i. Second, hK : ∑ i, (1 / (Fintype.card α : ℝ)) ^ ℓ i ≤ 1 asserts that the sum, taken over all i : ι, of the real number (1 / |α|)^{ℓ i} (where |α| denotes Fintype.card α, the cardinality of α, cast to a real number) is less than or equal to 1. Note that if ι is empty, this sum is the empty sum, equal to 0, so hK holds vacuously regardless of ℓ (and regardless of hℓ_pos) in that case.

The conclusion asserts the existence of a function c : ι → List α — that is, c assigns to each i : ι a list of elements of α — satisfying three properties jointly (all conjoined under the single existential, with c fixed once and for all across all three conjuncts):

Function.Injective c: c is injective, i.e., for all i, i' : ι, if c i = c i' then i = i' (equivalently, distinct elements of ι are always mapped to distinct lists).
∀ i, (c i).length = ℓ i: for every i : ι, the length of the list c i equals the prescribed value ℓ i exactly (not merely bounded by it).
InformationTheory.UniquelyDecodable (Set.range c): the range (image) of c, as a set of lists, denoted S := Set.range c (i.e., S = {c i : i : ι}), satisfies the predicate UniquelyDecodable, which unfolds exactly as follows: for all finite lists of lists L₁ L₂ : List (List α) such that every element w of L₁ belongs to S and every element w of L₂ belongs to S, if the concatenation (flattening) of L₁ equals the concatenation (flattening) of L₂ (i.e., L₁.flatten = L₂.flatten, concatenating all the constituent lists in order into one long list), then L₁ = L₂ (the two lists-of-lists are equal, i.e., have the same length and the same list at each corresponding position — not merely that their flattenings agree). Universally quantified variables L₁, L₂ here range over all lists of lists of elements of α, with no bound on their length, and the membership conditions and the flatten-equality are hypotheses of an implication whose conclusion is L₁ = L₂.

The conclusion does not assert anything about a "prefix" property (e.g., no codeword being a prefix of another) or any other structural property of the codewords or of c's range beyond these three stated properties: injectivity of c, exact matching of lengths to ℓ, and unique decodability of the range as defined above.

Human review

Endorsed by Shuze Chen · Sep 8, 2026
Endorsed by Elsie66 · Sep 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph