Example Eqs. (9)–(10): explicit PPT approximate private states

Open

QAlgorithms.Papers.Independent.Intakethird100.P09.ppt_private_bell_bound

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

prove2quantum

All states are normalized finite-dimensional bipartite density matrices. Gamma denotes transposition of Bob in the fixed product basis. The trace norm is the full trace norm. For a finite Bell expression S with real coefficients, C(S) and Q(S) are its largest signed classical value and its supremal signed quantum value over arbitrary finite local dimensions; Q_S(rho) optimizes complete local POVMs on the fixed state. Let d>=1 and let U=(u_ij) be a d-dimensional unitary with |u_ij|=1/sqrt(d). Define

X=\frac1{d\sqrt d}\sum_{i,j}u_{ij}|ij\rangle\langle ji|,\quad Y=\sqrt d\,X^\Gamma,\quad p=\frac1{\sqrt d+1},

\rho_p=(1-p)\gamma_X+\frac p2\bigl(|01\rangle\langle01|\otimes\sqrt{YY^\dagger}+|10\rangle\langle10|\otimes\sqrt{Y^\dagger Y}\bigr).

Regroup the registers as AA′:BB′. The constructed rho_p is a density matrix and is PPT. For every nonnegative-coefficient Bell expression,

Q_S(\rho_p)\le C(S)+\frac{Q(S)}{\sqrt d}.

The printed flat modulus 1/d is corrected to 1/sqrt(d), as required by unitarity and the named Fourier example. Density and PPT are conclusions, not premises. This supplies explicit weakly nonlocal PPT approximate private bits.

The fixed private-bit formula used here is

\gamma_X=\frac12\left(|00\rangle\langle00|\otimes\sqrt{XX^\dagger}+|00\rangle\langle11|\otimes X+|11\rangle\langle00|\otimes X^\dagger+|11\rangle\langle11|\otimes\sqrt{X^\dagger X}\right),

with the two key qubits and shields regrouped by owner.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P09

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P09

open scoped Matrix ComplexConjugate ComplexOrder ENNReal

open Filter

open QAlgorithms.Entanglement (IsSeparableDensity)

open QAlgorithms.Papers.Independent.Dependency50.P24
  (transposeSecond partyCut xForm swapPrivate hidingOne hidingTwo)

open QAlgorithms.Papers.Independent.Dependency50.P42 (dimensionedPower)

open QAlgorithms.Papers.Independent.Information100.P21 (Op FiniteLOCC)

open QAlgorithms.Papers.Independent.Information100.P56 (IsLaw)

open QAlgorithms.Papers.Independent.Advance50.P47 (Box)

open QAlgorithms.Papers.Independent.Information100.P54 (relativeEntanglement)

attribute [local instance] Classical.propDecidable

attribute [local instance] Classical.decEq

/-- PDF p.3, Eqs.(9)--(10): density and PPT are conclusions of the explicit construction.
CORRECTED flat modulus 1/sqrt(d), forced by unitarity; Bell domain corrected to s>=0. -/
theorem ppt_private_bell_bound (d : ℕ+) (U : Matrix.unitaryGroup (Fin d) ℂ)
    (hflat : ∀ i j, ‖(U : Op (Fin d)) i j‖ = (Real.sqrt d)⁻¹) :
    IsDensityMatrix (pptPrivate d U) ∧ (transposeSecond (pptPrivate d U)).PosSemidef ∧
    ∀ (S : BellScenario) (s : BellCoefficients S), (∀ x y a b, 0 ≤ s x y a b) →
      stateValue s (pptPrivate d U) ≤ classicalBound s + quantumBound s / Real.sqrt d := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P09

end

Source

Bounds on quantum nonlocality via partial transposition, arXiv:1407.6999v3, PDF p. 3, Example Eqs. (9)–(10): explicit PPT approximate private states

Read-back

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

Let $d$ be any positive integer and $U$ any $d\times d$ complex unitary matrix satisfying $|U_{ij}|=1/\sqrt d$ for every $i,j$ . On $\mathbb C^d\otimes\mathbb C^d$ , define $X_{(i,j),(k,l)}=U_{ij}/(d\sqrt d)$ when $(k,l)=(j,i)$ , and $0$ otherwise; put $Y=\sqrt d\,T_2(X)$ and $p=(\sqrt d+1)^{-1}$ , where $T_2(Z)_{(i,j),(k,l)}=Z_{(i,l),(k,j)}$ . Define $\Gamma$ on two parties of local dimension $2d$ by grouping their binary indices as a key and taking the nonzero key blocks to be

\Gamma_{00,00}=\frac{1-p}{2}\sqrt{XX^\dagger},\quad \Gamma_{11,11}=\frac{1-p}{2}\sqrt{X^\dagger X},\quad \Gamma_{00,11}=\frac{1-p}{2}X,\quad \Gamma_{11,00}=\frac{1-p}{2}X^\dagger,\quad \Gamma_{01,01}=\frac p2\sqrt{YY^\dagger},\quad \Gamma_{10,10}=\frac p2\sqrt{Y^\dagger Y}.

Then $\Gamma$ is positive semidefinite of trace $1$ , and its transpose on the entire second party, including both its binary and $d$ -dimensional coordinates, is positive semidefinite. Furthermore, for every Bell scenario with positive finite input and output sizes and every family $s_{xyab}\ge0$ , $V_s(\Gamma)\le C_s+Q_s/\sqrt d$ , where $V_s$ is the supremum of $\sum s_{xyab}\operatorname{Re}\operatorname{tr}((M_{a|x}\otimes N_{b|y})\Gamma)$ over local positive semidefinite measurement effects summing to the identity, $C_s=\sup_{f,g}\sum_{x,y}s_{xy,f(x),g(y)}$ , and $Q_s$ is the supremum of the measured expression over all positive finite local dimensions, density matrices, and local measurements. All square roots of matrices are given by functional calculus, and $d=1$ is included.

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