发表机构
The Chinese University of Hong Kong; Google; University of Southern California; Carnegie Mellon University（香港中文大学; 谷歌; 南加州大学; 卡内基梅隆大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文通过计算机辅助方法证明了Courtade--Kumar猜想，即布尔函数经二元对称信道后的互信息不超过1减二元熵，独裁函数达到等号，核心是微分方程与Bellman不等式。
AI 中文摘要
设$X$在$\{-1,1\}^n$上均匀分布，设$Y$通过将其坐标独立地通过交叉概率为$p$的二元对称信道而获得，并设$g:\{-1,1\}^n\to\{0,1\}$为一个布尔函数。我们给出了Courtade--Kumar猜想$I(g(X);Y)\le1-H_2(p)$的一个计算机辅助证明，其中$H_2$是二元熵，且等号由独裁函数取得。本工作建立在微分方程方法之上，该方法本身是网络信息论中辅助接收者方法的一种极限形式，使用连续统的退化接收者。证明从局部不等式推进到熵产生的维无关界。沿布尔噪声半群的微分将熵产生表示为边成本的平均值。因此，关键估计是一个具有两个均值约束和两个熵约束的无限制Bellman不等式，允许边变量的任意耦合。本文及其补充材料提供了证明和计算验证记录。文档篇幅较长，因为它旨在完全自包含，从第一原理推导所有证明并复现所引用结果的证明。支持计算机辅助部分证明的补充材料可在线获取。
英文摘要
Let $X$ be uniform on $\{-1,1\}^n$, let $Y$ be obtained by passing its coordinates independently through a binary symmetric channel with crossover probability $p$, and let $g:\{-1,1\}^n\to\{0,1\}$ be a Boolean function. We give a computer-assisted proof of the Courtade--Kumar conjecture $I(g(X);Y)\le1-H_2(p)$, where $H_2$ is binary entropy, with equality attained by dictator functions. The present work builds on the differential-equation method, itself a limiting form of the auxiliary-receiver approach in network information theory using a continuum of degraded receivers. The proof proceeds from a local inequality to a dimension-independent bound on entropy production. Differentiation along the Boolean noise semigroup expresses entropy production as an average of edge costs. The key estimate is therefore an unrestricted Bellman inequality with two mean constraints and two entropy constraints, allowing arbitrary couplings of the edge variables. This paper and its supplement provide the proofs and computational verification records. The document is lengthy because it is designed to be entirely self-contained, deriving all proofs from first principles and reproducing the proofs of cited results. We also give a self-contained expository note explaining the reduction to a low-dimensional inequality and the ideas behind the key lower bounds. The entire proof, including all numerical certificates, has been formally verified in Lean end-to-end, and is available online.
CommentsAdded links to end-to-end lean formalization, a short expository note, and discussion of concurrent work
