Lemma 3: security implies both secrecy and correctness

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.security_secrecy_correctness

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})$ .

For every $\varepsilon\ge0$ ,

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

Security controls both individual errors with constant one.

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.33–36, Lemma 3, (116),(146): both conclusions have constant one. -/
theorem security_secrecy_correctness {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) (e : ℝ) (he : 0 ≤ e)
    (h : 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. 33, Lemma 3 / equation (116)

Read-back

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

For finite nonempty types $K,T,E,Z$ , let $r$ consist of $\alpha\in[0,1]$ and pass and abort arrays $P,Q$ , both nonnegative and normalized over $a,b,t,e$ for every $z$ , with their marginals after summing over $e$ independent of $z$ . Set

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$ , let $d(R,S)$ be 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 with $\sum_z u(c,z)=1$ and $\sum_jv(c,z,e,j)=1$ . For every $z_0\in Z$ and real $\varepsilon\ge0$ , the hypothesis $(1-\alpha)d(P,I)\le\varepsilon$ implies both

(1-\alpha)\sum_{\substack{a,b\\a\ne b}}\sum_{t,e}P_{z_0}(a,b,t,e)\le\varepsilon \quad\text{and}\quad (1-\alpha)d(P^A,I^A)\le\varepsilon.

The distance uses $C=K\times K\times T$ in the hypothesis and $C=K\times T$ in the second conclusion.

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