Pipeline-generated

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.

✓ 2 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Point-to-Point Source–Channel Separation — Examples

1 · Prerequisites

2 · Summary

These examples compute a strict entropy-capacity budget for a finite IID source and a BSC, then show the limit of that asymptotic result. A full-support noisy channel has positive error at every finite blocklength for any nontrivial source, even when the asymptotic separation inequality is strict. The examples distinguish asymptotic reliability from finite-block zero-error performance.

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

A finite-alphabet source-channel rate budget

Example

Take an IID Bernoulli source with $P_{S} (1) = 1 / 4$ and a binary symmetric channel with crossover probability $1 / 4$ . Use five channel symbols per source symbol. Both the source entropy and the channel capacity are in nats; this example computes the strict asymptotic lossless separation margin exactly.

Facts & Assumptions

Given: A finite IID source, a finite DMC, and the formulas for finite mutual information and entropy.

[A1]

$S_{i}$ are IID Bernoulli $(1 / 4)$ , and $W$ is the BSC with input and output alphabets ${0, 1}$ and crossover probability $1 / 4$ .

[A2]

Write $h (q) : = - q \ln q - (1 - q) \ln (1 - q)$ for the entropy in nats of a Bernoulli $(q)$ variable, with $0 \ln 0 : = 0$ .

[F1]

Finite discrete memoryless channels: the BSC is a finite DMC; Single-letter information capacity of a finite DMC defines $C (W) = \sup_{P_{X}} I (X; Y)$ in nats per use.

[F2]

Finite mutual information, Finite conditional entropy, and Finite entropy and mutual-information chain rules: $I (X; Y) = H (Y) - H (Y ∣ X)$ for finite alphabets.

[F3]

Finite distributions, entropy, divergence, and stochastic matrices: the entropy of a binary probability vector $(q, 1 - q)$ is $- q \ln q - (1 - q) \ln (1 - q)$ , with $0 \ln 0 = 0$ .

[F4]

Finite KL divergence is nonnegative with equality exactly at equal laws: $D (Bern (q) ∥ Bern (1 / 2)) = \ln 2 - h (q) \geq 0$ .

[F5]

Operational capacity formula for a finite DMC: the operational DMC capacity equals the single-letter information capacity $C (W)$ .

[F6]

Lossless separation for finite IID sources and finite DMCs: if source entropy in nats is strictly below $ρ C (W)$ , reliable transmission is achievable asymptotically.

Verification

1.1A1A2F2F3givenalgebra

For an input $X \sim Bern (r)$ , the BSC output is Bernoulli with parameter $q = 1 / 4 + r / 2$ , while $H (Y ∣ X) = h (1 / 4)$ . By [F2], [F3], and the notation in [A2], $I (X; Y) = h (q) - h (1 / 4)$ .

2.1A1A2F1F4F5step 1.1algebra

By [F4], $h (q) \leq \ln 2$ , with equality at $q = 1 / 2$ , which is attained by $r = 1 / 2$ . Hence [F5] gives $C (W) = \ln 2 - h (1 / 4) = \frac{3}{4} \ln 3 - \ln 2$ , with $C (W)$ interpreted as in [F1]. The source entropy is $H (P_{S}) = h (1 / 4) = 2 \ln 2 - \frac{3}{4} \ln 3$ .

3.1A1F6step 2.1algebra∎

At $ρ = 5$ , the gap is $5 C (W) - H (P_{S}) = \frac{9}{2} \ln 3 - 7 \ln 2 > 0$ , because $3^{9} = 19683 > 16384 = 2^{14}$ and the natural logarithm is increasing. Therefore the strict hypothesis of [F6] holds, so asymptotically reliable lossless transmission is achievable at this ratio.

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passOpen item page →

Strict asymptotic separation need not give zero finite-block error

Statement refuted

For every finite IID source and finite DMC, if $H (P_{S}) < ρ C (W)$ , then every finite blocklength ratio $n / k = ρ$ admits a deterministic joint code with zero block error.

Facts & Assumptions

Given: A uniform binary IID source, a BSC with crossover probability $1 / 4$ , channel blocklength $n_{k} = 6 k$ , and a deterministic joint code as in Finite-alphabet point-to-point joint source-channel codes.

[A1]

Every word $s^{k} \in {0, 1}^{k}$ has source probability $2^{- k} > 0$ .

[A2]

In this verification, $H (P_{S}) : = - \sum_{s} P_{S} (s) \ln P_{S} (s)$ and $h (q) : = - q \ln q - (1 - q) \ln (1 - q)$ , with $0 \ln 0 : = 0$ .

[F1]

Finite discrete memoryless channels: for the BSC with crossover probability $1 / 4$ , each coordinate transition probability is either $1 / 4$ or $3 / 4$ , so every output word has positive probability under every input word.

[F2]

Single-letter information capacity of a finite DMC and Operational capacity formula for a finite DMC: $C (W) = \max_{P_{X}} I (X; Y)$ in nats per use.

[F3]

Finite conditional entropy, Finite mutual information, and Finite entropy and mutual-information chain rules: $I (X; Y) = H (Y) - H (Y ∣ X)$ .

[F4]

Finite distributions, entropy, divergence, and stochastic matrices and Finite KL divergence is nonnegative with equality exactly at equal laws: for binary $q$ , $h (q) \leq \ln 2$ , with equality at $q = 1 / 2$ .

[F5]

Lossless separation for finite IID sources and finite DMCs: a strict entropy-capacity gap ensures reliable transmission by a sequence of codes, asymptotically.

Counterexample

1.1A1A2F2F3F4givenalgebra

The source entropy is $H (P_{S}) = \ln 2$ . For a BSC with crossover $1 / 4$ and input $X \sim Bern (r)$ , the output parameter is $q = 1 / 4 + r / 2$ , and [F3] gives $I (X; Y) = h (q) - h (1 / 4)$ . By [F4], the maximum is at $r = 1 / 2$ , so $C (W) = \ln 2 - h (1 / 4) = \frac{3}{4} \ln 3 - \ln 2$ .

1.2A1F1givenchoosealgebra

Fix any $k \geq 1$ , any deterministic encoder $f_{k} : {0, 1}^{k} \to {0, 1}^{6 k}$ , and decoder $g_{k} : {0, 1}^{6 k} \to {0, 1}^{k}$ . Choose any output word $y_{0}$ and then a source word $s^{k} \neq g_{k} (y_{0})$ , which exists because $∣ {0, 1}^{k} ∣ \geq 2$ . By [A1] and [F1], $\Pr [S^{k} = s^{k}, Y^{6 k} = y_{0}] = 2^{- k} W^{6 k} (y_{0} ∣ f_{k} (s^{k})) > 0$ . On this event the decoder is wrong, so the block-error probability is positive for every finite code.

2.1A1A2F5step 1.1algebra

Hence $6 C (W) - H (P_{S}) = \frac{9}{2} \ln 3 - 7 \ln 2 > 0$ , since $3^{9} = 19683 > 16384 = 2^{14}$ . The asymptotic threshold is strict, so [F5] gives a reliable code sequence at ratio six.

3.1F5step 2.1step 1.2algebra∎

The strict asymptotic threshold in step 2.1 therefore cannot imply a zero-error code at each finite blocklength ratio. This refutes the statement while leaving the asymptotic separation conclusion intact.

Point-to-Point Source–Channel Separation — Examples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

A finite-alphabet source-channel rate budget

Example

Facts & Assumptions

Verification

Strict asymptotic separation need not give zero finite-block error

Statement refuted

Facts & Assumptions

Counterexample

Sources