Lemma 8: corrected white-noise conversion criterion

Open

QAlgorithms.Papers.Independent.Intakethird100.P19.whiteNoise_conversion

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

prove2quantum

All Hilbert spaces are finite-dimensional complex spaces with fixed product bases and positive local dimensions. States are positive semidefinite operators of trace one; pure kets have norm one. Let $k,d\ge2$ , with pure states $\psi$ on $k\times k$ and $\varphi$ on $d\times d$ , and decreasing squared Schmidt coefficients $\lambda_i,\mu_i$ . Define

\Lambda(X)=\operatorname{Tr}(\psi X)\varphi+\operatorname{Tr}((I_{k^2}-\psi)X)\frac{I_{d^2}}{d^2}.

This is a channel and is non-entangling if $(1+d^2\sqrt{\mu_1\mu_2})\lambda_1\le1$ . Under this condition it is also dually non-entangling if

(d^2\mu_1-1)\sqrt{\lambda_1\lambda_2}\le1.

Dually non-entangling means that both the channel and its trace dual preserve separable positive operators.

The cross-multiplied inequalities retain product-state cases.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P19

Formal statement

noncomputable section

open QAlgorithms QAlgorithms.Entanglement Filter

open scoped Matrix ComplexOrder ComplexConjugate ENNReal

attribute [local instance] Classical.propDecidable Classical.decEq

namespace QAlgorithms.Papers.Independent.Intakethird100.P19

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

open QAlgorithms.Papers.Independent.Information100.P19 (Bip)

open QAlgorithms.Papers.Independent.Information100.P69 (CP)

open QAlgorithms.Papers.Independent.Information100.P71 (supportPower SupportIncluded)

open QAlgorithms.Papers.Independent.Dependency50.P19 (epr)

/-- Lemma 8, PDF pp.11-12, corrected from its proof: printed Eq.(8)
omits 1+ in the denominator. Use (1+d^2 sqrt(mu_1 mu_2))*lambda_1<=1.
Eq.(9) is cross-multiplied to include zero second Schmidt coefficients.
The printed Bell-to-Bell case violates PPT preservation of separable inputs. -/
theorem whiteNoise_conversion {k d : ℕ} (hk : 2 ≤ k) (hd : 2 ≤ d)
    (psi : UnitBipartiteKet k k) (phi : UnitBipartiteKet d d)
    (hfirst : (1 + (d : ℝ) ^ 2 * Real.sqrt (schmidtAt phi.ket 0 * schmidtAt phi.ket 1)) *
      schmidtAt psi.ket 0 ≤ 1) :
    let L := binaryMeasurePrepare psi.rho phi.rho (((d : ℂ) ^ 2)⁻¹ • (1 : Bip d d))
    IsChannel L ∧ NE L ∧
      (((d : ℝ) ^ 2 * schmidtAt phi.ket 0 - 1) *
        Real.sqrt (schmidtAt psi.ket 0 * schmidtAt psi.ket 1) ≤ 1 → DNE L) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P19

end

Source

Entanglement manipulation and distillability beyond LOCC, arXiv:1711.03835v2, PDF p. 11, Lemma 8

Read-back

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

For all natural numbers $k,d\ge2$ and unit vectors $\psi\in\mathbb C^k\otimes\mathbb C^k$ and $\phi\in\mathbb C^d\otimes\mathbb C^d$ , let $P_\psi=|\psi\rangle\langle\psi|$ and $P_\phi=|\phi\rangle\langle\phi|$ . For either vector $v$ , let $\lambda_0(v)$ and $\lambda_1(v)$ be the largest and second-largest eigenvalues, counting multiplicities, of its first marginal $(\sum_jv_{ij}\overline{v_{i'j}})_{i,i'}$ ; these include zero eigenvalues. If $(1+d^2\sqrt{\lambda_0(\phi)\lambda_1(\phi)})\lambda_0(\psi)\le1$ , define the map $L$ on every input operator by $L(X)=\operatorname{Tr}(P_\psi X)P_\phi+\operatorname{Tr}((I-P_\psi)X)I_{d^2}/d^2$ . Then $L$ is a channel and is non-entangling. Moreover, if $(d^2\lambda_0(\phi)-1)\sqrt{\lambda_0(\psi)\lambda_1(\psi)}\le1$ , then both $L$ and its trace-bilinear dual are non-entangling. Here a channel has a finite Kraus representation $L(X)=\sum_jE_jXE_j^\dagger$ with $\sum_jE_j^\dagger E_j=I$ ; a non-entangling map has a finite Kraus representation, without a normalization requirement, and preserves the cone of finite nonnegative sums of tensor products of positive semidefinite trace-one matrices, including the empty sum. The trace-bilinear dual is defined entrywise by $(L^\vee(Y))_{ij}=\operatorname{Tr}(L(E_{ji})Y)$ , where $E_{ji}$ is the input matrix unit.

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