Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablePipeline-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.

No-feedback independent-private-message DM-MAC code

Definition

For a DM-MAC as in Two-user discrete memoryless multiple-access channel, fix integers n≥1 and M1,M2≥1, and write [m]={1,…,m}. A length-n no-feedback code consists of independent uniform private messages Mj∈[Mj], separate deterministic message-only encoders fj:[Mj]→Xjn, and one joint decoder g:Yn→[M1]×[M2]. The average joint error is Pr⁡[g(Yn)≠(M1,M2)]; Rj=n−1ln⁡Mj nats/use. A pair is achievable if a sequence with n→∞ has error tending to zero and limiting lower rates at least the pair; the capacity region is the closure. In particular, independent messages and separate encoders give X1i⊥X2i at every coordinate 1≤i≤n.

Facts & Assumptions

Given: A DM-MAC, an integer n≥1, and two finite nonempty message sets of sizes M1,M2≥1.

[F1]

Two-user discrete memoryless multiple-access channel: the conditional block law is ∏iW(yi∣x1i,x2i).

Proof

1.1givenF1algebra

The independent uniform messages and the two deterministic maps induce separate input words; combining these with [F1] defines a probability law on the finite set of message, input and output tuples.

2.1givenstep 1.1algebra∎

Since each input coordinate is a function only of its own independent message, X1i and X2i are independent for 1≤i≤n. Because n≥1 and Mj≥1, each rate n−1ln⁡Mj is a finite nonnegative real number. The decoder event belongs to the finite probability space in step 1.1, so its probability is well-defined.

Depends on

Used by

Dependency tree · two levels

2 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