Prove2Me

§III B, Eq.(27), Appendix B1: spectral error bound

Open
QAlgorithms.Papers.Independent.Intakethird100.P67.ideal_spectral_error

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

prove2quantum

Let normalized pure samples, K≥2K\ge2, generate all operators on their span, of dimension dd, and fix an anchor. Let λ⊥\lambda_\perp be the norm of the vectorized compressed reflection channel. Then 0≤λ⊥<10\le\lambda_\perp<1. For every supported input density operator, every ambient target unitary, and every integer T≥1T\ge1, the ideal averaged emulator obeys

F(EU(ρ),UρU†)≥1−d−1 λ⊥T.F(\mathcal E_U(\rho),U\rho U^\dagger)\ge1-\sqrt{d-1}\,\lambda_\perp^T.

If d≥2d\ge2, 0<ϵid<10<\epsilon_{\rm id}<1, and T≥1T\ge1 satisfies

T≥log⁡(2ϵid−2(d−1))1−λ⊥,T\ge\frac{\log(2\epsilon_{\rm id}^{-2}(d-1))}{1-\lambda_\perp},

then its trace distance from the target is at most ϵid\epsilon_{\rm id}. At d=1d=1 the zero-round anchor preparation is already exact for supported inputs. The formula avoids log⁡λ⊥\log\lambda_\perp and remains meaningful when λ⊥=0\lambda_\perp=0. This separates ideal convergence from sample-based reflection errors.

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.7,17–18, Eq.(27)/B18: the spectral gap is a conclusion, not a premise.
B12 has sqrt(d-1); B14 is its weaker d>=2 corollary. T>=1 handles lambda=0, and
rank one is separated from the logarithm. -/
theorem ideal_spectral_error (phi : K → EuclideanSpace ℂ I) (a : K)
    (hK : 2 ≤ Fintype.card K) (hphi : ∀ k, IsState (phi k))
    (hgen : Generates (pureSamples phi)) :
    0 ≤ lambdaPerp phi a ∧ lambdaPerp phi a < 1 ∧
    (∀ (U : Matrix.unitaryGroup I ℂ) (rho : Matrix I I ℂ), IsDensityMatrix rho →
      InSampleSupport (pureSamples phi) rho → ∀ T : ℕ, 1 ≤ T →
      1 - Real.sqrt (sampleDimension (pureSamples phi) - 1 : ℝ) * lambdaPerp phi a ^ T ≤
        rootFidelity (emulate phi a (U : Matrix I I ℂ) T rho) (densityConjugation (U : Matrix I I ℂ) rho)) ∧
    (∀ (U : Matrix.unitaryGroup I ℂ) (rho : Matrix I I ℂ), IsDensityMatrix rho →
      InSampleSupport (pureSamples phi) rho → ∀ eps : ℝ, 0 < eps → eps < 1 →
      2 ≤ sampleDimension (pureSamples phi) → ∀ T : ℕ, 1 ≤ T →
      Real.log (2 * eps⁻¹ ^ 2 * (sampleDimension (pureSamples phi) - 1 : ℝ)) /
        (1 - lambdaPerp phi a) ≤ T →
      traceDistance (emulate phi a (U : Matrix I I ℂ) T rho) (densityConjugation (U : Matrix I I ℂ) rho) ≤ eps) ∧
    (sampleDimension (pureSamples phi) = 1 →
      ∀ (U : Matrix.unitaryGroup I ℂ) (rho : Matrix I I ℂ), IsDensityMatrix rho →
        InSampleSupport (pureSamples phi) rho → emulate phi a (U : Matrix I I ℂ) 0 rho = densityConjugation (U : Matrix I I ℂ) rho) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end
Source
Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 7, §III B, Eq.(27), Appendix B1: spectral error bound
Read-back

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

Let II and KK be finite index types with decidable equality, let ∣K∣≥2|K|\ge2, let ϕk∈CI\phi_k\in\mathbb C^I have norm 11 for every k∈Kk\in K, and fix a∈Ka\in K. Write Pk=ϕkϕk†P_k=\phi_k\phi_k^\dagger, and let Π\Pi be the matrix obtained by applying the function x↦0x\mapsto 0 for x=0x=0 and x↦1x\mapsto1 otherwise to ∑kPk\sum_kP_k by functional calculus. Assume that the complex span of all nonempty products Pk1⋯PksP_{k_1}\cdots P_{k_s} is exactly {X:ΠXΠ=X}\{X:\Pi X\Pi=X\}. Put d=rank⁡Πd=\operatorname{rank}\Pi, Q=Π−PaQ=\Pi-P_a, Rk=1−2PkR_k=1-2P_k, Ck=QRkQC_k=QR_kQ, and pk=0p_k=0 if k=ak=a, otherwise pk=(∣K∣−1)−1p_k=(|K|-1)^{-1}, and define

λ=∥∑kpk Ck⊗Ck‾∥op,\lambda=\left\|\sum_kp_k\,C_k\otimes\overline{C_k}\right\|_{\mathrm{op}},

where the bar denotes entrywise conjugation and the norm is the Euclidean operator norm. To specify the matrix map occurring in the conclusions, let C(V)=1I⊗∣0⟩⟨0∣+V⊗∣1⟩⟨1∣C(V)=1_I\otimes|0\rangle\langle0|+V\otimes|1\rangle\langle1|, let H=2−1/2(111−1)H=2^{-1/2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}, and put Ek=C(Rk)(1I⊗H)C(Ra)E_k=C(R_k)(1_I\otimes H)C(R_a). For a history h∈KTh\in K^T, let Vh=EhT−1(T−1)⋯Eh0(0)V_h=E_{h_{T-1}}^{(T-1)}\cdots E_{h_0}^{(0)}, where the superscript indicates the ancilla qubit acted on, and let VU,hV_{U,h} be the same product with every EkE_k replaced by (U⊗12)Ek(U†⊗12)(U\otimes1_2)E_k(U^\dagger\otimes1_2). Set ηT=∣−⟩⊗T\eta_T=|-\rangle^{\otimes T}, where ∣−⟩=(∣0⟩−∣1⟩)/2|-\rangle=(|0\rangle-|1\rangle)/\sqrt2, Xh=Vh(ρ⊗ηTηT†)Vh†X_h=V_h(\rho\otimes\eta_T\eta_T^\dagger)V_h^\dagger, and Pfalse=Pa, Ptrue=1−PaP_{\mathrm{false}}=P_a,\ P_{\mathrm{true}}=1-P_a; then the emulator is the explicitly defined map

Eϕ,a,UT(ρ)=Tr⁡anc∑h∈KT(∏j<Tphj)∑b∈{false,true}VU,h†[UPaU†⊗Tr⁡I ⁣((Pb⊗1)Xh(Pb⊗1))]VU,h.\mathcal E_{\phi,a,U}^T(\rho)= \operatorname{Tr}_{\mathrm{anc}} \sum_{h\in K^T}\left(\prod_{j<T}p_{h_j}\right) \sum_{b\in\{\mathrm{false},\mathrm{true}\}} V_{U,h}^\dagger \left[ UP_aU^\dagger\otimes \operatorname{Tr}_{I}\!\left((P_b\otimes1)X_h(P_b\otimes1)\right) \right]V_{U,h}.

Here partial traces sum the diagonal indices of the indicated register, and empty history products are identities. The assertion is that 0≤λ<10\le\lambda<1; that for every unitary UU, every positive semidefinite ρ\rho of trace 11 satisfying ΠρΠ=ρ\Pi\rho\Pi=\rho, and every integer T≥1T\ge1,

1−d−1 λT≤Fr ⁣(Eϕ,a,UT(ρ),UρU†);1-\sqrt{d-1}\,\lambda^T \le F_{\mathrm r}\!\left(\mathcal E_{\phi,a,U}^T(\rho),U\rho U^\dagger\right);

that for every such U,ρU,\rho, every 0<ε<10<\varepsilon<1, and every integer T≥1T\ge1, if d≥2d\ge2 and

log⁡ ⁣(2ε−2(d−1))1−λ≤T,\frac{\log\!\left(2\varepsilon^{-2}(d-1)\right)}{1-\lambda}\le T,

then D(Eϕ,a,UT(ρ),UρU†)≤εD(\mathcal E_{\phi,a,U}^T(\rho),U\rho U^\dagger)\le\varepsilon; and that if d=1d=1, then Eϕ,a,U0(ρ)=UρU†\mathcal E_{\phi,a,U}^{0}(\rho)=U\rho U^\dagger for every such U,ρU,\rho. The distances here mean

Fr(A,B)=Re⁡tr⁡A BA,D(A,B)=12Re⁡tr⁡(A−B)†(A−B),F_{\mathrm r}(A,B)=\operatorname{Re}\operatorname{tr}\sqrt{\sqrt A\,B\sqrt A}, \qquad D(A,B)=\tfrac12\operatorname{Re}\operatorname{tr}\sqrt{(A-B)^\dagger(A-B)},

with square roots supplied by functional calculus; the subtraction d−1d-1 inside the real expressions is real subtraction.

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