Exact amplitude-damping phase output matrix

Proved

QAlgorithms.Papers.Independent.Intakethird100.P74.damping_phase_state

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

prove2quantum

For $0\le\eta\le1$ , let $\mathcal N_\eta$ be the qubit amplitude-damping channel with Kraus operators $\sqrt{1-\eta}|0\rangle\langle1|$ and $|0\rangle\langle0|+\sqrt\eta|1\rangle\langle1|$ . Let $|\Phi\rangle=(|00\rangle+|11\rangle)/\sqrt2$ , with reference $C$ first, and modulate $C$ by $Z^x$ for $x\in\{0,1\}$ . In the ordered basis $|00\rangle,|01\rangle,|10\rangle,|11\rangle$ ,

(\mathrm{id}_C\otimes\mathcal N_\eta)(Z_C^x|\Phi\rangle\langle\Phi|Z_C^x) =\begin{pmatrix} \frac12&0&0&\frac{(-1)^x\sqrt\eta}{2}\\ 0&0&0&0\\ 0&0&\frac{1-\eta}{2}&0\\ \frac{(-1)^x\sqrt\eta}{2}&0&0&\frac\eta2 \end{pmatrix}.

This gives an exact symbolic phase-channel state, without inferring a numerical parameter interval from Figure 2.

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 pp.10–11, Appendix C.C: the normalized symbolic phase output matrix, in
C-first computational order. The undefined gamma in an intermediate line is bypassed
using the printed Kraus operators and the final eta-only formula. No numerical key-rate
interval is inferred from this exact state identity. -/
theorem damping_phase_state (eta : ℝ) (he0 : 0 ≤ eta) (he1 : eta ≤ 1) (x : Bool) :
    dampingPhaseOutput eta x = Matrix.of (fun p q =>
      dampingPhaseMatrix eta x (cbIndex p) (cbIndex q)) := by sorry

end

end QAlgorithms.Papers.Independent.Intakethird100.P74

Source

Polar codes for private classical communication, arXiv:1203.5794v1, PDF p. 11, Appendix C.C, unnumbered: explicit phase-channel output matrices

Read-back

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

For every real $\eta$ satisfying $0\leq\eta\leq1$ , including both endpoints, and every Boolean $x$ , put $s_x=1$ for $x=\mathrm{false}$ and $s_x=-1$ for $x=\mathrm{true}$ . In the Boolean basis ordered as $\mathrm{false},\mathrm{true}$ , define

v_x=\frac{|\mathrm{false},\mathrm{false}\rangle+s_x|\mathrm{true},\mathrm{true}\rangle}{\sqrt2}, \qquad K_0=\begin{pmatrix}1&0\\0&\sqrt{\eta}\end{pmatrix}, \qquad K_1=\begin{pmatrix}0&\sqrt{1-\eta}\\0&0\end{pmatrix},

where each ket is the coordinate vector equal to one at its indicated pair and zero elsewhere. The assertion is that applying the map $X\mapsto K_0XK_0^\dagger+K_1XK_1^\dagger$ to the second Boolean factor of the matrix $v_xv_x^\dagger$ gives, for every pair of Boolean pairs $p,q$ ,

\left[\sum_{r=0}^{1}(I_2\otimes K_r)\,v_xv_x^\dagger\,(I_2\otimes K_r)^\dagger\right]_{p,q} = \begin{pmatrix} \frac12&0&0&\frac{s_x\sqrt{\eta}}2\\ 0&0&0&0\\ 0&0&\frac{1-\eta}2&0\\ \frac{s_x\sqrt{\eta}}2&0&0&\frac{\eta}2 \end{pmatrix}_{c(p),c(q)},

where $c(\mathrm{false},\mathrm{false})=0$ , $c(\mathrm{false},\mathrm{true})=1$ , $c(\mathrm{true},\mathrm{false})=2$ , and $c(\mathrm{true},\mathrm{true})=3$ , and $\dagger$ denotes conjugate transpose.

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