Minimum nonnegative TMSS squeezing, with singular cases corrected

Open

QAlgorithms.Papers.Independent.Intakethird100.P89.minimumTMSSSqueezing

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

prove2quantum

Let $\tau>0$ , $|1-\tau|\le y\le1+\tau$ , and $(\tau,y)\ne(1,0)$ . Define $r_0$ independently as the infimum of nonnegative solutions $s$ to the actual TMSS noise equation

(1+\tau)\cosh(2s)-2\sqrt\tau\sinh(2s)=y.

This set has a least element, and

r_0=\begin{cases}\dfrac12\operatorname{arcosh}\!\left(\dfrac{y(1+\tau)-2\sqrt{\tau[y^2-(1-\tau)^2]}}{(1-\tau)^2}\right),&\tau\ne1,\\[4pt]\dfrac12\log(2/y),&\tau=1.\end{cases}

A normalized pure TMSS of parameter $r_0$ , with covariance blocks $A=B=\cosh(2r_0)I$ , $C=-\sinh(2r_0)\sigma_z$ , has logarithmic negativity $2r_0$ and finite per-mode photon number $\sinh^2 r_0$ . At gain $\sqrt\tau$ it simulates this channel on every input density. The identity has no finite nonnegative solution of the noise equation. On $y=e^{-2r}(1+\tau)$ , $r\ge0$ , one has $r_0\ge r$ , with equality exactly when $\tau=1$ or $r=0$ , and strict inequality for $r>0$ , $\tau\ne1$ .

The unit-transmissivity extension and equality exceptions correct the printed singular formula and blanket strict comparison; no assertion of two distinct nonnegative roots is made.

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, (10): minimum defined by the actual noise equation; finite
TMSS realization on every input. CORRECTIONS: tau=1 uses log(2/y)/2;
identity has no finite solution; the strict r0>r comparison has equality
at tau=1 or r=0. No assertion of two distinct nonnegative roots is made. -/
theorem minimumTMSSSqueezing (tau y : ℝ) (htau : 0 < tau)
    (hy : |1 - tau| ≤ y) (hyupper : y ≤ 1 + tau)
    (hidentity : tau ≠ 1 ∨ y ≠ 0) :
    IsLeast {s : ℝ | 0 ≤ s ∧ tmssNoise (Real.sqrt tau) s = y}
      (minimumSqueezing tau y) ∧
    minimumSqueezing tau y = squeezingClosedForm tau y ∧
    (∃ (rho : State (ℕ × ℕ)) (Phi : OscillatorChannel),
      rho.coefficients = tmssKernel (minimumSqueezing tau y) ∧
      CenteredResource rho (standardFormCovariance
        (Real.cosh (2 * minimumSqueezing tau y)) (Real.cosh (2 * minimumSqueezing tau y))
        (-Real.sinh (2 * minimumSqueezing tau y)) (Real.sinh (2 * minimumSqueezing tau y))) ∧
      twoModeMeanPhotonEnergy rho = ENNReal.ofReal (Real.sinh (minimumSqueezing tau y) ^ 2) ∧
      twoModeMeanPhotonEnergy rho < ⊤ ∧
      traceSize (partialTransposeFirst rho.coefficients) =
        ENNReal.ofReal (Real.exp (2 * minimumSqueezing tau y)) ∧
      IsBK rho (Real.sqrt tau) Phi ∧ PhaseInsensitive Phi tau y) ∧
    (¬ ∃ s : ℝ, 0 ≤ s ∧ tmssNoise 1 s = 0) ∧
    (∀ r : ℝ, 0 ≤ r → y = Real.exp (-2 * r) * (1 + tau) →
      r ≤ minimumSqueezing tau y ∧
      (minimumSqueezing tau y = r ↔ tau = 1 ∨ r = 0) ∧
      (0 < r → tau ≠ 1 → r < minimumSqueezing 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, Minimum TMSS squeezing for the non-entanglement-breaking range, Eq. (10)

Read-back

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

For real $\tau,y$ satisfying $\tau>0$ , $|1-\tau|\le y\le1+\tau$ , and $\tau\ne1$ or $y\ne0$ , define

T(g,s)=(1+g^2)\cosh(2s)-2g\sinh(2s),\qquad s_*=\inf\{s\in\mathbb R:s\ge0,\ T(\sqrt\tau,s)=y\}.

The number $s_*$ belongs to this set and is at most every other member, and

s_*= \begin{cases} \frac12\log(2/y),&\tau=1,\\[2pt] \frac12\log\!\left(x+\sqrt{x^2-1}\right),&\tau\ne1, \end{cases} \qquad x=\frac{y(1+\tau)-2\sqrt{\tau\bigl(y^2-(1-\tau)^2\bigr)}}{(1-\tau)^2}.

To specify the resource assertion, a trace-class kernel on $I$ means a kernel $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, with empty infimum $\infty$ , and write $[x]_+=\max(x,0)$ in $[0,\infty]$ . There exist a two-mode density kernel $R$ and a function $\Phi$ on one-mode kernels with

R_{ab}=t_{s_*}(a)\overline{t_{s_*}(b)},\qquad t_s(a)=\mathbf1_{a_0=a_1}\frac{(-\tanh s)^{a_0}}{\cosh s},

V= \begin{pmatrix} \cosh(2s_*)&0&-\sinh(2s_*)&0\\ 0&\cosh(2s_*)&0&\sinh(2s_*)\\ -\sinh(2s_*)&0&\cosh(2s_*)&0\\ 0&\sinh(2s_*)&0&\cosh(2s_*) \end{pmatrix}.

This $V$ is symmetric positive definite and $V+i\operatorname{diag}(J,J)$ is positive semidefinite, $J=\left(\begin{smallmatrix}0&1\\-1&0\end{smallmatrix}\right)$ . 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).

Every inner and outer series here is summable for every real $v$ , and $\chi_R^{(2)}(v)=e^{-v^TVv/4}$ . Moreover

E(R):=\sum_p\left[\frac{p_0+p_1}{2}\operatorname{Re}R_{pp}\right]_+ =[\sinh^2s_*]_+<\infty,\qquad N(R^\Gamma)=[e^{2s_*}]_+, \quad R^\Gamma_{(a,b),(c,d)}=R_{(c,b),(a,d)}.

The function $\Phi$ 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\in\mathbb C$ ,

\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^{-y|z|^2/2}.

The statement also asserts that no $s\ge0$ satisfies $T(1,s)=0$ . Finally, for every $r\ge0$ with $y=e^{-2r}(1+\tau)$ , one has $r\le s_*$ , with $s_*=r$ if and only if $\tau=1$ or $r=0$ ; if $r>0$ and $\tau\ne1$ , then $r<s_*$ . The excluded case is exactly $(\tau,y)=(1,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