CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Huffman expected length is within one bit of entropy

Statement

Let $C_{H}$ be the code returned by Deterministic binary Huffman coding for a finite full-support source $p$ . If $m \geq 2$ , then $H_{2} (p) \leq L_{p} (C_{H}) < H_{2} (p) + 1.$ If $m = 1$ , then $H_{2} (p) = 0$ and $L_{p} (C_{H}) = 1$ .

Facts & Assumptions

Given: A finite full-support source $p$ and its deterministic Huffman code $C_{H}$ .

[F1]

The deterministic Huffman code is prefix-optimal: The deterministic Huffman procedure returns a binary prefix code minimizing $L_{p} (C)$ among all binary prefix codes on the same alphabet.

[F2]

Every finite binary prefix code is uniquely decodable: Every binary prefix code is uniquely decodable.

[F3]

Shannon bounds for finite binary codes: Every finite binary uniquely decodable code has expected length at least $H_{2} (p)$ , and for $m \geq 2$ a binary prefix code exists with expected length strictly less than $H_{2} (p) + 1$ .

[F4]

Base-two entropy of a finite source: $H_{2} (p) = - \sum_{i} p_{i} \log_{2} p_{i}$ .

[F5]

Deterministic binary Huffman coding: For $m = 1$ , the algorithm returns $C_{H} (1) = 0$ .

[F6]

Information units and logarithm-base convention: $\log_{2} t = \ln t / \ln 2$ with $\ln 2 > 0$ .

[F7]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm: $\ln 1 = 0$ .

Proof

1.1F1F2F3given

Suppose $m \geq 2$ . By [F1], $C_{H}$ is a prefix code; [F2] makes it uniquely decodable. Apply the lower bound in [F3] to obtain $H_{2} (p) \leq L_{p} (C_{H})$ .

2.1F1F3step 1.1algebra

The upper-bound construction in [F3] is a prefix code on the same source. Since $C_{H}$ minimizes expected length among prefix codes by [F1], its length is no larger than that constructed code, hence $L_{p} (C_{H}) < H_{2} (p) + 1$ .

3.1F4F5F6F7givenalgebra∎

If $m = 1$ , then $p_{1} = 1$ by the source definition and $H_{2} (p) = 0$ by [F4], [F6], and [F7]. The returned codeword has length one by [F5], so $L_{p} (C_{H}) = 1$ .

Depends on

Used by

Huffman tree for a dyadic three-symbol source Example

Dependency tree · two levels

23 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Stanford EE376A, Information Theory Course Notes, Chapter 4: Lossless Compression (standard reference, not scraped)
MIT OpenCourseWare 6.450, Memory-less sources, prefix free codes, and entropy (standard reference, not scraped)