Appendix H1–H2: asymptotic projective instrument

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.projective_measurement_limit

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

prove2quantum

For an arbitrary finite nonempty normalized sample family, let $\Pi$ project onto its span and let $\mathcal E_{T,0},\mathcal E_{T,1}$ be the actual subnormalized branches of the Fig.7 instrument with ideal controlled reflections. For every input density operator,

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

Thus the limiting outcome probabilities and conditional states are those of the projective measurement. Subnormalized branches remain defined when a Born probability is zero; no normalization of an impossible conditioned event or new diamond-norm rate is asserted.

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.31–32: convergence to the two subnormalized projective branches, including
zero Born probability, with b=0 for span detection and b=1 for its complement. -/
theorem projective_measurement_limit [Nonempty K] (phi : K → EuclideanSpace ℂ I)
    (hphi : ∀ k, IsState (phi k)) (rho : Matrix I I ℂ) (hrho : IsDensityMatrix rho) :
    let Pi := samplePi (pureSamples phi)
    Tendsto (fun T : ℕ => traceNorm (projectionBranch phi T false rho - Pi * rho * Pi)) atTop (nhds 0) ∧
    Tendsto (fun T : ℕ => traceNorm (projectionBranch phi 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. 32, Appendix H1–H2: asymptotic projective instrument

Read-back

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

Let $I$ and $K$ be finite index types with decidable equality, with $K$ nonempty, let each $\phi_k\in\mathbb C^I$ have norm $1$ , and let $\rho$ be positive semidefinite with trace $1$ . Define $E_k=\phi_k\phi_k^\dagger$ and $\Pi=f(\sum_kE_k)$ , where $f(0)=0$ , $f(x)=1$ for $x\ne0$ , and the function is applied by continuous functional calculus. For each natural number $T$ , let $\omega_T=|-\rangle\langle-|^{\otimes T}$ , with $|-\rangle=(|{\rm false}\rangle-|{\rm true}\rangle)/\sqrt2$ ; for each history $h:\{0,\ldots,T-1\}\to K$ , let $V_h$ successively apply $1-2E_{h(j)}$ to the system controlled by ancilla $j$ , in increasing order of $j$ . Define $Q_{\rm true}=1\otimes\omega_T$ , $Q_{\rm false}=1-Q_{\rm true}$ , and

B_{T,b}=|K|^{-T}\sum_h \operatorname{tr}_{\rm anc}\!\left[ V_h^\dagger Q_bV_h(\rho\otimes\omega_T) V_h^\dagger Q_bV_h\right].

Writing $\|X\|_{\rm tr}=\operatorname{Re}\operatorname{tr}\sqrt{X^\dagger X}$ , with the square root given by continuous functional calculus, both limits hold:

\lim_{T\to\infty}\|B_{T,{\rm false}}-\Pi\rho\Pi\|_{\rm tr}=0, \qquad \lim_{T\to\infty} \|B_{T,{\rm true}}-(1-\Pi)\rho(1-\Pi)\|_{\rm tr}=0.

The limits run through all natural $T$ , including the empty-history construction at $T=0$ ; the hypotheses cannot hold for empty $I$ .

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