Observation 1: abort factorization

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.abort_factorization

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

Let $P^{\rm real}=rP^{\rm abort}+(1-r)P^{\rm pass}$ and $P^{\rm ideal}=rP^{\rm abort}+(1-r)P^{\rm ideal,pass}$ . Then

d_{\rm NS}(P^{\rm real},P^{\rm ideal})=(1-r)d_{\rm NS}(P^{\rm pass},P^{\rm ideal,pass})=k.

A common abort branch contributes no distinguishing advantage.

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 p.31, Observation 1, (90): equal abort branches factor out exactly. -/
theorem abort_factorization {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) :
    cdDistance (withAbort r.abortProbability r.abort r.pass)
      (withAbort r.abortProbability r.abort (idealCDKey r.pass)) = securityError r := 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, Observation 1 / equation (90)

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$ have abort probability $\alpha\in[0,1]$ and pass and abort arrays $P,Q$ . Each array is nonnegative, sums to $1$ over $a,b,t,e$ for every $z$ , and has $\sum_eR_z(a,b,t,e)$ independent of $z$ . Put

I_z(a,b,t,e)=\mathbf1_{\{a=b\}}\frac{\sum_{u,v\in K}P_z(u,v,t,e)}{|K|}.

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

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 arbitrary nonnegative real probability distributions on $Z$ and $\{0,\ldots,m-1\}$ , respectively. With $C=K\times K\times T$ , the assertion is

d\bigl(\alpha Q+(1-\alpha)P,\ \alpha Q+(1-\alpha)I\bigr) =(1-\alpha)d(P,I),

whose right side is the defined security error of $r$ . Both endpoints $\alpha=0$ and $\alpha=1$ are included.

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