Theorem 3: equivalence of NSDI security criteria

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.security_criteria

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

prove2quantum

Let $P^{\rm pass}_{S_A S_B T E\mid Z}$ be a normalized classical-device law with a common finite nonempty key alphabet $\mathcal K$ and finite nonempty transcript, Eve-output and Eve-input alphabets. The $(S_A,S_B,T)$ marginal is independent of $Z$ . The ideal pass law replaces the keys by a uniform perfectly correlated pair, independent of the actual $(T,E\mid Z)$ marginal. The intermediate law copies Alice's key into Bob's register and preserves $(S_A,T,E\mid Z)$ . Let $r\in[0,1]$ be the abort probability, with an identical normalized abort branch in all three systems. Write $d_{\rm NS}$ for the operational NS distance, and $s,c,k$ for the pass-weighted secrecy, disagreement and security errors, respectively. Thus $s=(1-r)d_{\rm NS}(P_{S_A T E\mid Z}^{\rm pass},P_{S_A T E\mid Z}^{\rm ideal,pass})$ , $c=(1-r)\Pr[S_A\ne S_B\mid\mathrm{pass}]$ , and $k=(1-r)d_{\rm NS}(P^{\rm pass},P^{\rm ideal,pass})$ .

The following two implications hold for all nonnegative budgets:

s\le\varepsilon_{\rm sec},\ c\le\varepsilon_{\rm cor}\ \Longrightarrow\ k\le\varepsilon_{\rm sec}+\varepsilon_{\rm cor},

k\le\varepsilon\ \Longrightarrow\ c\le\varepsilon\ \text{and}\ s\le\varepsilon.

These parameter-independent constants express the security-criterion equivalence proved by the paper.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P22

Formal statement

noncomputable section

open scoped BigOperators

namespace QAlgorithms.Papers.Independent.Intakethird100.P22

attribute [local instance] Classical.propDecidable Classical.decEq

open QAlgorithms.Papers.Independent.Advance50.P47
  (Box IsCorrelation IsNoSignaling HasLocalModel correlationMixture prBox)

open QAlgorithms.Papers.Independent.Information100.P56 (IsLaw)

open QAlgorithms.Papers.Independent.Information100.P27 (shannon)

open QAlgorithms.Papers.Independent.Gap48.P25 (classicalMI)

/-- PDF pp.36–37, Theorem 3: the exact two implications (148),(149).
The printed arbitrary prescribed split-budget iff (147) is not asserted: it is
unjustified when one assigned budget is zero. Independent moderation is required. -/
theorem security_criteria {K T E Z : Type}
    [Fintype K] [Fintype T] [Fintype E] [Fintype Z]
    [Nonempty K] [Nonempty T] [Nonempty E] [Nonempty Z]
    (r : KeyOutput K T E Z) (z : Z) :
    (∀ es ec : ℝ, 0 ≤ es → 0 ≤ ec → cdSecrecyError r ≤ es → correctnessError r z ≤ ec →
      securityError r ≤ es + ec) ∧
    (∀ e : ℝ, 0 ≤ e → securityError r ≤ e →
      correctnessError r z ≤ e ∧ cdSecrecyError r ≤ e) := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P22

end

Source

Limitations on device independent key secure against non signaling adversary via the squashed non-locality, arXiv:1903.12154v7, PDF p. 36, Theorem 3 / equations (148), (149)

Read-back

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

For all finite nonempty types $K,T,E,Z$ , every $r$ consisting of $\alpha\in[0,1]$ and pass and abort arrays $P,Q$ , and every $z_0\in Z$ , assume each array is nonnegative, normalized over $a,b,t,e$ for every $z$ , and has its marginal after summing over $e$ independent of $z$ . Define

I_z(a,b,t,e)=\mathbf1_{\{a=b\}}\frac{\sum_{u,v}P_z(u,v,t,e)}{|K|}, \qquad P^A_z(a,t,e)=\sum_bP_z(a,b,t,e), \qquad I^A_z(a,t,e)=\sum_bI_z(a,b,t,e).

For arrays on $Z\times C\times E$ , define $d(R,S)$ as the supremum of

\frac12\sum_{j=0}^{m-1} \left|\sum_{c,z,e}u(c,z)(R_z(c,e)-S_z(c,e))v(c,z,e,j)\right|

over positive integers $m$ and nonnegative kernels satisfying $\sum_z u(c,z)=1$ and $\sum_jv(c,z,e,j)=1$ . Put

s=(1-\alpha)d(P^A,I^A),\qquad c=(1-\alpha)\sum_{\substack{a,b\\a\ne b}}\sum_{t,e}P_{z_0}(a,b,t,e),\qquad e=(1-\alpha)d(P,I),

using $C=K\times T$ for $s$ and $C=K\times K\times T$ for $e$ . The assertion is the conjunction of these two statements: for every pair of nonnegative real bounds $\varepsilon_s,\varepsilon_c$ , $s\le\varepsilon_s$ and $c\le\varepsilon_c$ imply $e\le\varepsilon_s+\varepsilon_c$ ; and for every nonnegative real $\varepsilon$ , $e\le\varepsilon$ implies both $c\le\varepsilon$ and $s\le\varepsilon$ .

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