Proposition 2: convergence of coherent erasure

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.proposition2_erasure

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

prove2quantum

Let $K\ge2$ normalized pure samples generate the full algebra on their span, and fix one anchor $\phi_a$ . At each round choose a nonanchor index independently and uniformly, apply $R(k)HR(a)$ to the system and a fresh $\lvert-\rangle$ ancilla, and trace out that ancilla. Let $\mathcal W$ be this averaged channel. For every supported density operator $\rho$ ,

\lim_{T\to\infty}\|\mathcal W^T(\rho)-\lvert\phi_a\rangle\langle\phi_a\rvert\|_1=0.

Moreover, the anchor density is the unique supported fixed density operator. The average is over histories; no claim is made about every individual random history. The displayed nonanchor average is restricted to $K\ge2$ ; rank-one reset is covered separately in the ideal-error result.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P67

Formal statement

noncomputable section

open scoped ComplexConjugate Matrix Matrix.Norms.L2Operator

attribute [local instance] Classical.propDecidable

open MeasureTheory Filter

namespace QAlgorithms.Papers.Independent.Intakethird100.P67

variable {I J K L A : Type*} [Fintype I] [DecidableEq I]
  [Fintype J] [DecidableEq J] [Fintype K] [DecidableEq K]
  [Fintype L] [DecidableEq L] [Fintype A] [DecidableEq A]

/-- PDF p.5, Proposition 2: the averaged channel converges in trace norm and has the
anchor as its unique supported fixed density. K>=2 makes the displayed average defined. -/
theorem proposition2_erasure (phi : K → EuclideanSpace ℂ I) (a : K)
    (hK : 2 ≤ Fintype.card K) (hphi : ∀ k, IsState (phi k))
    (hgen : Generates (pureSamples phi)) :
    (∀ rho, IsDensityMatrix rho → InSampleSupport (pureSamples phi) rho →
      Tendsto (fun T : ℕ => traceNorm
        ((coherentErasureChannel (nonanchorProbability a) (erasureGate phi a))^[T] rho -
          pureDensity (phi a))) atTop (nhds 0)) ∧
    (∀ rho, IsDensityMatrix rho → InSampleSupport (pureSamples phi) rho →
      coherentErasureChannel (nonanchorProbability a) (erasureGate phi a) rho = rho →
        rho = pureDensity (phi a)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 5, Proposition 2: convergence of coherent erasure

Read-back

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

Let $I,K$ be finite types with decidable equality, let $|K|\ge2$ , choose $a\in K$ , and let every vector $\phi_k\in\mathbb C^I$ have norm $1$ . Put $S_k=|\phi_k\rangle\langle\phi_k|$ , $\Pi=f(\sum_kS_k)$ , where continuous functional calculus uses $f(0)=0$ and $f(t)=1$ otherwise, and suppose that the complex span of all nonempty finite products of the $S_k$ consists exactly of the matrices $X$ satisfying $\Pi X\Pi=X$ . Define $R_k=1-2S_k$ , let $C(R)$ apply $R$ to the system when a Boolean ancilla is true and the identity when it is false, let $H=2^{-1/2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}$ in false–true order, and put

W_k=C(R_k)(1\otimes H)C(R_a),\qquad p_k=\begin{cases}0,&k=a,\$|K|-1)^{-1},&k\ne a,\end{cases} \qquad \mathcal E(\rho)=\sum_kp_k\operatorname{Tr}_{\mathrm{anc}} \!\left[W_k(\rho\otimes|-\rangle\langle-|)W_k^\dagger\right], \quad |-\rangle=\frac{|0\rangle-|1\rangle}{\sqrt2}.

Then both of the following hold: for every positive semidefinite trace-one (\rho $satisfying$ \Pi\rho\Pi=\rho $, the sequence$ \operatorname{Re}\operatorname{Tr}\sqrt{(\mathcal E^T(\rho)-S_a)^\dagger(\mathcal E^T(\rho)-S_a)} $tends to$ 0 $as the natural number$ T $tends to infinity; and every such$ \rho $with$ \mathcal E(\rho)=\rho $equals$ S_a $. Here$ \mathcal E^T $denotes$ T $-fold function iteration, including the identity at$ T=0$.

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