Channel and question
- Input
- A binary input string.
- Output
- The concatenation of each transmitted bit and, independently with probability \(p\), one fair inserted bit.
- Law
- Random insertions occur after transmitted bits; transmitted bits are never deleted or replaced.
- Quantity
- Random-insertion capacity \(C_{\mathrm{ins}}(p)\), measured in bits per transmitted input bit.
Criterion. Vanishing average decoding error under the fixed iid insertion law.
- Inserted bits are independent Bernoulli one-half symbols.
- The decoder observes only the resulting variable-length output string.
- This is not the Gallager replacement-by-two-bits model.
Parameters
- \(p\)
- Probability that one fair bit is inserted after a transmitted bit. Range: \(0\le p\le1\).
Current status
Small-insertion asymptotics are known, but no exact all-p formula is known.
| Result | Relation | Method | Year |
|---|---|---|---|
| Upper | \(C_{\mathrm{ins}}(p)\le1\) | Binary input entropy bound. | 2025 |
| Lower | \(C_{\mathrm{ins}}(p)\ge0\) | One-message code. | 2025 |
Research frontier
Determine capacity or sharper finite-p bounds for this random-after-each-bit insertion model.
Why it remains open. Random output length and synchronization ambiguity create memory in the induced channel.
What would count as progress
- Extend rigorous small-p expansions and finite-block certificates.
Lean formalization
Version 1 · Lean. The one-step finite-support law fixes the insertion convention and excludes the Gallager model.
CapacityAtlas.Channel.binaryInsertionCapacityBoundsstatement
lean/CapacityAtlas/Channels/Insertion.lean — Basic capacity bounds for the explicitly defined random-insertion law.
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
- Busra Tegin and Tolga M. Duman (2025). Capacity Approximations for Insertion Channels with Small Insertion Probabilities. IEEE Transactions on Information Theory. DOI 10.1109/TIT.2025.3644665.
Discussion
Thread key: capacityatlas:binary-insertion-channel