II.B: optimal unambiguous time-bin readout and absence of coding errors

Open

QAlgorithms.Papers.Independent.Intakethird100.P33.dataDiscrimination

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

prove2quantum

Consider two orthogonal temporal modes, a perfect blocking switch, and a common zero optical phase. Let $\mu\ge0$ be the mean photon number in an occupied source pulse and let the channel transmission $t$ , data-port transmission $t_B$ , and trusted detector efficiency $\eta$ lie in $[0,1]$ . After loss, put $x=\mu t t_B\eta$ and define the normalized full-Fock states $|0_x\rangle=|\sqrt{x},0\rangle$ and $|1_x\rangle=|0,\sqrt{x}\rangle$ . The two nondecoy bits have equal conditional prior probabilities. Their overlap and optimal unambiguous discrimination probability are

|\langle0_x|1_x\rangle|=e^{-x},\qquad p_{\rm success}=1-e^{-x}.

Every three-outcome unambiguous POVM has average success probability at most this value. Photon counting attains it: a nonzero occupation exclusively in the early or late bin reports bit 0 or 1, respectively, while vacuum is inconclusive. Each state has inconclusive probability $e^{-x}$ , and a wrong conclusive bit has probability zero. Optimality with $\eta<1$ concerns POVMs on the attenuated states. At $x=0$ the common state is vacuum and the optimal success is zero.

This gives the exact error-free data readout in the absence of dark counts; it does not assert a security rate.

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.2, II.B and (4)-(5): exact optimal unambiguous readout on states AFTER
trusted efficiency loss, with equal bit priors and no dark counts. Includes an
attaining number-counting POVM, the universal bound, and absence of coding errors. -/
theorem dataDiscrimination (mu t tB eta : ℝ) (hmu : 0 ≤ mu)
    (ht : t ∈ Set.Icc 0 1) (htB : tB ∈ Set.Icc 0 1)
    (heta : eta ∈ Set.Icc 0 1) :
    let x := mu * t * tB * eta
    (∀ bit : Bool, ‖dataState x bit‖ = 1 ∧
      ∀ nm, dataState x bit nm =
        coherentPairCoefficients (if bit then 0 else (Real.sqrt x : ℂ))
          (if bit then (Real.sqrt x : ℂ) else 0) nm) ∧
    ‖inner ℂ (dataState x false) (dataState x true)‖ = Real.exp (-x) ∧
    (∃ M : OpticalPOVM (Fin 3),
      (∀ o nm pq, M.effect o nm pq =
        if nm = pq ∧ countingOutcome nm = o then 1 else 0) ∧
      Unambiguous M x ∧ discriminationSuccess M x = 1 - Real.exp (-x) ∧
      realFockTracePair (rankOne (dataState x false)) (M.effect 2) = Real.exp (-x) ∧
      realFockTracePair (rankOne (dataState x true)) (M.effect 2) = Real.exp (-x)) ∧
    (∀ M : OpticalPOVM (Fin 3), Unambiguous M x →
      discriminationSuccess M x ≤ 1 - Real.exp (-x)) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P33

end

Source

Towards practical and fast Quantum Cryptography, arXiv:quant-ph/0411022v1, PDF p. 2, II.B, (4)–(5)

Read-back

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

For all real $\mu,t,t_B,\eta$ with $\mu\ge0$ and $t,t_B,\eta\in[0,1]$ , put $x=\mu t t_B\eta$ . Work in $\ell^2(\mathbb N^2;\mathbb C)$ , and write $c_a(r)=e^{-|a|^2/2}a^r/\sqrt{r!}$ . A coherent pair with amplitudes $a,b$ is the vector with coefficients $c_a(m)c_b(n)$ when this coefficient family is square summable, and is defined as zero otherwise. Let $\psi_0$ be the coherent pair with amplitudes $(\sqrt{x},0)$ , and $\psi_1$ the coherent pair with amplitudes $(0,\sqrt{x})$ . Both vectors have norm one, their coefficients are the stated products for every $(m,n)\in\mathbb N^2$ , and

|\langle\psi_0,\psi_1\rangle|=e^{-x}.

For a vector $v$ , put $R(v)_{a,b}=v_a\overline{v_b}$ , and for matrices $X,E$ put $\tau(X,E)=\operatorname{Re}\sum_a\sum_b X_{a,b}E_{b,a}$ , with both sums interpreted as totalized infinite sums. There exists a three-outcome measurement $M=(M_0,M_1,M_2)$ : each effect has real, nonnegative quadratic form on every finitely supported complex test vector, and their entrywise sum is the identity matrix. Its entries satisfy

(M_o)_{a,b}= \begin{cases} 1,&a=b\ \text{and }h(a)=o,\\ 0,&\text{otherwise}, \end{cases} \quad h(m,n)= \begin{cases} 0,&m>0,\ n=0,\\ 1,&m=0,\ n>0,\\ 2,&\text{otherwise}. \end{cases}

This measurement obeys $\tau(R(\psi_0),M_1)=\tau(R(\psi_1),M_0)=0$ , has average success $\bigl(\tau(R(\psi_0),M_0)+\tau(R(\psi_1),M_1)\bigr)/2=1-e^{-x}$ , and satisfies $\tau(R(\psi_0),M_2)=\tau(R(\psi_1),M_2)=e^{-x}$ . Moreover, every three-outcome measurement satisfying the same positivity and completeness conditions and the two zero-error equations has average success at most $1-e^{-x}$ . The hypotheses include $x=0$ , when the two vectors coincide and this success bound is zero.

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