The Courtade–Kumar and Hellinger conjectures

1 · The essentials

Imagine a collection of independent bits, each equally likely to be zero or one, and a rule that turns them into a single bit. If the original bits are independently flipped at random, how much can that single-bit answer still tell us about them? The main result says that simply choosing one original bit retains the most information. It also treats rules that use randomness: when their starting information is fixed, a suitably noisy single bit is best. The main manuscript has a Lean formalization, providing machine-checked verification of its central result. A companion manuscript shows a related bound using a different measure of information, even when the rule’s two possible answers are not equally likely. These conclusions concern equally likely, independent input bits and the specific independent bit-flip noise studied in the manuscripts.

A picture to help (an imperfect image, not to be taken literally)

As an imperfect image, imagine fair coin tosses written on a sheet, followed by independent random mistakes that reverse some entries. You may keep a one-bit note about the original sheet: the result says that recording one chosen entry is as informative about the altered sheet as any Boolean rule for writing that note. The image is limited because “informative” here has a precise mathematical meaning, not a judgment about which note would be most useful for a particular task.

Why it matters

The results identify an exact limit on how much information a binary summary can retain under the specified noise. The main manuscript resolves the Courtade–Kumar conjecture and strengthens it by comparing randomized binary summaries with the same starting information. The companion manuscript connects a Hellinger inequality to the same information bound, giving a related route to that conclusion.

2 · Going further

The setting is the uniform discrete cube: independent, uniformly distributed input bits, with independent symmetric bit-flip noise. The Courtade–Kumar question asks which Boolean function retains the most mutual information after this noise; a single coordinate is optimal. The main manuscript treats the broader problem of binary channels, which allow randomized outputs. At fixed initial information, a noisy coordinate is optimal, and the Boolean specialization includes an output-entropy refinement.

The main argument combines an explicit three-point optimizer for a local joining problem, two entropy capacities, and a common-output thinning inequality. These ingredients are followed by induction on dimension and integration along the noise semigroup. The manuscript also establishes a stronger entropy-production bound that depends on the output mean. The main result has a Lean formalization; the supplied description does not specify separate formalization coverage for every auxiliary claim.

The companion manuscript concerns Boolean functions written with values $- 1$ and $1$ . For mean $m$ and noise correlation $ρ \in [- 1, 1]$ , it shows the Hellinger inequality $1 - m^{2} - E 1 - (T_{ρ} f)^{2} \leq 1 - 1 - ρ^{2}$ , with equality for signed coordinates. Here $T_{ρ} f$ denotes the noise-averaged function. Its argument combines asymmetric dimension induction, a calibrated noise-semigroup energy estimate, and finite exact arithmetic certificates. This inequality also yields the Courtade–Kumar information bound, linking the companion manuscript to the main result.

Useful notions

Independent, equally likely random bits
Boolean functions and randomized binary outputs
Expectation and output bias
Entropy and mutual information
Induction on the number of input bits

What was known before / what is new

Before

The source identifies the Courtade–Kumar conjecture as the question of whether a single coordinate maximizes retained mutual information among Boolean functions under independent bit-flip noise. It also identifies a related Hellinger conjecture. It does not provide earlier partial results or a historical timeline.

New

The main manuscript establishes sharp binary-information contraction, including optimality of a noisy coordinate at fixed initial information for randomized binary summaries. It also gives an output-entropy refinement for Boolean functions and a stronger mean-dependent entropy-production bound. The companion manuscript shows the Hellinger inequality for arbitrary Boolean output bias and every noise correlation in $[- 1, 1]$ , and derives the Courtade–Kumar bound from it.

Limits and assumptions

The hypotheses are uniform, independent input bits and independent symmetric noise; the source does not state extensions to other input distributions or noise models. The fixed-initial-information comparison in the main manuscript concerns binary summaries, including randomized ones. The companion Hellinger result allows arbitrary Boolean output bias and all $ρ \in [- 1, 1]$ . The main result has a Lean formalization, but the supplied source does not delineate formal coverage of every refinement or auxiliary claim; it does not identify the companion manuscript as Lean-formalized. No remaining open problem is specified in the source.

Mini glossary

Boolean function: A rule that assigns one of two possible outputs to each input bit string.
Uniform discrete cube: The collection of fixed-length bit strings with every string equally likely, corresponding to independent fair input bits.
Mutual information: A mathematical measure of how much knowing one random quantity tells you about another.
Binary channel: A rule that produces one of two outputs from an input, possibly using randomness.
Signed coordinate: A function that returns a single input coordinate or its negative when bits are represented by $- 1$ and $1$ .
Noise semigroup: A family of noise operations organized so that successive applications correspond to a combined amount of noise.

Keywords : Courtade–Kumar conjecture · Information contraction · Hellinger inequality

AI-generated explanation based on the manuscript. Unofficial. Refer to the manuscript for the authoritative version.

3 · Technical details and sources

Claim made in the manuscript (source text)

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.

Verified by Lean: the Lean software checked the part of the reasoning described below, sometimes only part of the manuscript. This does not mean independent mathematicians have validated the result.

Scope of the Lean formalization (source text)

…

lean/docs/119.md

Manuscripts in this family

★

Sharp binary-information contraction on the discrete cube

24/09/2026

Verified by Lean

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.

PDF GitHub folder Lean formalization

Hellinger contraction with arbitrary Boolean output bias

24/09/2026

To be verified

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 $ρ \in [- 1, 1]$ , the loss $1 - m^{2} - E 1 - (T_{ρ} f)^{2}$ is at most $1 - 1 - ρ^{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.

PDF GitHub folder