Comparison with any product of matching individually optimal attacks

Open

QAlgorithms.Papers.Independent.Intakethird100.P18.coherentAttack_le_product_of_individual_optima

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

prove2quantum

Fix $n\ge1$ independent signals in a local prepare-and-measure protocol as above: normalized states, protocol-prescribed independent local choices, separate normalized Bob POVMs, local sifting of positive probability, correct ideal retained decoding, and publicly announced settings without secret symbols. All channel errors are included in Bob's expected disturbance. Eve's attack $C$ has any normalized ancilla, a fixed input-independent joint unitary, and any delayed POVM chosen using only public announcements.

For each signal $i$ , suppose $O_0(i)$ is any physical single-signal attack that is optimal among all such attacks at the exact expected disturbance $D_i(C)$ . Let $O_n=\bigotimes_{i=1}^n O_0(i)$ , with both independent probes and factorized interactions and measurements. Then

I(C)\le I(O_n),

where $I=H(X\mid B)-H(X\mid B,Y)$ is the total classical Shannon information about the whole raw string after Eve's measurement, in bits, averaged over actual public configurations and outcomes.

This lemma compares every attack with every matching optimal family; it does not assert that such optimizers exist. The helper labels disclosed in the proof's Game G are not included in the original attack's public data. The statement concerns expected raw-key errors without test acceptance, error correction, privacy amplification, or a final-key security claim.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P18

Formal statement

noncomputable section

open MeasureTheory

open scoped BigOperators

namespace QAlgorithms.Papers.Independent.Intakethird100.P18

/-- PDF p.4, separately named Lemma, with proof context on pp.5–6:
every coherent attack is dominated by the product of any individually optimal
single-signal attacks at its matching local disturbances. Optimizer existence
is not assumed as an ambient axiom and is not asserted by this lemma.
The extra labels revealed in Game G are not public data in the original attack. -/
theorem coherentAttack_le_product_of_individual_optima
    (n : ℕ) (hn : 1 ≤ n) (P : Fin n → LocalProtocol)
    (C : Attack P) (A : ProductAttack P)
    (hA : ∀ i, OptimalAt (P i) (qkdDisturbance C i) (A i)) :
    qkdInformation C ≤ productInformation A := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P18

end

Source

On the role of coherent attacks in a type of strategic problem related to quantum key distribution, arXiv:quant-ph/0110089v6, PDF p. 4, Lemma (unnumbered), with context pp.5–6

Read-back

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

For every natural number $n\ge1$ , every family $P=(P_i)_{i<n}$ of local protocols, every joint attack $C$ on that family, and every tuple $A=(A_i)_{i<n}$ of single-site attacks satisfying the optimality condition below, the information of $C$ is at most the information of the product outcome laws of $A$ . Each local protocol consists of positive finite raw, preparation, Bob-choice, public, and signal index sets $X_i,S_i,B_i,C_i,Z_i$ ; nonnegative weights $r_i,p_i,q_i$ , each summing to $1$ on its respective set; unit vectors $\psi^i_{x,a}\in\mathbb C^{Z_i}$ ; positive semidefinite matrices $M^i_{b,x}$ with $\sum_xM^i_{b,x}=I$ ; retention and announcement functions $k_i(a,b)$ and $c_i(a,b)$ ; and positive retained mass $s_i=\sum_{a,b:k_i(a,b)=\mathrm{true}}p_i(a)q_i(b)$ . It requires $\operatorname{Re}\operatorname{tr}(M^i_{b,x}\psi^i_{x,a}(\psi^i_{x,a})^*)=1$ whenever $(a,b)$ is retained. Give $\ell_i=(x_i,a_i,b_i)$ weight $w_i(\ell_i)=r_i(x_i)p_i(a_i)q_i(b_i)/s_i$ when retained and $0$ otherwise, and put $W(\ell)=\prod_iw_i(\ell_i)$ , $x(\ell)=(x_i)_i$ , and $c(\ell)=(c_i(a_i,b_i))_i$ . An attack on any such family has a complete complex inner-product ancilla space $E$ , a unit vector $e$ , a complex-linear isometric equivalence $U$ of the Euclidean space of $E$ -valued functions on the joint signal set $Z=\prod_iZ_i$ , an arbitrary measurable outcome space $O$ , and a measurement for each public string $c$ . Each measurement gives continuous complex-linear operators $F_c(D)$ for measurable sets $D$ , with real nonnegative quadratic forms and $F_c(O)=I$ , and measures $\lambda_{c,v}$ satisfying $\lambda_{c,v}(D)=\max\{\operatorname{Re}\langle v,F_c(D)v\rangle,0\}$ . For an attack $B$ , set $\Phi^B_\ell=U(z\mapsto(\prod_i\psi^i_{x_i,a_i}(z_i))e)$ , $\mu^B_{\ell,c}=\sum_z\lambda_{c,\Phi^B_\ell(z)}$ , and

\Delta_i(B)=\sum_\ell W(\ell)\left[ 1-\operatorname{Re} \sum_{\substack{z,w\in Z\\z_j=w_j\ \text{for every }j\ne i}} M^i_{b_i,x_i}(z_i,w_i) \langle\Phi^B_\ell(z),\Phi^B_\ell(w)\rangle \right].

For any laws $\mu_{\ell,c}$ , put $\pi_{c,x}=\sum_{\ell:c(\ell)=c,\ x(\ell)=x}W(\ell)$ , $p_c=\sum_x\pi_{c,x}$ , $\nu_{c,x}=\sum_{\ell:c(\ell)=c,\ x(\ell)=x}W(\ell)\mu_{\ell,c}$ , and $\nu_c=\sum_x\nu_{c,x}$ ; let $h_{c,y}(x)$ be the real value of $(d\nu_{c,x}/d\nu_c)(y)$ , and let $H(t)=-\sum_xt(x)\log(t(x))/\log2$ . Define

J(\mu)=\sum_c\left[ p_cH\!\left(x\mapsto\frac{\pi_{c,x}}{p_c}\right) -\int H(h_{c,y})\,d\nu_c(y) \right].

The information of an attack $B$ is $I(B)=J(\mu^B)$ ; these definitions also apply to a single-site attack by using the one-element family containing its protocol, yielding a scalar disturbance $\Delta(B)$ . Zero public masses are included, division by zero and $\log0$ evaluate to $0$ , infinite Radon–Nikodym derivatives convert to $0$ , and a nonintegrable real integrand has integral $0$ . The hypothesis on $A$ is that, for every $i<n$ , $\Delta(A_i)=\Delta_i(C)$ and every single-site attack $B$ on $P_i$ with $\Delta(B)=\Delta_i(C)$ satisfies $I(B)\le I(A_i)$ . The conclusion is exactly

I(C)\le J(\mu^A), \qquad \mu^A_{\ell,c}=\bigotimes_{i<n}\mu^{A_i}_{\ell_i,c_i},

where the right-hand side is the defined product information.

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