Lemma 1: real versus intermediate distance equals correctness error

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.intermediate_distance

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 the real and intermediate full output systems,

d_{\rm NS}(P^{\rm real},P^{\rm int})=c=(1-r)\Pr[S_A\ne S_B\mid\mathrm{pass}].

The intermediate system isolates correctness error while keeping Alice and Eve's actual marginal.

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.31–32, Lemma 1, (94),(104): NS distance to the constructed intermediate
system equals the weighted disagreement probability. -/
theorem intermediate_distance {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) :
    cdDistance (withAbort r.abortProbability r.abort r.pass)
      (withAbort r.abortProbability r.abort (intermediateKey r.pass)) = correctnessError r z := 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. 31, Lemma 1 / equations (94), (104)

Read-back

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

For all 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 each $z$ , with their marginals obtained by summing over $e$ independent of $z$ . For every $z_0\in Z$ , define

J_z(a,b,t,e)= \begin{cases} \displaystyle\sum_{v\in K}P_z(a,v,t,e),&a=b,\\ 0,&a\ne b. \end{cases}

For arrays $R,S$ on $Z\times C\times E$ , let

d(R,S)= \sup_{\substack{m\ge1,\ u,v}} \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|,

where $u(c,\cdot)$ and $v(c,z,e,\cdot)$ are nonnegative real probability distributions on $Z$ and $\{0,\ldots,m-1\}$ . With $C=K\times K\times T$ , the assertion is

d\bigl(\alpha Q+(1-\alpha)P,\ \alpha Q+(1-\alpha)J\bigr) =(1-\alpha)\sum_{\substack{a,b\in K\\a\ne b}}\sum_{t,e}P_{z_0}(a,b,t,e).

The right side is the correctness error at the arbitrarily supplied $z_0$ ; the left side has no chosen input $z_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