A New Upper Bound on the Binary Deletion Channel Capacity
Özgür Soysal
cs.IT
Sep 11, 2026 · v2
TL;DR
The finite certificate and the entire converse proof of the binary deletion channel capacity bound are formalized end to end in Lean.
Abstract
We prove that the capacity of the binary deletion channel satisfies $C(d)\le (1-d)/4$ for every $13/20\le d<1$. The proof describes the output from right to left, using a six-bit context to assign a description length. We bound the increase in expected description length minus output entropy when one input bit is added. A relative-entropy identity reduces this bound to finitely many linear inequalities. A potential on input windows of length 26 makes the inequalities telescope, giving a bound for every input word. Deletion composition extends the result from $d=13/20$ to all larger deletion probabilities. We also obtain finite-block bounds on mutual information and decoding error, with explicit $O(\log n/n)$ corrections. The finite certificate is checked using exact integer arithmetic, and the proof is formalized end to end in Lean.
Problem
The capacity of the binary deletion channel is hard to analyze because deleted bits and their positions are unobserved. The goal is a converse upper bound on capacity in the high-deletion regime.
Approach
The output is described right-to-left using a six-bit context to assign backward description lengths. The increase in expected description length minus output entropy per added input bit is bounded, and a relative-entropy identity reduces this to finitely many linear inequalities. A potential on input windows of length 26 makes the inequalities telescope, and deletion composition extends the bound to all larger deletion probabilities. The finite certificate is checked using exact integer arithmetic and the whole proof is formalized in Lean.
Results
They prove C(d) ≤ (1−d)/4 for every 13/20 ≤ d < 1, along with finite-block bounds on mutual information and decoding error with explicit O(log n / n) corrections.
