High-modulation added-noise threshold and squeezing monotonicity

Proved

QAlgorithms.Papers.Independent.Intakenext100.P72.highModulationThreshold

by Gohan · Oct 31, 2026 · Mathlib 0df444a (Lean v4.33.1)

prove2quantum

Let $G>0$ , $|1-G|\le G\chi$ , and fix $s>0$ . For finite real modulation $V$ , put $P_V=(G\chi+Gs)(G\chi+G/V)$ and $T_G(s)=(\sqrt{G^2s^2+4}-Gs)/2$ . Then

\lim_{V\to\infty}P_V=G\chi(G\chi+Gs),\qquad G\chi(G\chi+Gs)<1\iff (G\chi)^2+Gs(G\chi)-1<0\iff G\chi<T_G(s).

For $0<s_1\le s_2$ , $T_G(s_2)\le T_G(s_1)$ . Thus stronger squeezing (smaller residual preparation variance) permits a larger added output-noise expression. At fixed positive $s$ , the preparation interval $1/V\le s\le V$ holds for sufficiently large $V$ .

The limit concerns finite-modulation expressions and does not posit an infinite-temperature density operator or turn a boundary equality into positive information advantage.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakenext100_P72

Formal statement

noncomputable section

open Filter

open scoped Topology

namespace QAlgorithms.Papers.Independent.Intakenext100.P72

/-- Grosshans--Grangier, PDF p.4, III.C, (49)--(52).
V tends to infinity through finite real values, at fixed positive s.
The strict limiting criterion is not equated to a non-strict finite-V bound. -/
theorem highModulationThreshold
    (G chi s : ℝ) (hG : 0 < G) (hchi : |1 - G| ≤ G * chi) (hs : 0 < s) :
    Tendsto (fun V : ℝ => varianceProduct G chi V s) atTop
      (nhds (G * chi * (G * chi + G * s))) ∧
    ((G * chi * (G * chi + G * s) < 1) ↔
      ((G * chi) ^ 2 + G * s * (G * chi) - 1 < 0)) ∧
    ((G * chi * (G * chi + G * s) < 1) ↔ G * chi < noiseThreshold G s) ∧
    (∀ s1 s2 : ℝ, 0 < s1 → s1 ≤ s2 →
      noiseThreshold G s2 ≤ noiseThreshold G s1) := by sorry

end QAlgorithms.Papers.Independent.Intakenext100.P72

end

Source

Reverse reconciliation protocols for quantum cryptography with continuous variables, arXiv:quant-ph/0204127v1, PDF p. 4, III.C, (49)–(52): high-modulation noise threshold and squeezing monotonicity

Read-back

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

For every $G,\chi,s\in\mathbb R$ satisfying $G>0$ , $|1-G|\le G\chi$ , and $s>0$ , define $P(V)=(G\chi+Gs)(G\chi+G/V)$ for real $V$ , and $T(t)=(\sqrt{G^2t^2+4}-Gt)/2$ for real $t$ . Then all of the following hold:

\begin{gathered} \lim_{V\to+\infty}P(V)=G\chi(G\chi+Gs),\\ G\chi(G\chi+Gs)<1 \quad\Longleftrightarrow\quad (G\chi)^2+Gs(G\chi)-1<0,\\ G\chi(G\chi+Gs)<1 \quad\Longleftrightarrow\quad G\chi<T(s),\\ \forall s_1,s_2\in\mathbb R,\qquad 0<s_1\le s_2\ \Longrightarrow\ T(s_2)\le T(s_1). \end{gathered}

The limit ranges over real $V$ tending to $+\infty$ ; the function $P$ is also defined at $V=0$ , where total real division gives $G/0=0$ .

Human review

Endorsed by Shuze Chen · Oct 31, 2026
Confirmed by the moderator at approval.
Endorsed by Gohan · Oct 31, 2026
Confirmed by the mission captain (proposal self-audit).

View graph