III.C.2: intercept-resend destroys both checked coherences, (21)

Open

QAlgorithms.Papers.Independent.Intakethird100.P33.interceptResendMonitoring

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

prove2quantum

Take a finite train of source blocks with the occupied/vacuum patterns 10, 01, or 11, common phase, and occupied-pulse mean $x>0$ at Eve's ideal time-bin detector. In the specified intercept-resend construction, each occupied input is detected with probability $q=1-e^{-x}$ ; on detection a localized single photon is resent in that bin, otherwise vacuum is sent. A blocked bin remains vacuum. The resulting full-Fock density is the product of these diagonal localized-number mixtures.

For any two distinct occupied bins forming an illuminated tested pair, let $F_1,F_2$ denote the intrinsic mean output fluxes at their common interference slot of the balanced one-bin-delay monitor. Then the density is normalized, its required photon moments converge, and

F_1=F_2={q\over2},\qquad F_1+F_2>0,\qquad V={F_1-F_2\over F_1+F_2}=0.

This covers both within-decoy and 1,0-boundary tests, so both intrinsic visibilities in (21) vanish. It evaluates the localized resend construction; the distinct information-rate and exact count-preservation claims are deferred. Trusted dark counts are outside this intrinsic optical contrast.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P33

Formal statement

noncomputable section

namespace QAlgorithms.Papers.Independent.Intakethird100.P33

open scoped BigOperators ENNReal

open QAlgorithms.RealRegisters (Hilbert)

open QAlgorithms.Papers.Independent.Dependency50.P33 (IsDensity rankOne)

open QAlgorithms.Papers.Independent.Dependency50.P39 (coherentCoefficient)

open QAlgorithms.Papers.Independent.Support50.P48 (vacuumAmplitude)

open QAlgorithms.Papers.Independent.Next46.P32 (FockPOVM realFockTracePair)

open QAlgorithms.Papers.Independent.Dependency50.P34
  (TwoModeFock fockKet photonMean)

open QAlgorithms.Papers.Independent.Frontier18.P14
  (coherentPair coherentPairCoefficients)

attribute [local instance] Classical.propDecidable

attribute [local instance] Classical.decEq

/-- PDF p.5, Fig.3 and (21): construct the localized single-photon resend mixture
and evaluate its intrinsic monitor response on any illuminated tested pair.
Both within-decoy and cross-boundary pairs are covered. Trusted dark counts and
the unquantified first-order count-preservation assertion are separate. -/
theorem interceptResendMonitoring (n : ℕ) (w : Fin n → Fin 3) (x : ℝ) (hx : 0 < x) :
    IsDensity (interceptResend w x) ∧
    ∀ i j : Fin n × Bool, i ≠ j → sourceOccupation w i = 1 → sourceOccupation w j = 1 →
      FinitePairMoments (interceptResend w x) i j ∧
      monitorFlux (interceptResend w x) i j 0 = (1 - Real.exp (-x)) / 2 ∧
      monitorFlux (interceptResend w x) i j 1 = (1 - Real.exp (-x)) / 2 ∧
      0 < monitorFlux (interceptResend w x) i j 0 + monitorFlux (interceptResend w x) i j 1 ∧
      opticalVisibility (interceptResend w x) i j = 0 := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P33

end

Source

Towards practical and fast Quantum Cryptography, arXiv:quant-ph/0411022v1, PDF p. 5, III.C.2, Fig.3 and (21)

Read-back

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

For every natural number $n$ , every word $w:\{0,\ldots,n-1\}\to\{0,1,2\}$ , and every real $x>0$ , let $J=\{0,\ldots,n-1\}\times\{\mathrm{false},\mathrm{true}\}$ . Define an occupation indicator $s:J\to\{0,1\}$ by assigning $(s_{(k,\mathrm{false})},s_{(k,\mathrm{true})})=(1,0)$ when $w_k=0$ , $(0,1)$ when $w_k=1$ , and $(1,1)$ when $w_k=2$ . For a Boolean $b$ and a natural number $m$ , set $z=x$ if $b=\mathrm{true}$ and $z=0$ otherwise, and define $r_x(b,0)=e^{-z}$ , $r_x(b,1)=1-e^{-z}$ , and $r_x(b,m)=0$ for $m\ge2$ . Define the complex matrix $\rho$ , indexed by occupation functions $p,q:J\to\mathbb N$ , by

\rho_{p,q}= \begin{cases} \displaystyle\prod_{a\in J}r_x(s_a=1,p_a),&p=q,\\ 0,&p\ne q. \end{cases}

Then $\rho$ has the following density properties: there exist sequences $u_r,v_r\in\ell^2(J\to\mathbb N;\mathbb C)$ with $\sum_r\|u_r\|\|v_r\|<\infty$ and $\rho_{p,q}=\sum_{r=0}^{\infty}u_r(p)\overline{v_r(q)}$ ; every finite quadratic form $\sum_{p,q\in S}\overline{z_p}\rho_{p,q}z_q$ , for a finite set $S$ and any complex function $z$ on the occupation functions, has zero imaginary part and nonnegative real part; and the real diagonal entries are summable with sum $1$ . Moreover, for every pair of distinct $i,j\in J$ with $s_i=s_j=1$ , define

N_a(p)=p_a\operatorname{Re}\rho_{p,p},\qquad C_{ij}(p)= \begin{cases} 0,&p_j=0,\\ \sqrt{(p_i+1)p_j}\,\rho_{p,\,p+\mathbf e_i-\mathbf e_j},&p_j>0, \end{cases}

where the updated occupation function increases coordinate $i$ by one and decreases coordinate $j$ by one. The functions $N_i,N_j,C_{ij}$ are summable. With

F_0=\frac{\sum_pN_i(p)+\sum_pN_j(p)+2\operatorname{Re}\sum_pC_{ij}(p)}4,\qquad F_1=\frac{\sum_pN_i(p)+\sum_pN_j(p)-2\operatorname{Re}\sum_pC_{ij}(p)}4,

the conclusions are $F_0=F_1=(1-e^{-x})/2$ , $F_0+F_1>0$ , and $(F_0-F_1)/(F_0+F_1)=0$ . The statement includes $n=0$ , when the products are empty products equal to $1$ and there are no pairs $i,j$ ; more generally, the pair conclusions impose no conditions when no distinct occupied pair exists.

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