Universal output-entanglement cap for phase-insensitive channels

Open

QAlgorithms.Papers.Independent.Intakethird100.P89.universalOutputEntanglementCap

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

prove2quantum

Let $r\ge0$ , $\tau\ge0$ , and let $\Phi$ be a zero-displacement phase-insensitive Gaussian channel on a complete oscillator, with noise $y\ge|1-\tau|$ . For every normalized trace-class two-oscillator input $\rho$ , apply $\Phi$ to the first oscillator and the identity to the second. Partial transpose is taken in the number basis, and the trace norm has values in $[0,\infty]$ . Then

y\ge e^{-2r}(1+\tau)\quad\Longleftrightarrow\quad\forall\rho,\ \bigl\|[(\Phi\otimes\mathrm{id})(\rho)]^\Gamma\bigr\|_1\le e^{2r}.

Equivalently, membership in the physical closed region defined by (3) and (8) is precisely this universal cap. At $r=0$ its scalar threshold becomes $y\ge1+\tau$ , the entanglement-breaking threshold (4).

This statement tests all input densities, including non-Gaussian and infinite-energy ones. The closed region includes ideal boundary limits; it is not asserted to be the finite-energy realization set.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P89

Formal statement

noncomputable section

open MeasureTheory Filter

open scoped BigOperators ENNReal Topology ComplexOrder

attribute [local instance] Classical.propDecidable Classical.decEq

namespace QAlgorithms.Papers.Independent.Intakethird100.P89

open QAlgorithms.Papers.Independent.Dependency50.P33
  (State IsDensity IsTraceClassChannel tensorApply traceSize)

open QAlgorithms.Papers.Independent.Dependency50.P39
  (coherentKet coherentCoefficient operatorOfMatrix husimiQ HasFockMatrix CoherentRealized)

open QAlgorithms.Papers.Independent.Frontier30.P14 (weylCharacteristic)

open QAlgorithms.Papers.Independent.Claimed50.P19
  (Cov FockIndex DensityKernel PhysicalCovariance CharacteristicSummable
   multimodeWeylTrace covarianceCharacteristicValue standardFormCovariance)

open QAlgorithms.Papers.Independent.Frontier30.P08 (QuadratureIndex)

open QAlgorithms.Papers.Independent.Gap48.P26 (PhaseInsensitive coherentKernel)

open QAlgorithms.Entanglement (partialTransposeFirst)

/-- PDF p.3, (8): universal output cap on ALL normalized two-mode states,
not just Gaussian tests. Infinity of partial-transpose trace norm is preserved.
At r=0 the same condition is the entanglement-breaking noise threshold (4). -/
theorem universalOutputEntanglementCap (r tau y : ℝ) (Phi : OscillatorChannel)
    (hr : 0 ≤ r) (htau : 0 ≤ tau) (hPhi : PhaseInsensitive Phi tau y) :
    (Real.exp (-2 * r) * (1 + tau) ≤ y ↔
      ∀ rho : State (ℕ × ℕ),
        traceSize (partialTransposeFirst (tensorApply Phi rho.coefficients)) ≤
          ENNReal.ofReal (Real.exp (2 * r))) ∧
    ((tau, y) ∈ entanglementAccessibleRegion r ↔
      ∀ rho : State (ℕ × ℕ),
        traceSize (partialTransposeFirst (tensorApply Phi rho.coefficients)) ≤
          ENNReal.ofReal (Real.exp (2 * r))) ∧
    (Real.exp (-2 * (0 : ℝ)) * (1 + tau) ≤ y ↔ 1 + tau ≤ y) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P89

end

Source

Optimal continuous variable quantum teleportation with limited resources, arXiv:1705.03017v5, PDF p. 3, Implementable channels and universal output-entanglement cap, Eq. (8)

Read-back

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

Let $r,\tau,y\in\mathbb R$ with $r\ge0$ and $\tau\ge0$ , and let $\Phi$ be a function on complex kernels on $\mathbb N$ . A trace-class kernel on $I$ means one with an expansion $X_{ij}=\sum_k u_k(i)\overline{v_k(j)}$ , $u_k,v_k\in\ell^2(I;\mathbb C)$ , and $\sum_k\|u_k\|\|v_k\|<\infty$ ; a density kernel additionally has real nonnegative finite quadratic forms, a summable real diagonal, and real diagonal sum one. Assume $\Phi$ preserves trace-class kernels, is additive and complex homogeneous on them, and preserves density kernels under every finite ampliation on its first factor, including the vacuous ancillary-dimension-zero test. Assume also $|\tau-1|\le y$ and, for every one-mode density kernel $S$ and every $z\in\mathbb C$ ,

\chi_{\Phi(S)}(z)=\chi_S(\sqrt\tau z)e^{-y|z|^2/2}, \quad \chi_X(z)=\sum_m\sum_nX_{mn}D_{nm}(z), \quad D_{mn}(z)=e^{-|z|^2/2}\sqrt{m!n!} \sum_{j=0}^{\min(m,n)} \frac{z^{m-j}(-\overline z)^{n-j}}{j!(m-j)!(n-j)!}.

For any kernel $X$ , let $N(X)$ be the infimum, in $[0,\infty]$ , of $\sum_k\|u_k\|\|v_k\|$ over its expansions just specified, with value $\infty$ if there are none. For each two-mode density kernel $R$ , set

Z_{(i,a),(j,b)} =\Phi\bigl((R_{(k,a),(\ell,b)})_{k,\ell}\bigr)_{ij}, \qquad Z^\Gamma_{(i,a),(j,b)}=Z_{(j,a),(i,b)}.

Then $e^{-2r}(1+\tau)\le y$ holds if and only if $N(Z^\Gamma)\le[e^{2r}]_+$ for every such $R$ ; equivalently, the three conditions $\tau\ge0$ , $|1-\tau|\le y$ , and $e^{-2r}(1+\tau)\le y$ hold if and only if that same universal bound holds. This quantification imposes no energy or Gaussian condition on $R$ . The statement also includes

e^{-2\cdot0}(1+\tau)\le y\quad\Longleftrightarrow\quad1+\tau\le y.

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