ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-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.

A finite-power Ozarow feedback-region slice

Statement

For $P_{1} = P_{2} = N = 1$ and $ρ = 1 / 2$ , the feedback-region individual bounds are $R_{j} \leq \frac{1}{2} \ln (7 / 4)$ and the sum bound is $R_{1} + R_{2} \leq \ln 2$ . The point $R_{1} = R_{2} = \frac{1}{2} \ln (7 / 4)$ satisfies all three constraints and has sum rate strictly larger than the no-feedback sum bound $\frac{1}{2} \ln 3$ .

Facts & Assumptions

Given: The exact feedback region for independent private messages and the expected average-power model.

[F1]

Ozarow capacity region of the two-user real AWGN MAC with feedback: for a parameter $ρ$ , each individual rate is bounded by $\frac{1}{2} \ln (1 + P_{j} (1 - ρ^{2}) / N)$ and the sum by $\frac{1}{2} \ln (1 + (P_{1} + P_{2} + 2 ρ \sqrt{P_{1} P_{2}}) / N)$ .

[F2]

Two-user real AWGN MAC with perfect causal output feedback: the users have independent private messages, share only causal output feedback, and satisfy separate expected average-power constraints.

[F3]

No-feedback real AWGN MAC capacity region: the no-feedback sum rate is at most $\frac{1}{2} \ln (1 + (P_{1} + P_{2}) / N)$ .

Proof

1.1F1F2algebra

Substituting $P_{1} = P_{2} = N = 1$ and $ρ = 1 / 2$ into [F1] gives the individual bound $\frac{1}{2} \ln (1 + 3 / 4) = \frac{1}{2} \ln (7 / 4)$ and sum bound $\frac{1}{2} \ln (1 + 1 + 1 + 1) = \ln 2$ .

2.1F1F3step 1.1algebra∎

For the selected point, the individual constraints hold with equality and the sum constraint is $\ln (7 / 4) \leq \ln 2$ , true because $7 / 4 \leq 2$ . By [F3], the no-feedback Gaussian sum bound from the same powers is $\frac{1}{2} \ln (1 + 2) = \frac{1}{2} \ln 3$ . The feedback point has larger sum because $\ln (7 / 4) > \frac{1}{2} \ln 3$ is equivalent to $(7 / 4)^{2} > 3$ , i.e. $49 > 48$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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

Amos Lapidoth and Michèle Wigger, On the AWGN MAC with Imperfect Feedback, full-text paper and perfect-feedback discussion (standard reference, not scraped)
Abbas El Gamal and Young-Han Kim, Network Information Theory, Lecture Notes 18, Ozarow AWGN MAC feedback region (standard reference, not scraped)