ExampleConstruction: Literature-sourcedVerification: AI-generatedPipeline-generatedprecheck pending

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.

Binary Hamming rate-distortion curve at p equals one quarter

Statement

For a Bernoulli- $1 / 4$ source with Hamming distortion, the rates at $D = 0, 1 / 8, 1 / 4$ are respectively $h_{2} (1 / 4)$ , $h_{2} (1 / 4) - h_{2} (1 / 8)$ , and $0$ . At $D = 1 / 8$ , the backward test-channel reproduction mass is $P (\hat{X} = 1) = 1 / 6$ ; at $D = 1 / 4$ , a constant zero reproduction attains rate zero. The rate tends continuously to zero as $D ↑ 1 / 4$ .

Facts & Assumptions

Given: A Bernoulli source with parameter $p = 1 / 4$ , binary Hamming distortion, and the rate function of the binary theorem.

[F1]

Binary Hamming rate-distortion function: for $0 \leq D \leq \min (p, 1 - p)$ , $R (D) = h_{2} (p) - h_{2} (D)$ ; above that threshold the rate is zero.

Proof

1.1F1givenalgebra

Here $p_{0} = 1 / 4$ . Substitution in [F1] gives $R (0) = h_{2} (1 / 4) - h_{2} (0) = h_{2} (1 / 4)$ and $R (1 / 8) = h_{2} (1 / 4) - h_{2} (1 / 8)$ . At $D = 1 / 4$ , the threshold branch gives zero; the constant reconstruction zero has distortion $P (X = 1) = 1 / 4$ and carries no information.

2.1step 1.1givenconstructalgebra

For $D \in {0, 1 / 8}$ , put $q = (1 / 4 - D) / (1 - 2 D)$ , which equals $1 / 4$ or $1 / 6$ , respectively. Construct independent $Y \sim Bernoulli (q)$ and $E \sim Bernoulli (D)$ on their finite product space and set $X = Y \oplus E$ . Then $P (X = 1) = D + q (1 - 2 D) = 1 / 4$ and $P (X \neq Y) = D$ . Given either value of $Y$ , the two conditional source masses are $D$ and $1 - D$ in some order. Thus the finite joint-information sum is $\sum_{x, y} P (X = x, Y = y) \log_{2} (P (X = x ∣ Y = y) / P (X = x)) = h_{2} (1 / 4) - h_{2} (D)$ , with zero terms omitted. These channels attain the rates in step 1.1; in particular the backward test channel at $D = 1 / 8$ has reproduction mass $P (Y = 1) = 1 / 6$ .

3.1F1step 1.1givenalgebra∎

The function $h_{2}$ is continuous on $[0, 1]$ under $0 \log_{2} 0 = 0$ , so $\lim_{D ↑ 1 / 4} [h_{2} (1 / 4) - h_{2} (D)] = 0 = R (1 / 4)$ . This verifies the stated endpoint continuity.

Depends on

Binary Hamming rate-distortion function

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

6 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

MIT OpenCourseWare 6.441, Chapter 25: Evaluating R(D) (standard reference, not scraped)