Finite-energy minimum-entanglement resource family

Open

QAlgorithms.Papers.Independent.Intakethird100.P89.finiteEnergyOptimalResources

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

prove2quantum

Let $r\ge0$ , $\tau>0$ and $D=\tau+1-e^{2r}|\tau-1|>0$ . For $r>0$ this denominator condition is equivalent to $\tanh r<\tau<1/\tanh r$ . Define

b_{\min}=\frac{e^{2r}\tau+e^{-2r}-|\tau-1|}{D},\qquad a=\frac{b+e^{-2r}(\tau-1)}{\tau},\qquad c=\frac{b-e^{-2r}}{\sqrt\tau}.

For every $b\ge b_{\min}$ , the symmetric covariance with blocks $A=aI$ , $B=bI$ , $C=-c\sigma_z$ is physical and is the doubled covariance of a normalized centered Gaussian density $\rho$ on the complete two-oscillator space. It satisfies

\|\rho^\Gamma\|_1=e^{2r},\qquad \overline n_{AB}=\frac{a+b-2}{4}<\infty.

The deterministic BK protocol at gain $\sqrt\tau$ exactly simulates, on every input density, the phase-insensitive channel with noise $e^{-2r}(1+\tau)$ . Among this displayed family the per-mode mean photon number is minimized at $b=b_{\min}$ . Any finite-energy Gaussian BK realization of that channel with logarithmic negativity $2s$ , $s\ge0$ , has $s\ge r$ .

Physicality, state existence and exact simulation are conclusions of the result. The energy minimum is within family (9), with no claim of global energy optimality over all Gaussian resources.

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, (9): existence, physicality, exact all-input simulation and
minimum entanglement are CONCLUSIONS for the constructed finite-energy family.
The b=b_min energy minimum is only within the displayed family. -/
theorem finiteEnergyOptimalResources (r tau : ℝ) (hr : 0 ≤ r) (htau : 0 < tau)
    (hden : 0 < familyDenominator r tau) :
    (0 < r → (0 < familyDenominator r tau ↔
      Real.tanh r < tau ∧ tau < (Real.tanh r)⁻¹)) ∧
    (∀ b : ℝ, familyMinB r tau ≤ b →
      let a := familyA r tau b
      let c := familyC r tau b
      let V := standardFormCovariance a b (-c) c
      PhysicalCovariance V ∧
      ∃ (rho : State (ℕ × ℕ)) (Phi : OscillatorChannel),
        CenteredResource rho V ∧ twoModeMeanPhotonEnergy rho < ⊤ ∧
        twoModeMeanPhotonEnergy rho = ENNReal.ofReal ((a + b - 2) / 4) ∧
        traceSize (partialTransposeFirst rho.coefficients) = ENNReal.ofReal (Real.exp (2 * r)) ∧
        IsBK rho (Real.sqrt tau) Phi ∧
        PhaseInsensitive Phi tau (Real.exp (-2 * r) * (1 + tau))) ∧
    (∀ b : ℝ, familyMinB r tau ≤ b →
      familyMinEnergy r tau ≤ familyEnergy r tau b) ∧
    FiniteBKSimulates r tau (Real.exp (-2 * r) * (1 + tau)) ∧
    (∀ s : ℝ, 0 ≤ s → FiniteBKSimulates s tau (Real.exp (-2 * r) * (1 + tau)) → r ≤ s) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P89

end

Source

Optimal continuous variable quantum teleportation with limited resources, arXiv:1705.03017v5, PDF p. 3, Finite-energy minimum-entanglement Gaussian resource family, Eq. (9)

Read-back

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

For real $r,\tau$ satisfying $r\ge0$ , $\tau>0$ , and

d_r(\tau)=\tau+1-e^{2r}|\tau-1|>0,

define

b_{\min}=\frac{e^{2r}\tau+e^{-2r}-|\tau-1|}{d_r(\tau)},\qquad a(b)=\frac{b+e^{-2r}(\tau-1)}{\tau},\qquad c(b)=\frac{b-e^{-2r}}{\sqrt\tau},\qquad e(b)=\frac{a(b)+b-2}{4}.

If $r>0$ , then $d_r(\tau)>0$ is equivalent to $\tanh r<\tau<(\tanh r)^{-1}$ . For every real $b\ge b_{\min}$ , set

V_b= \begin{pmatrix} a(b)&0&-c(b)&0\\ 0&a(b)&0&c(b)\\ -c(b)&0&b&0\\ 0&c(b)&0&b \end{pmatrix}.

This matrix is positive definite and $V_b+i\operatorname{diag}(J,J)$ is positive semidefinite, where $J=\left(\begin{smallmatrix}0&1\\-1&0\end{smallmatrix}\right)$ . The statement uses the following kernel notions: a trace-class kernel $X$ on $I$ has an expansion $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; and $N(X)$ is the infimum of these norm-product sums in $[0,\infty]$ , with empty infimum $\infty$ . Write

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), \quad E(R)=\sum_{p\in\mathbb N^2} \left[\frac{p_0+p_1}{2}\operatorname{Re}R_{pp}\right]_+, \quad R^\Gamma_{(a,b),(c,d)}=R_{(c,b),(a,d)}.

Here $[x]_+=\max(x,0)$ is viewed in $[0,\infty]$ . For every $b\ge b_{\min}$ there exist a density kernel $R$ on $\mathbb N^2$ and a function $\Phi$ on one-mode kernels such that all the inner and outer sums defining $\chi_R^{(2)}(v)$ are summable for every $v$ , $\chi_R^{(2)}(v)=e^{-v^TV_bv/4}$ , $E(R)<\infty$ , $E(R)=[e(b)]_+$ , and $N(R^\Gamma)=[e^{2r}]_+$ . The function $\Phi$ preserves trace-class kernels, is additive and complex homogeneous on them, and preserves density kernels under every finite first-factor ampliation; the dimension-zero test is vacuous. For every one-mode density kernel $S$ and every $z\in\mathbb C$ , it satisfies

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

and $|\tau-1|\le e^{-2r}(1+\tau)$ . Also $e(b_{\min})\le e(b)$ for every $b\ge b_{\min}$ . In particular, a realization with these finite-energy, centered covariance, channel, and gain conditions exists at noise $e^{-2r}(1+\tau)$ . Finally, for every $s\ge0$ , if such a realization exists at the same $\tau$ and noise, with $N(R^\Gamma)=[e^{2s}]_+$ instead of $[e^{2r}]_+$ and with any centered physical covariance, then $r\le s$ . The assertions include $r=0$ ; only the interval equivalence is conditional on $r>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