§III: general-input projection and conditional emulation

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.emulator_projection_limit

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

prove2quantum

Let normalized pure samples, $K\ge2$ , generate the full algebra on their span, and let $\Pi$ be its projector. Fix an anchor and an unknown unitary $U$ . In Fig.2 take the reconstructed system on $b=0$ and the old system from the SWAP on $b=1$ . Let $\mathcal F_{T,b}$ be these averaged subnormalized output branches. For every input density operator,

\lim_{T\to\infty}\|\mathcal F_{T,0}(\rho)-U\Pi\rho\Pi U^\dagger\|_1=0,\qquad\lim_{T\to\infty}\|\mathcal F_{T,1}(\rho)-(I-\Pi)\rho(I-\Pi)\|_1=0.

This states projection followed by conditional emulation on the successful branch, including zero Born probability without division. The circuit and its algebra promise differ from Appendix H's unknown-projector instrument.

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 pp.4,6: general-input Fig.2 instrument converges to conditional emulation
on H_in and projection on its complement, using the actual outcome-dependent wires. -/
theorem emulator_projection_limit (phi : K → EuclideanSpace ℂ I) (a : K)
    (hK : 2 ≤ Fintype.card K) (hphi : ∀ k, IsState (phi k))
    (hgen : Generates (pureSamples phi)) (U : Matrix.unitaryGroup I ℂ)
    (rho : Matrix I I ℂ) (hrho : IsDensityMatrix rho) :
    let Pi := samplePi (pureSamples phi)
    Tendsto (fun T : ℕ => traceNorm (wireBranch phi a (U : Matrix I I ℂ) T false rho -
      densityConjugation (U : Matrix I I ℂ) (Pi * rho * Pi))) atTop (nhds 0) ∧
    Tendsto (fun T : ℕ => traceNorm (wireBranch phi a (U : Matrix I I ℂ) T true rho -
      (1-Pi) * rho * (1-Pi))) atTop (nhds 0) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 4, §III: general-input projection and conditional emulation

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, let $a\in K$ , assume $|K|\ge2$ , and let every $\phi_k\in\mathbb C^I$ have norm $1$ . Put $E_k=\phi_k\phi_k^\dagger$ , and let $\Pi=f(\sum_kE_k)$ by continuous functional calculus, where $f(0)=0$ and $f(x)=1$ otherwise. Assume that, for every complex matrix $X$ on $I$ , membership in the complex linear span of all nonempty products $E_{k_1}\cdots E_{k_r}$ is equivalent to $\Pi X\Pi=X$ . Let $U$ be unitary and let $\rho$ be positive semidefinite with trace $1$ . Define $p_a=0$ , $p_k=(|K|-1)^{-1}$ for $k\ne a$ , $R_k=1-2E_k$ , and $W_k=C(R_k)(1\otimes H_{\rm Had})C(R_a)$ , where $C(M)$ applies $M$ when the Boolean ancilla is true and the identity otherwise, and $H_{\rm Had}=2^{-1/2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}$ . For each natural $T$ and history $h:\{0,\ldots,T-1\}\to K$ , let $V_h$ successively apply $W_{h(j)}$ to the system and ancilla $j$ , and let $\widetilde V_h$ do the same with $(U\otimes1)W_{h(j)}(U^\dagger\otimes1)$ . Write $\omega_T=|-\rangle\langle-|^{\otimes T}$ , $X_h=V_h(\rho\otimes\omega_T)V_h^\dagger$ , $w_h=\prod_jp_{h(j)}$ , and $E'_a=(U\phi_a)(U\phi_a)^\dagger$ . The two matrices whose limits are asserted are

\begin{aligned} F_T&=\sum_h w_h\,\operatorname{tr}_{\rm anc} \!\left[\widetilde V_h^\dagger \left(E'_a\otimes \operatorname{tr}_{\rm sys}((E_a\otimes1)X_h(E_a\otimes1))\right) \widetilde V_h\right],\\ N_T&=\sum_h w_h\,\operatorname{tr}_{\rm anc} \!\left[((1-E_a)\otimes1)X_h((1-E_a)\otimes1)\right]. \end{aligned}

With $\|X\|_{\rm tr}=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ , the conclusion is

\lim_{T\to\infty}\|F_T-U(\Pi\rho\Pi)U^\dagger\|_{\rm tr}=0, \qquad \lim_{T\to\infty}\|N_T-(1-\Pi)\rho(1-\Pi)\|_{\rm tr}=0.

The histories and products are empty at $T=0$ ; no support condition on $\rho$ is assumed.

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