Exact and robust self-testing of entangled two-qubit states

Open

QAlgorithms.Papers.Independent.Intakethird100.P75.bell_exact_and_robust

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

prove2quantum

Let $0\leq\theta\leq\pi/4$ . Define the unit target and Bell parameter by

|\psi_\theta\rangle=\cos\theta|00\rangle+\sin\theta|11\rangle,\qquad \alpha(\theta)=\frac{2\cos(2\theta)}{\sqrt{1+\sin^2(2\theta)}},\qquad b(\alpha)=\sqrt{8+2\alpha^2}.

Then $0\leq\alpha(\theta)\leq2$ . The concrete qubit strategy $A_0=Z,A_1=X$ , $B_0=\cos\mu Z+\sin\mu X,B_1=\cos\mu Z-\sin\mu X$ , with Pauli matrices $X,Z$ and $\mu=\arctan(\sin(2\theta))$ , consists of dichotomic observables and attains $b(\alpha(\theta))$ on this target.

Let $H_A,H_B$ be arbitrary complex Hilbert spaces, $|\psi'\rangle$ a unit vector in their completed Hilbert tensor product, and $A_0,A_1,B_0,B_1$ bounded self-adjoint involutions on the indicated local spaces. Set

\mathcal B_\alpha=\alpha A_0\otimes I+ A_0\otimes(B_0+B_1)+A_1\otimes(B_0-B_1).

If its expectation on $\psi'$ equals $b(\alpha(\theta))$ , there exist local complex-linear isometric embeddings $\Phi_A,\Phi_B$ and normalized, possibly entangled junk with

(\Phi_A\otimes\Phi_B)|\psi'\rangle =|\mathrm{junk}\rangle\otimes|\psi_\theta\rangle.

For each fixed $0<\theta\leq\pi/4$ , for every $\eta>0$ there is a $\delta>0$ , depending only on $\theta,\eta$ , such that every realization above with Bell expectation at least $b(\alpha(\theta))-\delta$ admits such embeddings and junk satisfying

\|(\Phi_A\otimes\Phi_B)|\psi'\rangle- |\mathrm{junk}\rangle\otimes|\psi_\theta\rangle\|\leq\eta.

Equalities and norms use one fixed regrouping of physical and added registers. This certifies the state, without a measurement-intertwining claim. The endpoint $\theta=0,\alpha=2$ is retained in the exact clause as product extraction.

Formalization Note The printed tangent relation is corrected to a double-angle relation via the continuous parameter formula above. In particular, $\alpha=0$ gives $\theta=\pi/4$ . The qualitative robustness clause does not assert the defective explicit coefficients.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P75

Formal statement

noncomputable section

open scoped BigOperators

namespace QAlgorithms.Papers.Independent.Intakethird100.P75

universe u v w x

open QAlgorithms.Papers.Independent.Claimed50.P34 (HilbertTensor)

open QAlgorithms.Papers.Independent.Renew46.P03 (tensorVector)

/-- PDF pp.2–3, unnumbered Theorem, with robustness in the sense of (3).
The printed Schmidt relation is corrected as documented at tiltParameter.
The ideal qubit strategy realizes every target nonvacuously. Exact extraction
includes theta=0,alpha=2 as the product branch. Robustness is fixed-theta and
uniform over arbitrary physical Hilbert spaces and all dichotomic observables.
No measurement-intertwining conclusion or invalid (19)–(20) estimate is added. -/
theorem bell_exact_and_robust (theta : ℝ) (htheta : 0 ≤ theta)
    (hthetaUpper : theta ≤ Real.pi / 4) :
    0 ≤ tiltParameter theta ∧ tiltParameter theta ≤ 2 ∧
    ‖schmidtTarget (qubitCoefficients theta)‖ = 1 ∧
    Dichotomic idealZ ∧ Dichotomic idealX ∧
    Dichotomic (idealB0 theta) ∧ Dichotomic (idealB1 theta) ∧
    bellValue (tiltParameter theta) idealZ idealX (idealB0 theta) (idealB1 theta)
      (schmidtTarget (qubitCoefficients theta)) = quantumMaximum (tiltParameter theta) ∧
    (∀ (H : Type u) (K : Type v)
      [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
      [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
      (psi : HilbertTensor H K) (A0 A1 : H →L[ℂ] H) (B0 B1 : K →L[ℂ] K),
      ‖psi‖ = 1 → Dichotomic A0 → Dichotomic A1 → Dichotomic B0 → Dichotomic B1 →
      bellValue (tiltParameter theta) A0 A1 B0 B1 psi =
        quantumMaximum (tiltParameter theta) →
      ExtractsWithin (qubitCoefficients theta) psi 0) ∧
    (0 < theta → ∀ eta : ℝ, 0 < eta → ∃ delta : ℝ, 0 < delta ∧
      ∀ (H : Type u) (K : Type v)
      [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
      [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
      (psi : HilbertTensor H K) (A0 A1 : H →L[ℂ] H) (B0 B1 : K →L[ℂ] K),
      ‖psi‖ = 1 → Dichotomic A0 → Dichotomic A1 → Dichotomic B0 → Dichotomic B1 →
      quantumMaximum (tiltParameter theta) - delta ≤
        bellValue (tiltParameter theta) A0 A1 B0 B1 psi →
      ExtractsWithin (qubitCoefficients theta) psi eta) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P75

end

Source

Robust Self Testing of Unknown Quantum Systems into Any Entangled Two-Qubit States, arXiv:1210.4409v2, PDF p. 2, §III, unnumbered Theorem: exact and robust self-testing of every pure entangled two-qubit state

Read-back

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

For every real $\theta$ satisfying $0\le\theta\le\pi/4$ , put $\alpha=2\cos(2\theta)/\sqrt{1+\sin^2(2\theta)}$ , $\mu=\arctan(\sin(2\theta))$ , $Z=\operatorname{diag}(1,-1)$ , $X=\begin{pmatrix}0&1\\1&0\end{pmatrix}$ , $B_0=\cos\mu\,Z+\sin\mu\,X$ , $B_1=\cos\mu\,Z-\sin\mu\,X$ , and $\phi_\theta=\cos\theta\,e_0\otimes e_0+\sin\theta\,e_1\otimes e_1$ , where $e_0,e_1$ are the standard vectors indexed by $\mathrm{false},\mathrm{true}$ . All tensor products here are completed complex Hilbert tensor products, namely completions of the algebraic tensor products, and tensor products of operators denote the continuous extensions of their actions on elementary tensors. The statement asserts $0\le\alpha\le2$ , $\|\phi_\theta\|=1$ , and that each of $Z,X,B_0,B_1$ is self-adjoint and has square equal to the identity. Define

\mathcal B_\alpha(A_0,A_1,C_0,C_1) =\alpha A_0\otimes I+A_0\otimes(C_0+C_1)+A_1\otimes(C_0-C_1).

Then $\operatorname{Re}\langle\phi_\theta,\mathcal B_\alpha(Z,X,B_0,B_1)\phi_\theta\rangle=\sqrt{8+2\alpha^2}$ . Moreover, for every pair of complete complex normed inner product spaces $H,K$ , every $\psi\in H\widehat\otimes K$ with $\|\psi\|=1$ , and every continuous complex-linear $A_0,A_1:H\to H$ and $C_0,C_1:K\to K$ that are self-adjoint and square to the identity, equality $\operatorname{Re}\langle\psi,\mathcal B_\alpha(A_0,A_1,C_0,C_1)\psi\rangle=\sqrt{8+2\alpha^2}$ implies that there exist continuous complex-linear isometries $F_A:H\to H\widehat\otimes\mathbb C^2$ and $F_B:K\to K\widehat\otimes\mathbb C^2$ and a vector $J\in H\widehat\otimes K$ with $\|J\|=1$ such that $(F_A\otimes F_B)\psi=\cos\theta\,T_0J+\sin\theta\,T_1J$ , where $T_b$ is the continuous extension of $h\otimes k\mapsto(h\otimes e_b)\otimes(k\otimes e_b)$ . Finally, if $\theta>0$ , then for every real $\eta>0$ there exists a real $\delta>0$ such that, uniformly for all such $H,K,\psi,A_0,A_1,C_0,C_1$ , the inequality $\sqrt{8+2\alpha^2}-\delta\le\operatorname{Re}\langle\psi,\mathcal B_\alpha(A_0,A_1,C_0,C_1)\psi\rangle$ implies the existence of such isometries and unit vector $J$ satisfying $\|(F_A\otimes F_B)\psi-\cos\theta\,T_0J-\sin\theta\,T_1J\|\le\eta$ . The exact assertion includes $\theta=0$ ; the final robustness assertion is conditional on $\theta>0$ .

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