Channel and question
- Input
- Binary symbols constrained to have no consecutive ones along every output history.
- Output
- An unerased input bit or an erasure marker.
- Law
- The memoryless binary erasure channel has erasure probability epsilon.
- Quantity
- Input-constrained binary erasure channel with feedback capacity \(C\), measured in bits per channel use.
Criterion. Vanishing average block error, with the constraints specified in the model.
- 0 <= epsilon <= 1. Erasures are independent across time.
- The encoder sees strictly past outputs through noiseless feedback.
- The input constraint holds for every message and output history.
Current status
\[C_{\rm fb}=\max_{0\le p\le1/2}\frac{(1-\varepsilon)h_2(p)}{1+(1-\varepsilon)p}\]
| Result | Relation | Method | Year |
|---|---|---|---|
| Exact | \(C_{\rm fb}=\max_{0\le p\le1/2}\frac{(1-\varepsilon)h_2(p)}{1+(1-\varepsilon)p}\) | Dynamic programming converse and an explicit constrained feedback code. | 2015 |
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.
Claims
- Exact feedback capacity of the binary (1,infinity) input-constrained erasure channel.
operational-capacity· exact capacity · solved · Formally stated · v2
Lean declarations (1)
CapacityAtlas.Claims.constrainedBECclaim · operational-capacity
lean/CapacityAtlas/Claims/ConstrainedBEC.lean — Exact feedback capacity of the binary (1,infinity) input-constrained erasure channel.
References
- Oron Sabag, Haim H. Permuter, and Navin Kashyap (2015). The Feedback Capacity of the (1,infinity)-RLL Input-Constrained Erasure Channel. arXiv preprint.