§III C, Eqs.(30)–(31): two-dimensional example and information gap

Open

QAlgorithms.Papers.Independent.Intakethird100.P67.two_sample_gap

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

prove2quantum

Let two unit sample vectors have overlap magnitude $\cos(\theta/2)$ with $0<\theta<\pi$ . They span a two-dimensional input space. With the first sample as anchor, put $P=\lvert\phi_1\rangle\langle\phi_1\rvert$ and $Q=\Pi_{\rm in}-P$ . Then

\lambda_\perp=\cos^2\theta,\qquad \mathcal D_\perp(X)=\cos^2\theta\,QXQ,\qquad F(\mathcal E_U(\rho),U\rho U^\dagger)\ge1-(\cos\theta)^{2T}.

The fidelity bound holds for every supported density operator, target unitary and $T\ge0$ . For $U(\alpha)=\exp(i\alpha P)$ , $0\le\alpha<2\pi$ , the pure output family from the second sample has quantum Fisher information

I_\alpha=4\bigl(\langle P^2\rangle_{\phi_2}-\langle P\rangle_{\phi_2}^2\bigr)=1-\lambda_\perp.

The identity links distinguishability to convergence. The identical-sample endpoint is not assigned dimension two.

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–8, Eqs.(30)–(31): two-dimensional fidelity, compressed channel, and
quantum Fisher information (four times generator variance). The dimension-two promise
is made only for the strict interior overlap regime. -/
theorem two_sample_gap (phi : Fin 2 → EuclideanSpace ℂ I) (hphi : ∀ k, IsState (phi k))
    (theta : ℝ) (htheta : 0 < theta ∧ theta < Real.pi)
    (hoverlap : ‖inner ℂ (phi 0) (phi 1)‖ = Real.cos (theta / 2)) :
    lambdaPerp phi 0 = Real.cos theta ^ 2 ∧
    (∀ X : Matrix I I ℂ, let Q := samplePi (pureSamples phi) - pureDensity (phi 0)
      compressedReflectionChannel phi 0 X = (Real.cos theta ^ 2 : ℂ) • (Q * X * Q)) ∧
    (∀ (U : Matrix.unitaryGroup I ℂ) (rho : Matrix I I ℂ), IsDensityMatrix rho →
      InSampleSupport (pureSamples phi) rho → ∀ T : ℕ,
      1 - Real.cos theta ^ (2 * T) ≤
        rootFidelity (emulate phi 0 (U : Matrix I I ℂ) T rho) (densityConjugation (U : Matrix I I ℂ) rho)) ∧
    (∀ alpha : ℝ, 0 ≤ alpha → alpha < 2 * Real.pi →
      let family := fun t : ℝ => act (positivePhaseEvolution (pureDensity (phi 0)) t) (phi 1)
      let variance := (inner ℂ (phi 1) (act (pureDensity (phi 0) * pureDensity (phi 0)) (phi 1))).re -
        ((inner ℂ (phi 1) (act (pureDensity (phi 0)) (phi 1))).re) ^ 2
      DifferentiableAt ℝ family alpha ∧
        pureFisherInformation family alpha = 4 * variance ∧ 4 * variance = 1 - lambdaPerp phi 0) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P67

end

Source

Universal Quantum Emulator, arXiv:1606.02734v2, PDF p. 7, §III C, Eqs.(30)–(31): two-dimensional example and information gap

Read-back

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

Let $I$ be a finite index type with decidable equality, let $\phi_0,\phi_1\in\mathbb C^I$ both have norm $1$ , and let $0<\theta<\pi$ satisfy $|\langle\phi_0,\phi_1\rangle|=\cos(\theta/2)$ . Put $P_k=\phi_k\phi_k^\dagger$ , let $\Pi$ be the functional-calculus value of $x\mapsto\mathbf1_{x\ne0}$ on $P_0+P_1$ , and set $Q=\Pi-P_0$ , $R_k=1-2P_k$ , and $C_k=QR_kQ$ . The compressed-reflection map is $\mathcal C(X)=C_1XC_1$ , and the parameter in the statement is $\lambda=\|C_1\otimes\overline{C_1}\|_{\mathrm{op}}$ , with Euclidean operator norm and entrywise conjugation. Define $C(V)=1_I\otimes|0\rangle\langle0|+V\otimes|1\rangle\langle1|$ , $H=2^{-1/2}\begin{pmatrix}1&1\\1&-1\end{pmatrix}$ , and $E=C(R_1)(1_I\otimes H)C(R_0)$ . For $T\ge0$ , let $V_T=E^{(T-1)}\cdots E^{(0)}$ , where the factors act on distinct ancilla qubits, let $V_{U,T}$ use $(U\otimes1_2)E(U^\dagger\otimes1_2)$ in place of $E$ , put $\eta_T=((|0\rangle-|1\rangle)/\sqrt2)^{\otimes T}$ , and set $X_T=V_T(\rho\otimes\eta_T\eta_T^\dagger)V_T^\dagger$ . With $P_{\mathrm{false}}=P_0$ and $P_{\mathrm{true}}=1-P_0$ , define

\mathcal E_U^T(\rho)= \operatorname{Tr}_{\mathrm{anc}} \sum_bV_{U,T}^\dagger \left[ UP_0U^\dagger\otimes \operatorname{Tr}_{I}\!\left((P_b\otimes1)X_T(P_b\otimes1)\right) \right]V_{U,T}.

This is the stated emulator: its history weights assign probability $0$ to sample $0$ and probability $1$ to sample $1$ ; empty products are identities. The conclusions are $\lambda=\cos^2\theta$ and, for every complex matrix $X$ , $\mathcal C(X)=\cos^2\theta\,QXQ$ ; moreover, for every unitary $U$ , every positive semidefinite $\rho$ of trace $1$ satisfying $\Pi\rho\Pi=\rho$ , and every natural number $T$ , including $T=0$ ,

1-\cos^{2T}\theta \le \operatorname{Re}\operatorname{tr} \sqrt{\sqrt{\mathcal E_U^T(\rho)}\,U\rho U^\dagger \sqrt{\mathcal E_U^T(\rho)}}.

Finally, for every $0\le\alpha<2\pi$ , the vector-valued function $v(t)=e^{itP_0}\phi_1$ is differentiable at $\alpha$ , and, writing

\operatorname{Var} =\operatorname{Re}\langle\phi_1,P_0^2\phi_1\rangle -\bigl(\operatorname{Re}\langle\phi_1,P_0\phi_1\rangle\bigr)^2,

one has

4\!\left(\|v'(\alpha)\|^2- |\langle v(\alpha),v'(\alpha)\rangle|^2\right) =4\operatorname{Var} =1-\lambda.

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