Theorem 3: generalized emulation fidelity and conditional fidelity

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.theorem3_generalized_fidelity

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

prove2quantum

Let $\Lambda$ be a finite nonempty parameter set with probability distribution $p$ , and let $W_{\rm in}(\lambda)$ be arbitrary system/one-qubit unitaries. Fix a unit anchor $\phi$ , an ambient unitary $U$ , and $T\ge0$ . Use independent parameters with law $p$ , $T$ ancillas initially in $\lvert-\rangle$ , output anchor $U\phi$ , and $W_{\rm out}(\lambda)=(U\otimes I)W_{\rm in}(\lambda)(U^\dagger\otimes I)$ . Let $\mathcal E_U$ and $\Sigma_U$ be the main and joint outputs of the four Appendix-A steps, ignoring the measurement label, and let $p_{\rm erase}(\rho)=\langle\phi|\mathcal W^T(\rho)|\phi\rangle$ . For every input density operator,

F(\Sigma_U(\rho),U\rho U^\dagger\otimes\lvert-\rangle\langle-\rvert^{\otimes T})\ge p_{\rm erase}(\rho),\qquad F(\mathcal E_U(\rho),U\rho U^\dagger)\ge p_{\rm erase}(\rho).

For a pure input and positive erasure probability, the normalized successful output has root fidelity at least $\sqrt{p_{\rm erase}(\rho)}$ with $U\rho U^\dagger$ . No supported-input or algebra-generation assumption is needed. These estimates include the working ancillas before tracing.

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.13–16, Theorem 3: root fidelity for actual Fig.5, including the joint
output and positive-probability pure-input conditional output. A1's missing adjoint is
corrected by Eq.(18) and A12; no algebra or input-support promise is assumed here. -/
theorem theorem3_generalized_fidelity [Nonempty L] (p : L → ℝ)
    (hp : QAlgorithms.Learning.IsDistribution p) (W : L → Matrix.unitaryGroup (I × Bool) ℂ)
    (phi : EuclideanSpace ℂ I) (hphi : IsState phi) (U : Matrix.unitaryGroup I ℂ) (T : ℕ) :
    (∀ rho, IsDensityMatrix rho →
      let joint := jointEmulator p (fun l => (W l : Matrix (I × Bool) (I × Bool) ℂ))
        (transportedGate (U : Matrix I I ℂ) (fun l => (W l : Matrix (I × Bool) (I × Bool) ℂ)))
        phi (act (U : Matrix I I ℂ) phi) T rho
      let pe := eraseProbability p (fun l => (W l : Matrix (I × Bool) (I × Bool) ℂ)) phi T rho
      pe ≤ rootFidelity joint (Matrix.kronecker (densityConjugation (U : Matrix I I ℂ) rho)
          (pureDensity (minusRegister T))) ∧
        pe ≤ rootFidelity (traceRight joint) (densityConjugation (U : Matrix I I ℂ) rho)) ∧
    (∀ psi : EuclideanSpace ℂ I, IsState psi →
      let pe := eraseProbability p (fun l => (W l : Matrix (I × Bool) (I × Bool) ℂ)) phi T (pureDensity psi)
      0 < pe → Real.sqrt pe ≤ rootFidelity
        ((pe : ℂ)⁻¹ • traceRight (jointBranch p (fun l => (W l : Matrix (I × Bool) (I × Bool) ℂ))
          (transportedGate (U : Matrix I I ℂ) (fun l => (W l : Matrix (I × Bool) (I × Bool) ℂ)))
          phi (act (U : Matrix I I ℂ) phi) T false (pureDensity psi)))
        (densityConjugation (U : Matrix I I ℂ) (pureDensity psi))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 13, Theorem 3: generalized emulation fidelity and conditional fidelity

Read-back

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

Let $I,L$ be finite types with decidable equality and $L\ne\varnothing$ , let $p:L\to\mathbb R$ satisfy $p_l\ge0$ and $\sum_lp_l=1$ , let each $W_l$ be unitary on $\mathbb C^I\otimes\mathbb C^2$ , let $\|\phi\|=1$ , let $U$ be unitary on $\mathbb C^I$ , and let $T$ be any natural number. Write $P_v=|v\rangle\langle v|$ , $\mu_T=P_{|-\rangle^{\otimes T}}$ , where $|-\rangle=(|0\rangle-|1\rangle)/\sqrt2$ , and define $\mathcal E(\rho)=\sum_lp_l\operatorname{Tr}_{\mathrm{anc}}[W_l(\rho\otimes P_{|-\rangle})W_l^\dagger]$ and $e_T(\rho)=\operatorname{Re}\operatorname{Tr}[P_\phi\mathcal E^T(\rho)]$ . For a history $h:\{0,\ldots,T-1\}\to L$ , put $p_h=\prod_{j<T}p_{h(j)}$ , let $H_h$ apply $W_{h(0)},\ldots,W_{h(T-1)}$ in that order, with gate $j$ acting on the system and ancilla $j$ while preserving the other ancillas, and put $H'_h=(U\otimes1)H_h(U^\dagger\otimes1)$ . For $b\in\{\mathrm{false},\mathrm{true}\}$ , set $Q_{\mathrm{false}}=P_\phi$ , $Q_{\mathrm{true}}=1-P_\phi$ , and

J_b(\rho)=\sum_h p_h\,H_h'{}^\dagger \left[ P_{U\phi}\otimes \operatorname{Tr}_{I}\!\left( (Q_b\otimes1)H_h(\rho\otimes\mu_T)H_h^\dagger(Q_b\otimes1)^\dagger \right) \right]H'_h,\qquad J(\rho)=J_{\mathrm{false}}(\rho)+J_{\mathrm{true}}(\rho).

Define $F(A,B)=\operatorname{Re}\operatorname{Tr}\sqrt{\sqrt A\,B\,\sqrt A}$ , with matrix square roots taken by real continuous functional calculus. The conclusion is the conjunction of two assertions: every positive semidefinite trace-one $\rho$ satisfies

e_T(\rho)\le F\!\left(J(\rho),\,U\rho U^\dagger\otimes\mu_T\right), \qquad e_T(\rho)\le F\!\left(\operatorname{Tr}_{\mathrm{anc}}J(\rho),\,U\rho U^\dagger\right);

and every norm-one vector $\psi$ for which $e=e_T(P_\psi)>0$ satisfies

\sqrt e\le F\!\left(e^{-1}\operatorname{Tr}_{\mathrm{anc}}J_{\mathrm{false}}(P_\psi), \,UP_\psi U^\dagger\right).

No sample-support or generation hypothesis is imposed. At $T=0$ , histories are empty, their weight is $1$ , their history matrices are identities, and $\mathcal E^0$ is the identity.

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