# Classical capacity of generalized amplitude damping

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

- [Classical capacity and entropy inequalities for generalized amplitude damping](../../preprints/Classical-capacity-and-entropy-inequalities-for-generalized-amplitude-damping-September-24-2026/paper.pdf)

## 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

| Result | Comparator statement |
| --- | --- |
| Additivity and capacity for generalized amplitude damping | [AmplitudeDamping.lean](../ComparatorChallenges/AmplitudeDamping.lean) |