∑math20

Mathematical physics · Result 276

Classical capacity of generalized amplitude damping

1 paperLean

Determines the unassisted classical capacity of every qubit generalized amplitude-damping channel, including all damping and thermal parameters. An explicit one-variable optimization gives the capacity, attained by independent two-state signal ensembles with collective decoding. Holevo capacity, minimum output entropy and regularized classical capacity are additive when tensoring with any finite-dimensional quantum channel.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of Classical capacity and entropy inequalities for generalized amplitude damping

Classical capacity and entropy inequalities for generalized amplitude damping

OpenAI · September 24, 2026

We determine the unassisted classical capacity of every qubit generalized amplitude-damping channel, for all damping strengths and thermal occupations. It equals the one-shot Holevo capacity and is given by a one-variable maximum. A binary pure-state ensemble attains the one-use optimum, and its independent products attain the optimum at every block length. We also prove that one-shot Holevo capacity, minimum output entropy, and regularized unassisted classical capacity are additive under tensor product with every finite-dimensional completely positive trace-preserving partner channel.

Read PDF Download Source

Cite
@misc{OAI:Classical-capacity-and-entropy-inequalities-for-generalized-amplitude-damping-September-24-2026,
  author = {{OpenAI}},
  title = {{Classical capacity and entropy inequalities for generalized amplitude damping}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Classical-capacity-and-entropy-inequalities-for-generalized-amplitude-damping-September-24-2026/paper.pdf}{OAI:Classical-capacity-and-entropy-inequalities-for-generalized-amplitude-damping-September-24-2026}},
  year = {2026}
}

What was formalized in Lean

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

Scope

The formalized result determines the unassisted classical capacity of every generalized amplitude-damping channel with parameters in \([0,1]^2\). Its unrestricted Holevo information is additive across every number of repeated uses, equals an attained scalar maximum, and agrees with the operational capacity per use. Every maximizing equiprobable phase-pair product ensemble attains the corresponding block value. Additivity with an arbitrary different partner channel and decoding by separate measurements are not included.

Comparator links

ResultComparator statement
Additivity and capacity for generalized amplitude dampingAmplitudeDamping.lean

Scope note on GitHub →