III.C.3: cross-pair counting preserves boundary coherence and destroys decoy coherence, (23)

Open

QAlgorithms.Papers.Independent.Intakethird100.P33.twoCoherentMonitoring

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

prove2quantum

Take $n\ge0$ source blocks with symbols 0, 1, or decoy, each occupied bin carrying coherent amplitude $\sqrt{x}$ for $x>0$ and each blocked bin vacuum. On every disjoint cross-boundary late/early pair $(2k,2k+1)$ , perform a nondemolition measurement of the total photon number and discard the measurement result. The resulting density retains a number-basis matrix element exactly when its bra and ket have the same total in every measured pair. The outer unpaired bins are untouched.

Both the original and counted full-Fock densities are normalized. For each occupied 1,0 boundary, the required number moments converge and the intrinsic monitor fluxes and contrast are

F_1=x,\quad F_2=0,\quad V_{10}=1.

For each decoy block strictly inside the train, its early and late bins belong to different measured pairs, and

F_1=F_2=x/2,\quad V_d=0.

The summed flux in each ratio is positive. Empty trains are allowed, with no tested pairs. The restriction to internal decoys avoids endpoint artifacts in the finite train.

This constructs the total-number attack rather than assuming its visibility response. It is separate from the conservative information assignment (22) and does not claim exact count preservation for an operational attack mixture.

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 pp.5-6, Fig.3 and (23): evaluated nonselective nondemolition counting on
successive disjoint shifted pairs. Cross-boundary 1,0 coherence survives, while
internal decoy coherence vanishes. The finite train's endpoints are excluded
only from the decoy test that needs two distinct measured pairs. No information
assignment from (22), count-preserving mixture, or detector probability is assumed. -/
theorem twoCoherentMonitoring (n : ℕ) (w : Fin n → Fin 3) (x : ℝ) (hx : 0 < x) :
    IsDensity (trainDensity w x) ∧ IsDensity (crossCounting w x) ∧
    (∀ k : Fin (n - 1), w (boundaryLeft k) = 1 → w (boundaryRight k) = 0 →
      let i := (boundaryLeft k, true)
      let j := (boundaryRight k, false)
      FinitePairMoments (crossCounting w x) i j ∧
      monitorFlux (crossCounting w x) i j 0 = x ∧
      monitorFlux (crossCounting w x) i j 1 = 0 ∧
      0 < monitorFlux (crossCounting w x) i j 0 + monitorFlux (crossCounting w x) i j 1 ∧
      opticalVisibility (crossCounting w x) i j = 1) ∧
    (∀ k : Fin n, 0 < k.val → k.val + 1 < n → w k = 2 →
      FinitePairMoments (crossCounting w x) (k, false) (k, true) ∧
      monitorFlux (crossCounting w x) (k, false) (k, true) 0 = x / 2 ∧
      monitorFlux (crossCounting w x) (k, false) (k, true) 1 = x / 2 ∧
      0 < monitorFlux (crossCounting w x) (k, false) (k, true) 0 +
        monitorFlux (crossCounting w x) (k, false) (k, true) 1 ∧
      opticalVisibility (crossCounting w x) (k, false) (k, true) = 0) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P33

end

Source

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

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$ , put $J=\{0,\ldots,n-1\}\times\{\mathrm{false},\mathrm{true}\}$ , and assign occupation indicators $(s_{(k,\mathrm{false})},s_{(k,\mathrm{true})})=(1,0),(0,1),(1,1)$ according as $w_k=0,1,2$ . Set $\alpha_a=0$ when $s_a=0$ and $\alpha_a=\sqrt{x}$ otherwise, and define

c(\alpha,m)=e^{-|\alpha|^2/2}\frac{\alpha^m}{\sqrt{m!}},\qquad T_{p,q}=\left(\prod_{a\in J}c(\alpha_a,p_a)\right) \overline{\left(\prod_{a\in J}c(\alpha_a,q_a)\right)}

for occupation functions $p,q:J\to\mathbb N$ . Define another matrix $\rho$ by $\rho_{p,q}=T_{p,q}$ if

p_{(r,\mathrm{true})}+p_{(r+1,\mathrm{false})} =q_{(r,\mathrm{true})}+q_{(r+1,\mathrm{false})} \quad\text{for every }0\le r<n-1,

and by $\rho_{p,q}=0$ otherwise. Both $T$ and $\rho$ have the following density properties: each matrix $X$ admits sequences $u_r,v_r\in\ell^2(J\to\mathbb N;\mathbb C)$ with $\sum_r\|u_r\|\|v_r\|<\infty$ and $X_{p,q}=\sum_r u_r(p)\overline{v_r(q)}$ ; every finite quadratic form $\sum_{p,q\in S}\overline{z_p}X_{p,q}z_q$ has zero imaginary part and nonnegative real part; and its real diagonal entries are summable with sum $1$ . To state the remaining conclusions, for distinct coordinates $i,j\in J$ 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}

and

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

Here the updated occupation function increases coordinate $i$ by one and decreases coordinate $j$ by one. For every adjacent pair $r,r+1$ with $0\le r<n-1$ , $w_r=1$ , and $w_{r+1}=0$ , take $i=(r,\mathrm{true})$ , $j=(r+1,\mathrm{false})$ ; then $N_i,N_j,C_{ij}$ are summable, $F_0(i,j)=x$ , $F_1(i,j)=0$ , their sum is positive, and their difference divided by their sum equals $1$ . For every $k$ satisfying $0<k$ , $k+1<n$ , and $w_k=2$ , take $i=(k,\mathrm{false})$ , $j=(k,\mathrm{true})$ ; then $N_i,N_j,C_{ij}$ are summable, $F_0(i,j)=F_1(i,j)=x/2$ , their sum is positive, and their difference divided by their sum equals $0$ . Natural subtraction in $n-1$ is truncated at zero: for $n=0$ or $n=1$ there are no adjacent-pair conditions and $\rho=T$ ; for $n\le2$ there are no interior-index conditions. Each conditional conclusion is vacuous when no index satisfies its word requirements, while both density conclusions hold for every $n$ , including $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