Channel and question
- Input
- \(X^n\in\{0,1\}^n\)
- Output
- A random subsequence of the input, without deletion markers.
- Law
- Each bit is retained independently with probability \(1-d\); surviving bits keep their order.
- Quantity
- Shannon capacity \(C_{\mathrm{del}}(d)\), measured in bits per input bit.
Criterion. Average-error operational capacity.
- Neither terminal observes the deletion pattern.
- Average decoding error vanishes.
Parameters
- \(d\)
- Independent deletion probability. Range: \(0<d<1\).
Current status
\[0.1221(1-d)<C_{\mathrm{del}}(d)\le0.3578(1-d)\]
Conditions. The displayed pair is a simple uniform high-deletion summary; the upper bound shown holds for \(d\ge0.64\).
Pointwise numerical envelopes can be stronger.
| Result | Relation | Method | Year |
|---|---|---|---|
| Lower | \(C_{\mathrm{del}}(d)>0.1221(1-d)\) | Optimized run-length input distributions. | 2023 |
| Upper | \(C_{\mathrm{del}}(d)\le0.3578(1-d)\)\(d\ge0.64\) | Parallelized finite-block Blahut-Arimoto upper bounds. | 2026 |
Open question
Determine \(C_{\mathrm{del}}(d)\), even at \(d=1/2\).
Deletions destroy alignment, and finite-letter optimizations grow exponentially without a known single-letter reduction.
Research directions
- Improve a certified pointwise bound.
- Prove structure of capacity-achieving stationary inputs.
Formal verification
Lean coverageFormally stated
Concrete operational definitions and admitted research statements are present. Existing proofs are preserved. New statements require mathematical review and proof completion. The converse coefficient applies only for deletion probability at least 16/25. Numerical certificates still need to be supplied by the future proof.
Claims
- Published deletion bounds in bits per INPUT bit, with the high-deletion restriction explicit.
published-capacity-bounds· capacity bounds · solved · Formally stated · v1 - Independently tracked run length achievability.
run-length-achievability· achievability · solved · Formally stated · v1 - Independently tracked high deletion converse.
high-deletion-converse· converse · solved · Formally stated · v1
Lean declarations (3)
CapacityAtlas.Claims.deletionBoundsclaim · published-capacity-bounds
lean/CapacityAtlas/Claims/DeletionBounds.lean — Published deletion bounds in bits per INPUT bit, with the high-deletion restriction explicit.CapacityAtlas.Claims.deletionRunLengthclaim · run-length-achievability
lean/CapacityAtlas/Claims/DeletionBounds.lean — Independently tracked run length achievability.CapacityAtlas.Claims.deletionHighConverseclaim · high-deletion-converse
lean/CapacityAtlas/Claims/DeletionBounds.lean — Independently tracked high deletion converse.
References
- Ittai Rubinstein and Roni Con (2023). Improved Upper and Lower Bounds on the Capacity of the Binary Deletion Channel. arXiv preprint.
- Martim Pinto and João Ribeiro (2026). Improved Capacity Upper Bounds for the Deletion Channel using a Parallelized Blahut-Arimoto Algorithm. arXiv preprint; presented at ISIT 2026.