Classical Capacity and Entanglement Cost of the Amplitude Damping Channel
Ziao Tang, Chengkai Zhu, Ge Bai, Xin Wang
quant-ph
Sep 23, 2026 · v1
TL;DR
Results on the amplitude damping channel's classical capacity are formalized in Lean 4 with Mathlib and Lean-QIT, released with a manuscript-to-Lean correspondence on GitHub.
Abstract
Determining a noisy quantum channel's classical capacity and entanglement cost generally requires regularization over many channel uses. We remove both regularizations for every qubit-to-qubit channel admitting a pure output. For each such channel, Holevo information, channel entanglement of formation, and parallel entanglement cost are additive with those of any finite-dimensional partner channel. This class includes all qubit-to-qubit channels of Kraus rank at most two. For the amplitude damping channel with damping probability $p$, the unassisted classical capacity equals the known single-use Holevo information, attained by a binary pure-state ensemble with collective decoding, and the entanglement cost is $h_2((1+\sqrt p)/2)$ ebits per use. The common mechanism is a support criterion for strong superadditivity of entanglement of formation: one marginal has no support on the sector in which both local systems are orthogonal to fixed distinguished vectors. We prove this criterion in arbitrary finite dimensions using a triangular block-matrix entropy inequality and decompositions preserving two expectations. For amplitude damping, we also derive an exact finite-block Holevo deficit, identify the unique optimal average input for $p<1$, and construct a binary Kraus representation attaining the uniform formation bound.
Problem
The classical capacity and entanglement cost of a noisy quantum channel generally require regularization over many channel uses. For the qubit amplitude damping channel, it was open whether entangled encodings could beat the single-use Holevo information.
Approach
The authors prove a support criterion for strong superadditivity of entanglement of formation in arbitrary finite dimensions. The proof uses a triangular block-matrix entropy inequality and decompositions that preserve two expectations. Via the Stinespring and Choi correspondences, the criterion yields additivity for qubit-to-qubit channels admitting a pure output. The results are formalized in Lean 4 using Mathlib and Lean-QIT.
Results
For every qubit-to-qubit channel with a pure output, which includes all channels of Kraus rank at most two, classical capacity equals the Holevo information and parallel entanglement cost equals the entanglement of formation of the Choi state, with additivity against any partner channel. For amplitude damping, the capacity is the known single-use Holevo information and the entanglement cost is h2((1+√p)/2) ebits per use.
