Resource-energy divergence and finite-energy attainment branches

Open

QAlgorithms.Papers.Independent.Intakethird100.P89.resourceEnergyBoundary

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

prove2quantum

Fix finite $r>0$ , put $L=\tanh r$ and $U=1/\tanh r$ , and let $b_{\min}(\tau)$ be the bound in (9). Define $a_{\min}(\tau)$ and $\overline n_{\min}(\tau)$ from the same family at $b=b_{\min}$ . All three functions are continuous on $(L,U)$ , and

a_{\min}(\tau),\ b_{\min}(\tau),\ \overline n_{\min}(\tau)\longrightarrow+\infty\quad\text{as }\tau\to L^+\text{ or }\tau\to U^-.

For the attainment classification, allow any finite $r\ge0$ . For every $\lambda>0$ , let $(\tau_{\rm opt},y_{\rm opt})$ be the optimizer of (13), and let $s=e^{2r}/(e^r+\lambda\cosh r)^2$ . If $s\le\tanh r$ , including equality, then $r>0$ and

\tau_{\rm opt}=\tanh r,\qquad y_{\rm opt}=1-\tanh r,

and this channel has no finite-energy centered Gaussian BK realization with logarithmic negativity exactly $2r$ . If $\tanh r<s$ , such a finite-energy realization exists.

The divergence is expressed through one-sided limits, without evaluating the rational family at a singular endpoint or introducing an infinite-energy density. The $r=0$ vacuum-replacer endpoint is not a divergence case.

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 pp.3--4, after (9) and (13): divergence is a one-sided LIMIT,
never a density or a rational expression evaluated at a zero denominator.
For r=0 the vacuum replacer endpoint is excluded from divergence. -/
theorem resourceEnergyBoundary (r : ℝ) (hr : 0 ≤ r) :
    (0 < r →
      let low := Real.tanh r
      let high := (Real.tanh r)⁻¹
      let interval := Set.Ioo low high
      ContinuousOn (familyMinA r) interval ∧
      ContinuousOn (familyMinB r) interval ∧
      ContinuousOn (familyMinEnergy r) interval ∧
      Tendsto (familyMinA r) (nhdsWithin low interval) atTop ∧
      Tendsto (familyMinB r) (nhdsWithin low interval) atTop ∧
      Tendsto (familyMinEnergy r) (nhdsWithin low interval) atTop ∧
      Tendsto (familyMinA r) (nhdsWithin high interval) atTop ∧
      Tendsto (familyMinB r) (nhdsWithin high interval) atTop ∧
      Tendsto (familyMinEnergy r) (nhdsWithin high interval) atTop) ∧
    (∀ lambda : ℝ, 0 < lambda →
      (stationaryTau lambda r ≤ Real.tanh r →
        0 < r ∧ optimalTau lambda r = Real.tanh r ∧
        optimalNoise lambda r = 1 - Real.tanh r ∧
        ¬ FiniteBKSimulates r (optimalTau lambda r) (optimalNoise lambda r)) ∧
      (Real.tanh r < stationaryTau lambda r →
        FiniteBKSimulates r (optimalTau lambda r) (optimalNoise lambda r))) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P89

end

Source

Optimal continuous variable quantum teleportation with limited resources, arXiv:1705.03017v5, PDF p. 3, Energy divergence at the quantum-limited boundary of Eq. (9)

Read-back

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

For every real $r\ge0$ , put

d_r(t)=t+1-e^{2r}|t-1|,\qquad B_r(t)=\frac{e^{2r}t+e^{-2r}-|t-1|}{d_r(t)},\qquad A_r(t)=\frac{B_r(t)+e^{-2r}(t-1)}{t},\qquad E_r(t)=\frac{A_r(t)+B_r(t)-2}{4}.

If $r>0$ , each of $A_r,B_r,E_r$ is continuous on $I_r=(\tanh r,(\tanh r)^{-1})$ , and each tends to $+\infty$ both as $t$ approaches $\tanh r$ within $I_r$ and as $t$ approaches $(\tanh r)^{-1}$ within $I_r$ . For every $\lambda>0$ , define

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

If $s\le\tanh r$ , then $r>0$ , $t_*=\tanh r$ , $y_*=1-\tanh r$ , and no finite realization specified below exists for $(r,t_*,y_*)$ ; if $\tanh r<s$ , such a realization does exist. Here a finite realization of $(r,t,y)$ means a density kernel $R$ on $\mathbb N^2$ , a real symmetric positive-definite $4\times4$ matrix $V$ , a gain $g>0$ , and a function $\Phi$ on one-mode kernels satisfying the following explicit conditions. A trace-class kernel $X$ on $L$ admits $X_{ij}=\sum_k u_k(i)\overline{v_k(j)}$ with $u_k,v_k\in\ell^2(L;\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; its trace size $N(X)$ is the extended-nonnegative infimum of those norm-product sums, with empty infimum $\infty$ . With

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),

require $V+i\operatorname{diag}(J,J)$ positive semidefinite for $J=\left(\begin{smallmatrix}0&1\\-1&0\end{smallmatrix}\right)$ , summability of every inner and outer series in $\chi_R^{(2)}(v)$ , and $\chi_R^{(2)}(v)=e^{-v^TVv/4}$ for every real $v$ . Require

\sum_{p\in\mathbb N^2}\left[\frac{p_0+p_1}{2}\operatorname{Re}R_{pp}\right]_+<\infty, \qquad N(R^\Gamma)=[e^{2r}]_+,\qquad R^\Gamma_{(a,b),(c,d)}=R_{(c,b),(a,d)},\qquad g^2=t\ge0.

The function $\Phi$ must preserve trace-class kernels, be additive and complex homogeneous on them, and preserve density kernels under every finite first-factor ampliation, with the dimension-zero test vacuous. Finally $|t-1|\le y$ , and for every one-mode density kernel $S$ and every $z$ ,

\chi_{\Phi(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 t\,z)e^{-y|z|^2/2}.

The divergence assertions are conditional on $r>0$ ; the assertions for $\lambda>0$ also apply when $r=0$ . All scalar divisions defining $A_r,B_r,E_r$ are total, taking value zero when their denominator is zero.

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