Sufficient excess-noise bounds for positive signed model expressions

Proved

QAlgorithms.Papers.Independent.Intakenext100.P72.excessNoiseSufficiency

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

prove2quantum

Let $0<G\le1$ , $V\ge1$ , and $\epsilon\ge0$ , and set $\chi=(1-G)/G+\epsilon$ . Write $C=\tfrac12\log_2[1/((G\chi+G/V)(G\chi+G))]$ and $E=\tfrac14\log_2[1/(G\chi+G/V)^2]$ . Then

\epsilon<\frac{V-1}{2V}\Longrightarrow C>0,\qquad \epsilon<\frac{V-1}{V}\Longrightarrow E>0.

The thresholds tend to $1/2$ and $1$ , respectively, as $V\to\infty$ . These sufficient conditions hold for every positive lossy transmission, beyond the strong-loss regime surrounding the source paragraph. At $V=1$ neither strict premise can hold for nonnegative excess noise.

The result concerns explicit signed information-model expressions; the general security interpretation is retained in the deferred paper seed.

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.5, IV.B, excess-noise paragraph.
The displayed bounds are sufficient for positivity of the explicit signed
expressions for every lossy transmission. They are not definitions of security. -/
theorem excessNoiseSufficiency
    (G V excess : ℝ) (hG : 0 < G) (hGloss : G ≤ 1)
    (hV : 1 ≤ V) (hexcess : 0 ≤ excess) :
    (excess < coherentExcessThreshold V →
      0 < coherentExpression G ((1 - G) / G + excess) V) ∧
    (excess < eprExcessThreshold V →
      0 < eprExpression G ((1 - G) / G + excess) V) ∧
    Tendsto coherentExcessThreshold atTop (nhds (1 / 2 : ℝ)) ∧
    Tendsto eprExcessThreshold atTop (nhds (1 : ℝ)) := 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. 5, IV.B: excess-noise tolerance for coherent and EPR protocols

Read-back

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

For every $G,V,e\in\mathbb R$ satisfying $0<G\le1$ , $V\ge1$ , and $e\ge0$ , put $\chi_e=(1-G)/G+e$ . Then both implications hold:

\begin{aligned} e<\frac{V-1}{2V} &\quad\Longrightarrow\quad 0<\frac12\log_2\!\left( \frac1{(G\chi_e+G)(G\chi_e+G/V)} \right),\\ e<\frac{V-1}{V} &\quad\Longrightarrow\quad 0<\frac14\log_2\!\left( \frac1{(G\chi_e+G/V)^2} \right). \end{aligned}

The statement also asserts the limits

\lim_{W\to+\infty}\frac{W-1}{2W}=\frac12, \qquad \lim_{W\to+\infty}\frac{W-1}{W}=1,

where these quotient functions are defined on all real $W$ using total division, including value zero at $W=0$ . The case $V=1$ is allowed; in that case both strict-bound antecedents require $e<0$ , which is impossible under $e\ge0$ , so both implications hold vacuously.

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