Özgür Soysal

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.