Channel and question
- Input
- Independent uniform messages \(M_i\) originate at specified nodes \(s_i\) of a finite directed acyclic network \(G=(V,E)\).
- Output
- Every sink \(t\in T\) decodes the entire message tuple from its incoming packets and any messages generated locally.
- Law
- Edge \(e\) transmits exactly \(\lfloor n c_e\rfloor\) noiseless bits in an n-use code, for a fixed nonnegative real capacity \(c_e\).
- Quantity
- Multisource multicast capacity region \(\mathcal C\), measured in bits per network use.
Criterion. Nonnegative rate vectors attainable at every sufficiently large blocklength, with a common vanishing rate tolerance and joint average block error.
- The sink set is nonempty. Multiple messages may originate at the same node, including a sink.
- Nodes process packets in topological order using deterministic functions of local messages and incoming packets.
- Packet lengths and schedules are fixed and carry no information.
- The probability that any sink decodes any message incorrectly vanishes.
Current status
\[\mathcal C=\{R\ge0:\ \sum_{i:s_i\in U}R_i\le\sum_{e\in\delta^+(U)}c_e\quad\forall t\in T,\ U\subseteq V\setminus\{t\}\}\]
Here \(\delta^+(U)\) contains edges leaving U. Zero-error linear codes over finite binary extension fields achieve the whole region in the limit, including its boundary.
| Result | Relation | Method | Year |
|---|---|---|---|
| Lower | \(\{R\ge0:\ \sum_{i:s_i\in U}R_i\le\sum_{e\in\delta^+(U)}c_e\ \forall t\in T,\ U\subseteq V\setminus\{t\}\}\subseteq\mathcal C\) | Linear network coding for independent sources, with finite-field symbols represented by binary packets. | 2006 |
| Upper | \(\mathcal C\subseteq\{R\ge0:\ \sum_{i:s_i\in U}R_i\le\sum_{e\in\delta^+(U)}c_e\ \forall t\in T,\ U\subseteq V\setminus\{t\}\}\) | Cut-set converse conditioned on the messages originating outside the cut. | 2006 |
Formal verification
Lean coverageFormally stated
The local proof constructs zero-error codes for the inner bound and proves the converse for arbitrary deterministic local codes. Real link capacities, zero rates, and sources located at sinks are included.
Claims
- The operational multisource multicast region equals the nonnegative cut-constraint region.
capacity-region· exact capacity · solved · Formally proved · v1
Lean declarations (3)
CapacityAtlas.Multisource.Network.Codedefinition
lean/CapacityAtlasForMathlib/Network/Multisource/Basic.lean — Independent message sets and fixed binary packets with local encoder and decoder constraints.CapacityAtlas.Multisource.Network.capacityRegiondefinition
lean/CapacityAtlasForMathlib/Network/Multisource/Basic.lean — Vanishing joint average error with a shared rate tolerance.CapacityAtlas.Claims.multisourceMulticastCapacityclaim · capacity-region
lean/CapacityAtlas/Claims/MultisourceMulticast.lean — Locally proved equality of operational and cut-constraint regions.
References
- Tracey Ho, Muriel Médard, Ralf Koetter, David R. Karger, Michelle Effros, Jun Shi, and Ben Leong (2006). A Random Linear Network Coding Approach to Multicast. IEEE Transactions on Information Theory. DOI 10.1109/TIT.2006.881746.