Classical capacity of generalized amplitude damping
Classical capacity of generalized amplitude damping is the subject of a manuscript dated 24 September 2026 in OpenAI's public mathematics collection (github.com/openai/math). Generalized amplitude-damping channels model the loss of energy of a qubit to a thermal environment. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
The original result
- Claim. The unassisted classical capacity of every qubit generalized amplitude-damping channel, for all damping strengths and thermal occupations, equals its one-shot Holevo capacity and is given by a one-variable maximum; a binary pure-state ensemble attains the one-use optimum. The manuscript also states that the one-shot Holevo capacity, the minimum output entropy and the regularized classical capacity are additive under tensor product with every finite-dimensional channel. Source: the manuscript Classical capacity and entropy inequalities for generalized amplitude damping, dated 24 September 2026.
- Formalization, as described by the repository. The scope note lean/docs/276.md states that the formalization determines the capacity for all parameters, proves additivity of the Holevo information across repeated uses of the same channel, and identifies it with the operational capacity per use; additivity with an arbitrary different partner channel is not included.
Related work
- K. Fang, The classical capacity of generalized amplitude-damping channels and its strong-converse exponent (arXiv:2609.14621, v1 13 September 2026, v2 6 October 2026), states that the classical capacity of generalized amplitude-damping channels equals the known one-copy Holevo information, and determines the strong-converse exponent.
- Z. Tang, C. Zhu, G. Bai, X. Wang, Classical Capacity and Entanglement Cost of the Amplitude Damping Channel (arXiv:2609.28592, v1 23 September 2026), state additivity of the Holevo information with any finite-dimensional partner for every qubit-to-qubit channel admitting a pure output.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 14 October 2026) |
|---|---|---|---|---|
| 2026-10-08 | MathVet (GitHub; review of openai/math at commit adc7f12, tables at repository commit cd0063d, 13 October 2026) |
Review (fidelity of the formal statements) | Rates this family "partial": the Lean states the capacity formula, additivity across uses of the same channel and the operational capacity, but not the additivity with an arbitrary finite-dimensional partner channel stated in the summary. Its per-challenge table records a sandboxed Comparator pass for the challenge AmplitudeDamping (8 October 2026). |
The review states that its ratings concern whether the Lean states the headline and "does not say the mathematics is correct beyond what Lean checked"; it describes itself as a model-assisted reading without a referee yet. |
2026-10-11 (latest commit 90e61c4, 12 October 2026) |
KitaKen1/qubit-strong-additivity (GitHub) | Extension (formal) | States a Lean proof that χ(Φ ⊗ Ω) = χ(Φ) + χ(Ω) for every qubit channel Φ and every channel Ω between matrix algebras of positive finite dimension, where χ is the Holevo information over finite ensembles with entangled inputs allowed, and hence χ(Φ⊗n) = n χ(Φ). The formalization vendors parts of Physlib and of OpenAI's formalization for this family. | The README gives an AI-generated sketch of the proof and records the author's run of the Lean Comparator. |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.