Erasure complement has commuting outputs in every input basis

Open

QAlgorithms.Papers.Independent.Intakethird100.P10.erasure_classical_environment

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

prove2quantum

Let $d\ge1$ , $0\le\epsilon\le1$ , and let $\{|x\rangle\}_{x=1}^d$ be any orthonormal input basis. Use the orthogonally flagged erasure complement $E_{1-\epsilon}$ , with flag $|e\rangle$ orthogonal to the data space. For every density operator $\rho$ ,

E_{1-\epsilon}(\rho)=\epsilon\rho\oplus(1-\epsilon)|e\rangle\langle e|,

where $\rho$ is embedded into the data sector. Moreover, for every pair of basis indices $x,y$ ,

[E_{1-\epsilon}(|x\rangle\langle x|),E_{1-\epsilon}(|y\rangle\langle y|)]=0.

This gives the classical-environment criterion in any orthonormal input basis, including the one-dimensional case.

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 p.11: the genuine orthogonally flagged complement is the accepted erasureMap
at 1-epsilon. Its action on density matrices has the printed flag weight, and
all outputs from ANY orthonormal input basis commute pairwise. -/
theorem erasure_classical_environment (d : ℕ) (hd : 0 < d)
    (epsilon : ℝ) (hlo : 0 ≤ epsilon) (hhi : epsilon ≤ 1)
    (basis : Matrix.unitaryGroup (Fin d) ℂ) :
    (∀ rho : Matrix (Fin d) (Fin d) ℂ, IsDensityMatrix rho →
      QAlgorithms.Papers.Independent.Support50.P07.erasureMap d (1 - epsilon) rho =
        (epsilon : ℂ) • erasureData d rho +
          ((1 - epsilon : ℝ) : ℂ) • basisDensity (none : Option (Fin d))) ∧
    (∀ x y : Fin d, Commute
      (QAlgorithms.Papers.Independent.Support50.P07.erasureMap d (1 - epsilon)
        (pureDensity (basisColumn basis x)))
      (QAlgorithms.Papers.Independent.Support50.P07.erasureMap d (1 - epsilon)
        (pureDensity (basisColumn basis y)))) := 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 erasure-channel classical-environment example

Read-back

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

For every positive natural number $d$ , every real $\epsilon$ with $0\leq\epsilon\leq1$ , and every unitary complex $d\times d$ matrix $U$ , let $u_x$ denote column $x$ of $U$ , and define the map $\mathcal E_\epsilon$ by $(\mathcal E_\epsilon(\rho))_{a,b}=\epsilon\rho_{a,b}$ on ordinary indices, $(\mathcal E_\epsilon(\rho))_{\varnothing,\varnothing}=(1-\epsilon)\operatorname{tr}\rho$ , and zero on mixed ordinary and additional indices. Then every positive semidefinite matrix $\rho$ of trace one satisfies

\mathcal E_\epsilon(\rho)=\epsilon\widetilde{\rho}+(1-\epsilon)|\varnothing\rangle\langle\varnothing|,

where $\widetilde{\rho}$ is $\rho$ extended by a zero row and column, and $|\varnothing\rangle\langle\varnothing|$ has its sole nonzero entry, equal to one, at $(\varnothing,\varnothing)$ . Moreover, for every pair of column indices $x,y$ , the matrices $\mathcal E_\epsilon(u_xu_x^\dagger)$ and $\mathcal E_\epsilon(u_yu_y^\dagger)$ commute. Both endpoints $\epsilon=0$ and $\epsilon=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