关于双重对称二进制源二进制信道的三个猜想
Three Conjectures on Binary Channels for the Doubly Symmetric Binary Source
中文总结 AI 辅助
本文解决了关于双重对称二进制源在二进制信道下的三个猜想，包括平均BSC猜想和双侧信息瓶颈的极值问题，并在Lean 4中完成了形式化验证。
中文摘要 AI 辅助
我们解决了关于交叉概率为 $p$ 的双重对称二进制源 $(X,Y)$ 的三个猜想。考虑马尔可夫链 $U - X - Y - V$，其中 $U,V$ 为二进制，并设 $\nathcal{A}$ 为可通过任意二进制信道 $X\to U$, $Y\to V$ 达到的速率三元组 $(I(U;V),I(U;X),I(Y;V))$ 的集合，$\nathcal{B}$ 为可通过二进制对称信道达到的子集。平均 BSC 猜想，即 Pichler, Piantanida 和 Matz (2022) 的猜想 5.2，断言 $\noperatorname{conv}\nathcal{A}=\noperatorname{conv}\nathcal{B}$。我们对每个 $p\in[0,1]$ 证明了该猜想。Dikshtein, Ordentlich 和 Shamai (2022) 的两个猜想涉及 $p=0$ 时的双侧信息瓶颈，此时 $Y=X$，两个信道看到相同的源：他们的猜想 1 确定了在给定速率 $I(U;X)$ 和 $I(Y;V)$ 下 $I(U;V)$ 的精确最大值，他们的猜想 2 确定了精确最小值。我们证明了对于二进制 $U,V$ 这两个猜想：两个极值由同一对 Z/S 信道达到，最大值时方向相反，最小值时方向相同。证明过程借助了大量 AI 辅助，所有三个定理均在 Lean 4 中结合 Mathlib 进行了形式化验证，仅依赖于标准公理。相关代码可在 https://github.com/g-pichler/bsc-averaging 获取。Dikshtein, Ordentlich 和 Shamai (2022) 猜想 1 的证明包含三个经认证的计算：一个多项式界、一个区间扫描和一个多项式正性证书，所有这些都在 Lean 中进行了检查。
英文摘要
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.
