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.

A degraded binary erasure wiretap channel

Statement

Bob observes a binary erasure channel (BEC) with input alphabet ${0, 1}$ , output alphabet ${0, 1, e}$ , and erasure probability $1 / 4$ . Eve observes Bob's output after independently erasing each surviving bit with probability $1 / 3$ , while an erasure remains an erasure. This is a finite degraded wiretap channel. Its strong- and weak-secrecy capacities under average or maximal error are all $\ln 2 / 4$ nats per use. Define $h (p) : = - p \ln p - (1 - p) \ln (1 - p)$ with $0 \ln 0 : = 0$ . For Bernoulli- $p$ input the single-letter difference is $h (p) / 4$ , which is zero at $p = 0, 1$ and maximal at $p = 1 / 2$ .

Facts & Assumptions

Given: Bob's channel is BEC $(1 / 4)$ and Eve's output is obtained by an independent BEC $(1 / 3)$ erasure of Bob's non-erased symbols.

[F1]

Finite degraded wiretap channel: a degraded wiretap channel has factorization $W (y, z ∣ x) = W_{Y} (y ∣ x) V (z ∣ y)$ .

[F2]

Secrecy capacity of a finite degraded wiretap channel: all four operational secrecy capacities equal $\max_{P_{X}} [I (X; Y) - I (X; Z)]$ .

[F3]

Finite mutual information: mutual information is finite joint-law KL in nats.

[F4]

Finite entropy and mutual-information chain rules: finite mutual information satisfies $I (X; Y) = H (X) - H (X ∣ Y)$ and the entropy chain rule.

[F5]

Finite KL divergence is nonnegative with equality exactly at equal laws: finite KL divergence is nonnegative and vanishes exactly for equal laws.

[F6]

Finite distributions, entropy, divergence, and stochastic matrices: $h (p) = - p \ln p - (1 - p) \ln (1 - p)$ with zero terms omitted, and the uniform binary entropy is $\ln 2$ .

Proof

1.1F1givenconstructalgebra

Define $V (e ∣ e) = 1$ , $V (y ∣ y) = 2 / 3$ , and $V (e ∣ y) = 1 / 3$ for $y \in {0, 1}$ , with all other entries zero. Each row sums to one. Given input $x$ , the joint probabilities are $W_{Y} (e ∣ x) V (e ∣ e) = 1 / 4$ for $(Y, Z) = (e, e)$ , $W_{Y} (x ∣ x) V (x ∣ x) = (3 / 4) (2 / 3) = 1 / 2$ for $(x, x)$ , and $W_{Y} (x ∣ x) V (e ∣ x) = (3 / 4) (1 / 3) = 1 / 4$ for $(x, e)$ ; all other pairs have probability zero. Thus $W (y, z ∣ x) = W_{Y} (y ∣ x) V (z ∣ y)$ and [F1] applies.

2.1F3F4F6step 1.1algebra

For a Bernoulli- $p$ input, a BEC with erasure probability $ϵ$ has $H (X ∣ Y) = ϵ h (p)$ : on a received bit the conditional entropy is zero, and on erasure it is $H (X) = h (p)$ . Since $I (X; Y) = H (X) - H (X ∣ Y)$ by [F4], Bob's mutual information is $(3 / 4) h (p)$ and Eve's is $(1 / 2) h (p)$ . Their difference is $h (p) / 4$ .

3.1F2F5F6step 2.1algebra∎

For every $p \in [0, 1]$ , compare the Bernoulli- $p$ law with the uniform binary law. By [F5], $0 \leq D ((p, 1 - p) ∥ (1 / 2, 1 / 2)) = \ln 2 - h (p),$ with equality exactly when $p = 1 / 2$ . At $p = 0$ and $p = 1$ , the zero-term convention in [F6] gives $h (p) = 0$ . Thus $h (p) / 4$ has maximum $\ln 2 / 4$ at the fair input and vanishes at both deterministic endpoints. The capacity claim follows from [F2] and step 2.1.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

21 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

Abbas El Gamal and Young-Han Kim, Network Information Theory, arXiv:1001.3404v3 (standard reference, not scraped)
Paul Cuff, Princeton ELE 538: Information Theoretic Security, Lecture 11 (standard reference, not scraped)