Proof settles three key conjectures about binary communication channels
Three Conjectures on Binary Channels for the Doubly Symmetric Binary Source
Information Theory
Summary
This paper resolves three long-standing questions about how information moves between two related binary signals through simple channels. The authors look at how pairs of processed signals can share, limit, or maximize information under given conditions. They prove that complicated scenarios can be reduced to simpler ones without loss, and show exactly which simple processing methods achieve the best and worst information sharing. Their proofs rely on computer-assisted methods and formal verification for full mathematical certainty.
What this means in practice
- •For communication system designers: Optimize encoding and decoding schemes for binary data transmission knowing the fundamental limits rigorously proven for binary symmetric channels.
- •For data compression engineers: Design binary compression methods with precise guarantees on information bottlenecks and channel behavior to improve efficiency under symmetric noise conditions.
A theory result. No direct application yet.
Authors
Georg Pichler
Abstract
We settle three conjectures concerning a doubly symmetric binary source $(X,Y)$ with crossover $p$. Consider Markov chains $U - X - Y - V$ with $U,V$ binary, and let $\mathcal{A}$ be the set of rate triples $(I(U;V),I(U;X),I(Y;V))$ attainable with arbitrary binary channels $X\to U$, $Y\to V$, and $\mathcal{B}$ the subset attainable with binary symmetric channels. The averaged BSC conjecture, Conjecture 5.2 of Pichler, Piantanida and Matz (2022), asserts $\operatorname{conv}\mathcal{A}=\operatorname{conv}\mathcal{B}$. We prove this for every $p\in[0,1]$. Two conjectures of Dikshtein, Ordentlich and Shamai (2022) concern the double-sided information bottleneck at $p=0$, where $Y=X$ and the two channels see the same source: their Conjecture 1 identifies the exact maximum of $I(U;V)$ at prescribed rates $I(U;X)$ and $I(Y;V)$, and their Conjecture 2 the exact minimum. We prove both for binary $U,V$: the two extrema are attained by the same pair of Z/S-channels, in opposite orientation for the maximum and in the same orientation for the minimum. The proofs were found with substantial AI assistance, and all three theorems are formalised in Lean 4 with Mathlib, depending only on the standard axioms. The development is available at https://github.com/g-pichler/bsc-averaging . The proof of Conjecture 1 of Dikshtein, Ordentlich and Shamai (2022) contains three certified computations, a polynomial bound, an interval sweep and a polynomial positivity certificate, all of which are checked in Lean.