Zero-entanglement optimum and heterodyne preparation

Open

QAlgorithms.Papers.Independent.Intakethird100.P89.zeroEntanglementHeterodyne

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

prove2quantum

For every finite $\lambda>0$ , zero shared entanglement gives the Gaussian optimum

g=\frac1{1+\lambda},\qquad \tau_{\rm opt}=g^2=\frac1{(1+\lambda)^2},\qquad y_{\rm opt}=1+\tau_{\rm opt},\qquad \overline F_{\rm opt}=\frac{1+\lambda}{2+\lambda}.

The minimum-energy resource family (9) has $a=b=1$ , $c=0$ : it is the actual two-mode vacuum with zero photon energy and partial-transpose trace norm one. The BK map is heterodyne detection on the input followed by preparation of $|g\beta\rangle$ for outcome $\beta$ . Explicitly, the channel is the coefficientwise integral of $|g\beta\rangle\langle g\beta|$ against $\langle\beta|\rho|\beta\rangle d^2\beta/\pi$ ; all such coefficient integrands are integrable. It is the phase-insensitive channel with the displayed parameters and actual average fidelity.

The transmissivity corrects the printed (14), which conflicts with $\tau=g^2$ in (7) and the gain in its own paragraph. The recovered Gaussian specialization is stated, while the older unrestricted classical benchmark [25] and implementation [7] retain their provenance.

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.4, (14), CORRECTED: printed tau=(1+lambda)^(-1) is replaced
by tau=(1+lambda)^(-2), because (7) and the same paragraph give g=(1+lambda)^(-1).
This is the Gaussian specialization and its heterodyne implementation, not a
new claim about the independently cited unrestricted classical benchmark. -/
theorem zeroEntanglementHeterodyne (lambda : ℝ) (hlambda : 0 < lambda) :
    let g := (1 + lambda)⁻¹
    let tau := ((1 + lambda)⁻¹) ^ 2
    optimalTau lambda 0 = tau ∧ optimalNoise lambda 0 = 1 + tau ∧
    scalarOptimum lambda 0 = (1 + lambda) / (2 + lambda) ∧
    familyMinA 0 tau = 1 ∧ familyMinB 0 tau = 1 ∧ familyMinC 0 tau = 0 ∧
    (∃ rho : State (ℕ × ℕ),
      rho.coefficients = tmssKernel 0 ∧
      CenteredResource rho (standardFormCovariance 1 1 0 0) ∧ twoModeMeanPhotonEnergy rho = 0 ∧
      traceSize (partialTransposeFirst rho.coefficients) = 1 ∧
      IsBK rho g (heterodynePrepare g)) ∧
    PhaseInsensitive (heterodynePrepare g) tau (1 + tau) ∧
    gaussianPriorFidelity lambda (heterodynePrepare g) = (1 + lambda) / (2 + lambda) ∧
    (∀ (rho : State ℕ) (m n : ℕ), Integrable (fun beta : ℂ =>
      (inner (𝕜 := ℂ) (coherentKet beta) ((operatorOfMatrix rho.coefficients) (coherentKet beta)) /
        (Real.pi : ℂ)) * coherentKernel ((g : ℂ) * beta) m n)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P89

end

Source

Optimal continuous variable quantum teleportation with limited resources, arXiv:1705.03017v5, PDF p. 4, Zero-entanglement specialization and optimal heterodyne gain, Eq. (14)

Read-back

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

For every real $\lambda>0$ , set $g=(1+\lambda)^{-1}$ and $\tau=g^2$ . Define

t_{\lambda,r}=\max\!\left(\tanh r,\frac{e^{2r}}{(e^r+\lambda\cosh r)^2}\right), \qquad y_{\lambda,r}=e^{-2r}(1+t_{\lambda,r}).

Then $t_{\lambda,0}=\tau$ , $y_{\lambda,0}=1+\tau$ , and the real supremum of

\left\{ \frac{2\lambda}{2(1-\sqrt t)^2+\lambda(1+y+t)}: t\ge0,\ |1-t|\le y,\ 1+t\le y \right\}

equals $(1+\lambda)/(2+\lambda)$ . With

d_r(t)=t+1-e^{2r}|t-1|,\quad B_r(t)=\frac{e^{2r}t+e^{-2r}-|t-1|}{d_r(t)},\quad A_r(t)=\frac{B_r(t)+e^{-2r}(t-1)}t,\quad C_r(t)=\frac{B_r(t)-e^{-2r}}{\sqrt t},

one has $A_0(\tau)=B_0(\tau)=1$ and $C_0(\tau)=0$ . To state the channel assertions, a trace-class kernel on $I$ admits $X_{ij}=\sum_k u_k(i)\overline{v_k(j)}$ with $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 and a summable real diagonal of sum one. Let $N(X)$ be the extended-nonnegative infimum of these norm-product sums. Put $c_\alpha(n)=e^{-|\alpha|^2/2}\alpha^n/\sqrt{n!}$ , $P_\alpha=c_\alpha c_\alpha^*$ , let $h_\alpha$ be a chosen square-summable realization of $c_\alpha$ or zero if absent, and let $O(X)$ be a chosen bounded operator with matrix $X$ or zero if absent. Define

\mathcal H_g(X)_{mn} =\int_{\mathbb C}\frac{\langle h_\beta,O(X)h_\beta\rangle}{\pi} c_{g\beta}(m)\overline{c_{g\beta}(n)}\,d\beta.

There exists a two-mode density kernel $R$ with $R_{ab}=\mathbf1_{a=(0,0)}\mathbf1_{b=(0,0)}$ , with

E(R):=\sum_{p\in\mathbb N^2} \left[\frac{p_0+p_1}{2}\operatorname{Re}R_{pp}\right]_+=0, \qquad N(R^\Gamma)=1, \quad R^\Gamma_{(a,b),(c,d)}=R_{(c,b),(a,d)}.

Here $[x]_+=\max(x,0)$ in $[0,\infty]$ . Define

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)!}, \quad \chi_X(z)=\sum_m\sum_nX_{mn}D_{nm}(z),

\chi_R^{(2)}(v)=\sum_a\sum_bR_{ab} \prod_{j=0}^1D_{b_ja_j}\!\left(\frac{-v_{j,1}+iv_{j,0}}{\sqrt2}\right).

Its defining inner and outer series are summable for every real $v$ , and $\chi_R^{(2)}(v)=e^{-|v|^2/4}$ ; the covariance $I_4$ is symmetric positive definite and $I_4+i\operatorname{diag}(J,J)$ is positive semidefinite for $J=\left(\begin{smallmatrix}0&1\\-1&0\end{smallmatrix}\right)$ . The function $\mathcal H_g$ preserves trace-class kernels, is additive and complex homogeneous on them, and preserves density kernels under every finite first-factor ampliation, including the vacuous dimension-zero test. For every one-mode density kernel $S$ and every $z$ ,

\chi_{\mathcal H_g(S)}(z)=\chi_S(gz)\, \chi_R^{(2)}(\sqrt2g\operatorname{Im}z,\sqrt2g\operatorname{Re}z, \sqrt2\operatorname{Im}z,-\sqrt2\operatorname{Re}z) =\chi_S(\sqrt\tau z)e^{-(1+\tau)|z|^2/2},

and $|\tau-1|\le1+\tau$ . Its defined prior fidelity is

\int_{\mathbb C}\frac{\lambda}{\pi}e^{-\lambda|\alpha|^2} \operatorname{Re}\langle h_\alpha,O(\mathcal H_g(P_\alpha))h_\alpha\rangle\,d\alpha =\frac{1+\lambda}{2+\lambda}.

Finally, for every density kernel $S$ and every $m,n\in\mathbb N$ , the integrand defining $\mathcal H_g(S)_{mn}$ is integrable.

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