III.C.1: basic splitting preserves Bob and reveals the bit on an Eve click, (15)

Open

QAlgorithms.Papers.Independent.Intakethird100.P33.basicSplitting

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

prove2quantum

Let $\mu\ge0$ and $t\in[0,1]$ . A nondecoy source bit $b\in\{0,1\}$ is the normalized coherent product $|\psi_b(\mu)\rangle$ , occupied in its early bin for $b=0$ and late bin for $b=1$ . Apply the vacuum beam splitter of intensity transmission $t$ separately to both bins, using its full normalized number-basis coefficients and positive output phases. The normalized output and Bob marginal are

|\Psi_b\rangle=|\psi_b(\mu t)\rangle_B\otimes|\psi_b(\mu(1-t))\rangle_E, \qquad \rho_B^b=|\psi_b(\mu t)\rangle\langle\psi_b(\mu t)|.

Thus Bob's state is the state of the untouched lossy channel. An ideal time-bin click on Eve's part reveals the bit without error. Its probability is $p_E=1-e^{-\mu(1-t)}$ , independently of $b$ . If $\mu(1-t)>0$ , let $K(p,y)$ be any finite-output trusted stochastic readout of Bob's two photon occupations $p$ : $K\ge0$ and $\sum_y K(p,y)=1$ . This kernel does not depend on Eve's outcome. With equal nondecoy bit priors, the normalized joint law of Bob's output $Y$ and Eve's inferred bit $E$ , conditional on her click, equals the original joint law of $Y$ and Alice's bit $A$ . In particular,

I(Y:E\mid D_E)=I(Y:A).

Equality of the joint laws also permits the same subsequent Bob acceptance conditioning and throughput weighting. At zero Eve-click probability, only the optical product and marginal statements apply. The exponential click probability is not replaced by its mean $\mu(1-t)$ .

This pins the exact content of the specified basic splitting attack and (15), without an optimality, privacy-amplification, or exact first-order Bob-rate assertion.

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.4-5, Fig.2 and (15): the full vacuum beam splitter produces a product
of attenuated coherent trains. Bob's marginal equals the untouched lossy channel.
On Eve's positive-probability click event the exact joint law equals Alice-Bob's
law, for arbitrary finite trusted number-readout/noise K. The probability used
here is exponential; the source's mu*(1-t) leakage claim is deferred separately.
Equality of joint laws also preserves subsequent Bob acceptance conditioning and
its common throughput weight; no first-order detection rate is asserted. -/
theorem basicSplitting (mu t : ℝ) (hmu : 0 ≤ mu) (ht : t ∈ Set.Icc 0 1) :
    (∀ bit : Bool,
      Memℓp (splitCoefficients t (dataState mu bit)) 2 ∧
      ‖dataState mu bit‖ = 1 ∧ ‖dataState (mu * t) bit‖ = 1 ∧
      ‖dataState (mu * (1 - t)) bit‖ = 1 ∧
      ‖splitState t (dataState mu bit)‖ = 1 ∧
      (∀ p q, splitState t (dataState mu bit) (p, q) =
        dataState (mu * t) bit p * dataState (mu * (1 - t)) bit q) ∧
      (∀ p q, Summable (fun e : ℕ × ℕ =>
        splitState t (dataState mu bit) (p, e) * star (splitState t (dataState mu bit) (q, e)))) ∧
      splitBobDensity t (dataState mu bit) = rankOne (dataState (mu * t) bit)) ∧
    (∀ bit : Bool, ∀ q, eveReadout q = some (!bit) →
      dataState (mu * (1 - t)) bit q = 0) ∧
    eveClickProbability mu t = 1 - Real.exp (-mu * (1 - t)) ∧
    (0 < mu * (1 - t) →
      0 < eveClickProbability mu t ∧
      ∀ (O : Type) [Fintype O] (K : (ℕ × ℕ) → O → ℝ),
        (∀ p o, 0 ≤ K p o) → (∀ p, ∑ o, K p o = 1) →
        clickJoint K mu t = aliceBobJoint K mu t ∧
        (∀ o b, 0 ≤ clickJoint K mu t o b) ∧
        (∑ o, ∑ b : Bool, clickJoint K mu t o b) = 1 ∧
        QAlgorithms.mutualInfoBits (Function.uncurry (clickJoint K mu t)) =
          QAlgorithms.mutualInfoBits (Function.uncurry (aliceBobJoint K mu t))) := 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.1, Fig.2 and (15)

Read-back

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

For all real $\mu,t$ with $\mu\ge0$ and $t\in[0,1]$ , write $c_z(r)=e^{-|z|^2/2}z^r/\sqrt{r!}$ , and let $\psi_{y,0}$ and $\psi_{y,1}$ denote the coherent pairs with amplitudes $(\sqrt y,0)$ and $(0,\sqrt y)$ , respectively: a coherent pair has the corresponding product coefficients when they are square summable, and is defined as zero otherwise. For nonnegative integers $r,s$ , put

b_t(r,s)=\sqrt{\frac{(r+s)!}{r!\,s!}}\,(\sqrt t)^r(\sqrt{1-t})^s.

For $v\in\ell^2(\mathbb N^2;\mathbb C)$ , define

s_{t,v}(p,e)=v_{p_1+e_1,p_2+e_2}\,b_t(p_1,e_1)b_t(p_2,e_2),

and let $S_t(v)\in\ell^2(\mathbb N^2\times\mathbb N^2;\mathbb C)$ be this coefficient family if it is square summable, and zero otherwise. For every Boolean $b$ , the family $s_{t,\psi_{\mu,b}}$ is square summable; each of $\psi_{\mu,b}$ , $\psi_{\mu t,b}$ , $\psi_{\mu(1-t),b}$ , and $S_t(\psi_{\mu,b})$ has norm one; and for every $p,e\in\mathbb N^2$ ,

S_t(\psi_{\mu,b})_{p,e} =\psi_{\mu t,b}(p)\psi_{\mu(1-t),b}(e).

For every $p,q\in\mathbb N^2$ , the family $e\mapsto S_t(\psi_{\mu,b})_{p,e}\overline{S_t(\psi_{\mu,b})_{q,e}}$ is summable, and its sum equals $\psi_{\mu t,b}(p)\overline{\psi_{\mu t,b}(q)}$ . Define $h(e)=\mathrm{some}(\mathrm{false})$ when $e_1>0,e_2=0$ , $h(e)=\mathrm{some}(\mathrm{true})$ when $e_1=0,e_2>0$ , and $h(e)=\mathrm{none}$ otherwise. For every Boolean $b$ and every $e$ , if $h(e)=\mathrm{some}(\neg b)$ , then $\psi_{\mu(1-t),b}(e)=0$ . The quantity

E=\sum_{e:\,h(e)=\mathrm{some}(\mathrm{false})} |\psi_{\mu(1-t),0}(e)|^2

equals $1-e^{-\mu(1-t)}$ . If $\mu(1-t)>0$ , then $E>0$ , and for every finite type $O$ and every real function $K:\mathbb N^2\times O\to\mathbb R$ satisfying $K(p,o)\ge0$ and $\sum_oK(p,o)=1$ for every $p$ , the functions

A(o,b)=\frac12\sum_p|\psi_{\mu t,b}(p)|^2K(p,o),\qquad J(o,e)=\frac{1}{2E}\sum_{b\in\{0,1\}} \sum_{\substack{p,q\in\mathbb N^2\\h(q)=\mathrm{some}(e)}} |S_t(\psi_{\mu,b})_{p,q}|^2K(p,o)

are equal, $J(o,b)\ge0$ for all $o,b$ , and $\sum_o\sum_bJ(o,b)=1$ . They also have equal values of the explicitly defined information quantity

\mathcal I(P)=\sum_o\sum_b P(o,b)\log_2\!\left( \frac{P(o,b)} {\left(\sum_{b'}P(o,b')\right)\left(\sum_{o'}P(o',b)\right)} \right), \qquad \mathcal I(J)=\mathcal I(A).

The finite type $O$ is not assumed nonempty, although its normalization condition on $K$ cannot hold when $O$ is empty. The unconditional assertions include $\mu=0$ and $t=1$ ; the conclusions about $J$ require the stated strict positivity condition, and its defining division is totalized to zero when $E=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