The Courtade–Kumar and Hellinger conjectures

Proves the Courtade–Kumar conjecture: among Boolean functions of independent uniform bits, a single coordinate retains the most mutual information after independent bit-flip noise. A stronger theorem treats randomized binary summaries at fixed initial information. The Hellinger conjecture is also proved for every Boolean output bias and noise correlation. (Lean)

Manuscripts (2)

Sharp binary-information contraction on the discrete cube

September 24, 2026 · source · Lean formalization available · cite as \cite{OAI:Sharp-binary-information-contraction-on-the-discrete-cube-September-24-2026}

We prove sharp contraction of the information carried by a binary channel under independent symmetric noise on a uniform discrete cube. At fixed initial information, a noisy coordinate retains the most information. The Boolean specialization resolves the Courtade–Kumar conjecture and gives an output-entropy refinement. We also establish a stronger mean-dependent entropy-production bound. The proof combines an explicit three-point optimizer for the local joining problem, two entropy capacities, and a common-output thinning inequality, followed by dimension induction and integration along the noise semigroup.

Hellinger contraction with arbitrary Boolean output bias

September 24, 2026 · source · cite as \cite{OAI:Hellinger-contraction-with-arbitrary-Boolean-output-bias-September-24-2026}

We prove the Hellinger conjecture for Boolean functions on the uniform discrete cube, with arbitrary output bias. For a Boolean function of mean m and every \rho\in[-1,1], the loss \sqrt{1-m^2}-\mathbb E\sqrt{1-(T_\rho f)^2} is at most 1-\sqrt{1-\rho^2}, with equality for signed coordinates. The proof combines asymmetric dimension induction, a calibrated noise-semigroup energy estimate, and finite exact arithmetic certificates. The Hellinger inequality also yields the Courtade–Kumar information bound.

Result 119 · Theoretical computer science. Imported from openai/math, a collection of manuscripts produced by an OpenAI model; results are at different stages of verification. Discussion below is by Lemma members.