Proposition 2: operational NS norm for classical-device states

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.cdNorm_formula

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

prove2quantum

All alphabets are finite and nonempty. Both conditional laws are nonnegative and normalized for every input, and each classical marginal is independent of Eve's input.

For any two compatible classical-device states $P_{CE\mid Z}$ and $Q_{CE\mid Z}$ , the classical alphabet $C$ may be a tuple of arbitrarily many classical subsystems. The operational distance allows a random input $Z$ chosen after seeing $C$ and arbitrary stochastic processing of the resulting observation. Then

d_{\rm NS}(P,Q)=\frac12\sum_c\max_z\sum_e|P(c,e\mid z)-Q(c,e\mid z)|.

This formula characterizes the source's causal generating operations on classical-device states.

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.24, Proposition 2, (33); maximization is inside the classical sum. -/
theorem cdNorm_formula {C E Z : Type}
    [Fintype C] [Fintype E] [Fintype Z] [Nonempty C] [Nonempty E] [Nonempty Z]
    (p q : CDArray C E Z) (hp : IsCD p) (hq : IsCD q) :
    cdDistance p q = (1 / 2 : ℝ) * ∑ c, finiteMax (fun z => ∑ e, |p z c e - q z c 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. 24, Proposition 2 / equation (33)

Read-back

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

For finite, nonempty types $C,E,Z$ and arrays $p,q:Z\times C\times E\to\mathbb R$ , assume that both arrays are nonnegative, that each has total mass $1$ for every $z$ , and that each has a $C$ -marginal independent of $z$ : for $h=p$ and $h=q$ ,

\sum_{c,e}h(z,c,e)=1,\qquad \sum_e h(z,c,e)=\sum_e h(z',c,e) \quad\text{for all }z,z',c.

Then

d(p,q)=\frac12\sum_{c\in C}\max_{z\in Z} \sum_{e\in E}|p(z,c,e)-q(z,c,e)|.

Here $d(p,q)$ is the supremum of $\frac12\sum_{j=0}^{m-1}|g[p](j)-g[q](j)|$ over all positive natural numbers $m$ and all nonnegative kernels $u(c,z)$ , $v(c,z,e,j)$ with $\sum_z u(c,z)=1$ and $\sum_jv(c,z,e,j)=1$ , where $g[h](j)=\sum_{c,z,e}u(c,z)h(z,c,e)v(c,z,e,j)$ . Each maximum on the right is the supremum of the indicated finite, nonempty set of real values.

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