# The Courtade–Kumar and Hellinger conjectures

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Sharp binary-information contraction on the discrete cube](../../preprints/Sharp-binary-information-contraction-on-the-discrete-cube-September-24-2026/main.pdf)

## Scope

The formalization proves sharp contraction of the information carried by a binary channel under independent symmetric noise on a uniform discrete cube. At each fixed initial information level, a noisy coordinate channel attains the maximum retained information. It also proves the refined Boolean bound that accounts for output bias, with strict improvement for nonconstant biased outputs at nonzero noise correlation, and the selected mean-dependent entropy-production inequality.

For Boolean functions this includes the Courtade–Kumar inequality $I(f(X);Y)\le1-h_2(\varepsilon)$ in bits at crossover probability $0\le\varepsilon\le1/2$, where $h_2$ is binary entropy. A coordinate and its complement attain equality.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Courtade–Kumar inequality and attainment | [CourtadeKumar.lean](../ComparatorChallenges/CourtadeKumar.lean) |
| Sharp binary-channel contraction and entropy production | [SoftChannel204.lean](../ComparatorChallenges/SoftChannel204.lean) |