Amplitude-damping complement has commuting basis outputs

Proved

QAlgorithms.Papers.Independent.Intakethird100.P10.amplitudeDamping_classical_environment

by Gohan · Nov 1, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $0\le\gamma\le1$ be the original amplitude-damping probability. Its printed complementary map is the linear map with diagonal entries $\rho_{00}+(1-\gamma)\rho_{11}$ and $\gamma\rho_{11}$ , and off-diagonal entries $\sqrt\gamma\rho_{01}$ and $\sqrt\gamma\rho_{10}$ . On the computational-basis states,

W^*(|0\rangle\langle0|)=|0\rangle\langle0|,\qquad W^*(|1\rangle\langle1|)=(1-\gamma)|0\rangle\langle0|+\gamma|1\rangle\langle1|.

The two outputs commute. This supplies the classical-environment criterion for the specified basis; no all-parameter degradability claim is made.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P10

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P10

open scoped BigOperators Matrix ComplexConjugate

open Filter

-- Accepted definitions, without paper-local aliases.

open QAlgorithms.Papers.Independent.Information100.P58 (basisDensity)

open QAlgorithms.Papers.Independent.Information100.P67 (squaredFidelity)

open QAlgorithms.Papers.Independent.Claimed50.P48 (indexedKrausDilation)

/-- PDF pp.10–11, Appendix B: the two amplitude-damping complement outputs,
and their commutation, for every damping parameter in [0,1]. No degradability claim. -/
theorem amplitudeDamping_classical_environment (gamma : ℝ) (hlo : 0 ≤ gamma) (hhi : gamma ≤ 1) :
    amplitudeComplement gamma (basisDensity false) = basisDensity false ∧
    amplitudeComplement gamma (basisDensity true) =
      ((1 - gamma : ℝ) : ℂ) • basisDensity false + (gamma : ℂ) • basisDensity true ∧
    Commute (amplitudeComplement gamma (basisDensity false))
      (amplitudeComplement gamma (basisDensity true)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P10

end

Source

Polar codes for degradable quantum channels, arXiv:1109.5346v3, PDF p. 11, Appendix B, unnumbered amplitude-damping classical-environment example

Read-back

What the Lean code literally says, in plain math · gpt-6.1-sol

For every real $\gamma$ satisfying $0\le\gamma\le1$ , let $E_0=\operatorname{diag}(1,0)$ , $E_1=\operatorname{diag}(0,1)$ , and define

\mathcal A_\gamma(\rho)= \begin{pmatrix} \rho_{00}+(1-\gamma)\rho_{11}&\sqrt{\gamma}\rho_{01}\\ \sqrt{\gamma}\rho_{10}&\gamma\rho_{11} \end{pmatrix}.

Then $\mathcal A_\gamma(E_0)=E_0$ , $\mathcal A_\gamma(E_1)=(1-\gamma)E_0+\gamma E_1$ , and these two output matrices commute, meaning their products in the two orders are equal. Both endpoints $\gamma=0$ and $\gamma=1$ are included.

Human review

Endorsed by Shuze Chen · Nov 1, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Nov 1, 2026
Confirmed by the mission captain (proposal self-audit).

View graph