Channel and question
- Input
- A binary symbol \(X\).
- Output
- Binary outputs \(Y_1,Y_2\).
- Law
- For \(X=0\), \(Y_1=0\) and \(Y_2\) is fair; for \(X=1\), \(Y_1\) is fair and \(Y_2=1\).
- Quantity
- Private-message capacity region \(\mathcal C_{\mathrm{BSSC}}\), measured in ordered pairs of bits per channel use.
Criterion. Closure of achievable private-message rate pairs.
- Independent private messages are sent to the receivers.
- Average probability that either receiver errs vanishes.
Current status
Equality of the named inner and outer descriptions is the canonical formal target.
| Result | Relation | Method | Year |
|---|---|---|---|
| Inner Region | \(\mathcal R_{\mathrm{Marton}}\subseteq\mathcal C_{\mathrm{BSSC}}\) | Marton coding specialized to binary input and symmetric outputs. | 1979 |
| Outer Region | \(\mathcal C_{\mathrm{BSSC}}\subseteq\mathcal R_{\mathrm{UV}}\) | Auxiliary-variable broadcast outer bound. | 2007 |
Research frontier
Close the gap between the best Marton-type inner region and UV-type outer region for the fixed BSSC law.
Why it remains open. Known auxiliary-variable optimizations do not coincide on all supporting hyperplanes.
What would count as progress
- Certify a strict separating rate pair or prove the two optimized descriptions equal.
Lean formalization
Version 1 · Lean. The transition law is concrete; the proposition interface fixes the inner-versus-outer equality target without supplying a proof.
CapacityAtlas.Channel.binarySkewSymmetricBroadcastCapacityStatementstatement
lean/CapacityAtlas/Channels/Broadcast.lean — Equality target for the Marton inner and UV outer regions.
No external Lean proof is registered. Proofs longer than roughly 50 lines or requiring problem-specific infrastructure should live in a dedicated repository and link back to this statement version.
References
- Katalin Marton (1979). A Coding Theorem for the Discrete Memoryless Broadcast Channel. IEEE Transactions on Information Theory. DOI 10.1109/TIT.1979.1056046.
- Chandra Nair and Abbas El Gamal (2007). An Outer Bound to the Capacity Region of the Broadcast Channel. IEEE Transactions on Information Theory. DOI 10.1109/TIT.2006.887492.
- Yanlin Geng, Chandra Nair, Shlomo Shamai, and Zizhou Vincent Wang (2010). On Broadcast Channels with Binary Inputs and Symmetric Outputs. arXiv preprint.
Discussion
Thread key: capacityatlas:binary-skew-symmetric-broadcast-channel