Theorem 5: unknown-projector outcome and nondisturbance bounds

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.theorem5_unknown_projector

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

prove2quantum

Take any finite nonempty family of unit sample vectors, with arbitrary overlaps and dependencies. Let $\Pi$ project onto their span, $\sigma_{\rm avg}=K^{-1}\sum_k|\phi_k\rangle\langle\phi_k|$ , and $\lambda_{\min}$ its minimum strictly positive eigenvalue. Use the Fig.7 history of $T\ge0$ independent uniform sample reflections, measure all-minus versus its complement, undo the same history, and let $\mathcal E_T$ ignore the outcome. The positive spectral support is nonempty and $0<\lambda_{\min}\le1$ . For every density input,

\operatorname{Tr}(\Pi\rho)-(1-\lambda_{\min})^T\le\Pr(b=0)\le\operatorname{Tr}(\Pi\rho).

If $[\Pi,\rho]=0$ , then also

F(\mathcal E_T(\rho),\rho)\ge1-(1-\lambda_{\min})^T.

Here $b=0$ is span detection and $b=1$ is all-minus. No algebra-generation promise is used.

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.32–34, Theorem 5: both probability and fidelity clauses. The commutation
hypothesis belongs only to fidelity; minPositiveEigenvalue excludes ambient zeros. -/
theorem theorem5_unknown_projector [Nonempty K] (phi : K → EuclideanSpace ℂ I)
    (hphi : ∀ k, IsState (phi k)) (T : ℕ) (rho : Matrix I I ℂ) (hrho : IsDensityMatrix rho) :
    let Pi := samplePi (pureSamples phi)
    let lam := minPositiveEigenvalue (meanSampleDensity phi)
    0 < lam ∧ lam ≤ 1 ∧
    (effectProb Pi rho - (1 - lam) ^ T ≤ (projectionBranch phi T false rho).trace.re ∧
      (projectionBranch phi T false rho).trace.re ≤ effectProb Pi rho) ∧
    (Pi * rho = rho * Pi → 1 - (1 - lam) ^ T ≤ rootFidelity (projectionChannel phi T rho) rho) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 32, Theorem 5: unknown-projector outcome and nondisturbance bounds

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 $\phi_k\in\mathbb C^I$ satisfy $\|\phi_k\|=1$ for every $k\in K$ ; let $T\ge0$ be a natural number; and let $\rho$ be positive semidefinite with $\operatorname{tr}\rho=1$ . Put $E_k=\phi_k\phi_k^\dagger$ , whose $(i,j)$ -entry is $\phi_k(i)\overline{\phi_k(j)}$ , and define $\Pi=f(\sum_kE_k)$ by continuous functional calculus, where $f(0)=0$ and $f(x)=1$ for $x\ne0$ . Let $\lambda$ be the smallest strictly positive eigenvalue of $|K|^{-1}\sum_kE_k$ , with value $0$ if there is no strictly positive eigenvalue. To specify the matrices in the conclusion, set $R_k=1-2E_k$ , let $C_k$ apply $R_k$ to the system when its Boolean ancilla is true and apply the identity when it is false, and write $\omega_T=|-\rangle\langle-|^{\otimes T}$ , where $|-\rangle=(|{\rm false}\rangle-|{\rm true}\rangle)/\sqrt2$ . For a history $h:\{0,\ldots,T-1\}\to K$ , let $V_h$ apply $C_{h(j)}$ to the system and ancilla $j$ , in increasing order of $j$ . Set $Q_{\rm true}=1\otimes\omega_T$ , $Q_{\rm false}=1-Q_{\rm true}$ , and

B_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].

Then the assertion is

0<\lambda\le1,\qquad \operatorname{Re}\operatorname{tr}(\Pi\rho)-(1-\lambda)^T \le\operatorname{Re}\operatorname{tr}B_{\rm false} \le\operatorname{Re}\operatorname{tr}(\Pi\rho),

together with the implication

\Pi\rho=\rho\Pi \quad\Longrightarrow\quad 1-(1-\lambda)^T \le \operatorname{Re}\operatorname{tr} \sqrt{\sqrt{B_{\rm false}+B_{\rm true}}\, \rho\, \sqrt{B_{\rm false}+B_{\rm true}}}.

The square roots use continuous functional calculus. The quantification includes $T=0$ , when the history is empty, $B_{\rm false}=0$ , and $B_{\rm true}=\rho$ ; the hypotheses cannot hold when $I$ is empty.

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