Appendix G1: mixed samples with one pure anchor

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.mixed_samples_pure_anchor

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

prove2quantum

Let a finite nonempty family of density operators $\rho_k$ generate all operators on the span of their supports, and assume the fixed anchor is exactly $\rho_a=|\phi\rangle\langle\phi|$ . Independently choose $k$ uniformly and $t$ uniformly on $[0,1]$ , and use $W(k,t)=T(k,t)HT(a,\pi)$ with $T(k,t)$ the controlled $e^{-it\rho_k}$ . Define $\mathcal W$ by the actual partial trace and entrywise integral. The integrands are continuous and integrable on the interval and every finite-history unit cube. Then

\mathcal W(|\phi\rangle\langle\phi|)=|\phi\rangle\langle\phi|,\qquad\lim_{T\to\infty}\|\mathcal W^T(\rho)-|\phi\rangle\langle\phi|\|_1=0.

The anchor is the unique supported fixed density operator. Using exact output records $U\rho_kU^\dagger$ and the corresponding reverse history, the integral-defined emulator converges uniformly on supported density operators to $U\rho U^\dagger$ . This is the exactly pure-anchor construction, without an unquantified near-purity extension.

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.28, G1: the EXACTLY pure anchor is the unique supported fixed state of
the continuous uniform-time channel. Its convergence permits supported-input emulation;
continuity/integrability of the displayed body is asserted, not assumed. -/
theorem mixed_samples_pure_anchor [Nonempty K] (S : K → Matrix I I ℂ) (a : K)
    (hS : ∀ k, IsDensityMatrix (S k)) (hgen : Generates S)
    (phi : EuclideanSpace ℂ I) (hphi : IsState phi) (hanchor : S a = pureDensity phi) :
    (∀ (rho : Matrix I I ℂ) (k : K), Continuous (fun t : ℝ =>
      traceRight (densityConjugation (mixedGate S a k t) (Matrix.kronecker rho (pureDensity minusVector))))) ∧
    (∀ (rho : Matrix I I ℂ) (k : K) (i j : I), IntegrableOn (fun t : ℝ =>
      traceRight (densityConjugation (mixedGate S a k t)
        (Matrix.kronecker rho (pureDensity minusVector))) i j) (Set.Icc 0 1)) ∧
    (∀ (rho : Matrix I I ℂ) (U : Matrix.unitaryGroup I ℂ) (T : ℕ) (h : Fin T → K) (i j : I),
      IntegrableOn (fun ts : Fin T → ℝ => mixedHistoryOutput S a phi (U : Matrix I I ℂ) rho h ts i j)
        (Set.pi Set.univ (fun _ : Fin T => Set.Icc (0 : ℝ) 1))) ∧
    mixedSampleErasureChannel S a (pureDensity phi) = pureDensity phi ∧
    (∀ rho : Matrix I I ℂ, IsDensityMatrix rho → InSampleSupport S rho →
      mixedSampleErasureChannel S a rho = rho → rho = pureDensity phi) ∧
    (∀ rho : Matrix I I ℂ, IsDensityMatrix rho → InSampleSupport S rho →
      Tendsto (fun T : ℕ => traceNorm ((mixedSampleErasureChannel S a)^[T] rho - pureDensity phi)) atTop (nhds 0)) ∧
    (∀ (U : Matrix.unitaryGroup I ℂ) (eps : ℝ), 0 < eps → ∃ N : ℕ, ∀ T ≥ N,
      ∀ rho : Matrix I I ℂ, IsDensityMatrix rho → InSampleSupport S rho →
      traceDistance (mixedEmulate S a phi (U : Matrix I I ℂ) T rho) (densityConjugation (U : Matrix I I ℂ) rho) ≤ eps) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 28, Appendix G1: mixed samples with one pure anchor

Read-back

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

Let $I,K$ be finite index types with decidable equality, with $K$ nonempty, and fix $a\in K$ . Let every $S_k$ be a positive semidefinite matrix on $\mathbb C^I$ of trace $1$ , let $\Pi$ be the functional-calculus value of $x\mapsto\mathbf1_{x\ne0}$ on $\sum_kS_k$ , and assume that the complex span of all nonempty products $S_{k_1}\cdots S_{k_s}$ is $\{X:\Pi X\Pi=X\}$ . Let $\phi\in\mathbb C^I$ have norm $1$ , and assume $S_a=\phi\phi^\dagger$ . Write $C(V)=1_I\otimes|0\rangle\langle0|+V\otimes|1\rangle\langle1|$ , $H=2^{-1/2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}$ , $\eta=(|0\rangle-|1\rangle)/\sqrt2$ , and

E_k(s)=C(e^{-isS_k})(1_I\otimes H)C(e^{-i\pi S_a}), \qquad F_{\rho,k}(s)=\operatorname{Tr}_{\mathrm{anc}}\!\left[ E_k(s)(\rho\otimes\eta\eta^\dagger)E_k(s)^\dagger \right], \qquad \mathcal A(\rho)=\frac1{|K|}\sum_k\int_0^1F_{\rho,k}(s)\,ds,

where matrix integrals are taken entrywise with respect to Lebesgue measure. For $h\in K^T$ and $s\in[0,1]^T$ , let $V_{h,s}$ apply $E_{h_j}(s_j)$ successively to the system and ancilla $j$ , put $\eta_T=\eta^{\otimes T}$ , $X_{h,s}=V_{h,s}(\rho\otimes\eta_T\eta_T^\dagger)V_{h,s}^\dagger$ , and $V^{U}_{h,s}=(U\otimes1)V_{h,s}(U^\dagger\otimes1)$ , and define

G_{\rho,U,h}(s)= \operatorname{Tr}_{\mathrm{anc}}\!\left[ (V^U_{h,s})^\dagger \left(U\phi\phi^\dagger U^\dagger\otimes\operatorname{Tr}_{I}X_{h,s}\right) V^U_{h,s} \right], \qquad \mathcal M_{U,T}(\rho)=\frac1{|K|^T}\sum_{h\in K^T}\int_{[0,1]^T}G_{\rho,U,h}(s)\,ds.

The assertion is that $F_{\rho,k}$ is continuous for every complex matrix $\rho$ and every $k$ ; that each entry of $F_{\rho,k}$ is integrable on $[0,1]$ for every $\rho,k$ ; and that each entry of $G_{\rho,U,h}$ is integrable on $[0,1]^T$ for every complex matrix $\rho$ , every unitary $U$ , every natural number $T$ , and every history $h\in K^T$ . It also asserts $\mathcal A(\phi\phi^\dagger)=\phi\phi^\dagger$ ; for every positive semidefinite $\rho$ of trace $1$ with $\Pi\rho\Pi=\rho$ , the implication $\mathcal A(\rho)=\rho\Rightarrow\rho=\phi\phi^\dagger$ ; for every such $\rho$ ,

\operatorname{Re}\operatorname{tr} \sqrt{(\mathcal A^{\,T}(\rho)-\phi\phi^\dagger)^\dagger (\mathcal A^{\,T}(\rho)-\phi\phi^\dagger)} \longrightarrow0\quad(T\to\infty),

where $\mathcal A^{\,T}$ means $T$ -fold composition; and, for every unitary $U$ and every $\varepsilon>0$ , the existence of a natural number $N$ such that, for every $T\ge N$ and every such $\rho$ ,

\tfrac12\operatorname{Re}\operatorname{tr} \sqrt{(\mathcal M_{U,T}(\rho)-U\rho U^\dagger)^\dagger (\mathcal M_{U,T}(\rho)-U\rho U^\dagger)} \le\varepsilon.

The definitions and integrability assertions include $T=0$ , using empty products and the zero-dimensional integration domain; no assumption $|K|\ge2$ is imposed.

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