Prove2Me

Amplitude-damping amplitude outputs and root fidelity

Open
QAlgorithms.Papers.Independent.Intakethird100.P74.damping_amplitude_fidelity

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

prove2quantum

Let 0≤η≤10\le\eta\le1 be transmissivity. The qubit amplitude-damping channel has Kraus operators A0=1−η∣0⟩⟨1∣A_0=\sqrt{1-\eta}|0\rangle\langle1| and A1=∣0⟩⟨0∣+η∣1⟩⟨1∣A_1=|0\rangle\langle0|+\sqrt\eta|1\rangle\langle1|. Its computational-basis amplitude outputs are

ρ0=∣0⟩⟨0∣,ρ1=(1−η)∣0⟩⟨0∣+η∣1⟩⟨1∣,F(ρ0,ρ1)=1−η.\rho_0=|0\rangle\langle0|,\qquad \rho_1=(1-\eta)|0\rangle\langle0|+\eta|1\rangle\langle1|, \qquad\sqrt{F(\rho_0,\rho_1)}=\sqrt{1-\eta}.

This identifies the amplitude contribution to the source's root-fidelity criterion. The source's word fidelity in this sentence refers to root fidelity under its squared-FF convention.

Preamble
import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P74
Formal statement
namespace QAlgorithms.Papers.Independent.Intakethird100.P74

open QAlgorithms

open scoped ComplexConjugate Matrix

noncomputable section

local instance (p : Prop) : Decidable p := Classical.propDecidable p

variable {B E S1 S2 : Type}

variable [Fintype B] [Fintype E] [Fintype S1] [Fintype S2]

variable [DecidableEq B] [DecidableEq E] [DecidableEq S1] [DecidableEq S2]

/-- PDF p.10, Appendix C.C: both amplitude outputs and their ROOT fidelity.
The source's word "fidelity" here means root fidelity under its §I squared-F convention. -/
theorem damping_amplitude_fidelity (eta : ℝ) (he0 : 0 ≤ eta) (he1 : eta ≤ 1) :
    dampingAmplitude eta false = pureDensity (ket false) ∧
    dampingAmplitude eta true = (1 - (eta : ℂ)) • pureDensity (ket false) +
      (eta : ℂ) • pureDensity (ket true) ∧
    rootFidelity (dampingAmplitude eta false) (dampingAmplitude eta true) =
      Real.sqrt (1 - eta) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P74
Source
Polar codes for private classical communication, arXiv:1203.5794v1, PDF p. 10, Appendix C.C, unnumbered: amplitude-damping amplitude channel
Read-back

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

For every real number η\eta with 0≤η≤10\le\eta\le1, define ρη,z=∑j=01Kj∣z⟩⟨z∣Kj†\rho_{\eta,z}=\sum_{j=0}^1K_j|z\rangle\langle z|K_j^\dagger for Boolean zz, where ∣z⟩|z\rangle is the coordinate vector, K0=diag⁡(1,η)K_0=\operatorname{diag}(1,\sqrt\eta), and K1=1−η ∣false⟩⟨true∣K_1=\sqrt{1-\eta}\,|\mathrm{false}\rangle\langle\mathrm{true}|. Then all three assertions hold:

ρη,false=∣false⟩⟨false∣,ρη,true=(1−η)∣false⟩⟨false∣+η∣true⟩⟨true∣,Re⁡tr⁡ρη,false ρη,trueρη,false=1−η.\rho_{\eta,\mathrm{false}}=|\mathrm{false}\rangle\langle\mathrm{false}|,\qquad \rho_{\eta,\mathrm{true}} =(1-\eta)|\mathrm{false}\rangle\langle\mathrm{false}| +\eta|\mathrm{true}\rangle\langle\mathrm{true}|, \qquad \operatorname{Re}\operatorname{tr} \sqrt{\sqrt{\rho_{\eta,\mathrm{false}}}\, \rho_{\eta,\mathrm{true}}\sqrt{\rho_{\eta,\mathrm{false}}}} =\sqrt{1-\eta}.

The matrix square roots use spectral functional calculus, and both endpoints η=0,1\eta=0,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