Exact binary no-signaling vertex classification

Open

QAlgorithms.Papers.Independent.Intakethird100.P22.binary_vertex_classification

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

prove2quantum

The vertices of the binary-input binary-output NS polytope are exactly the sixteen deterministic devices L_alpha,beta,gamma,sigma and eight PR-type devices B_r,s,t given in (321)-(322). The two displayed families have cardinalities 16 and 8; every deterministic member is local and every PR-type member is nonlocal.

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.56, cited classification [98]: exactly sixteen local deterministic
and eight nonlocal PR-type vertices. Both counts and both locality classes
are included, not merely membership of the supplied examples. -/
theorem binary_vertex_classification :
    (∀ p : Box Bool Bool Bool Bool, IsVertex p ↔
      (∃ alpha beta gamma sigma, p = deterministicBox alpha beta gamma sigma) ∨
      (∃ r s t, p = prVariant r s t)) ∧
    (Set.range (fun v : Bool × Bool × Bool × Bool =>
      deterministicBox v.1 v.2.1 v.2.2.1 v.2.2.2)).ncard = 16 ∧
    (Set.range (fun v : Bool × Bool × Bool => prVariant v.1 v.2.1 v.2.2)).ncard = 8 ∧
    (∀ alpha beta gamma sigma, HasLocalModel (deterministicBox alpha beta gamma sigma)) ∧
    (∀ r s t, ¬ HasLocalModel (prVariant r s t)) := 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. 56, Equations (321)-(322) and cited classification [98]

Read-back

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

For every real array $p(x,y,a,b)$ with all four arguments Boolean, $p$ is a valid extreme array if and only if it has one of the forms

p(x,y,a,b)=\mathbf1_{\{a=(\alpha\land x)\oplus\beta,\ b=(\gamma\land y)\oplus\sigma\}} \quad\text{for some }\alpha,\beta,\gamma,\sigma,

p(x,y,a,b)=\frac12\mathbf1_{\{a\oplus b=(x\land y)\oplus(r\land x)\oplus(s\land y)\oplus t\}} \quad\text{for some }r,s,t.

Validity means nonnegativity, $\sum_{a,b}p(x,y,a,b)=1$ for every $x,y$ , independence of $\sum_a p(x,y,a,b)$ from $x$ , and independence of $\sum_b p(x,y,a,b)$ from $y$ . Extremality means that whenever $p=\lambda q+(1-\lambda)r'$ for valid arrays $q,r'$ and $0<\lambda<1$ , both equal $p$ . The set of distinct arrays of the first form has cardinality $16$ , and the set of distinct arrays of the second form has cardinality $8$ . Every array of the first form has a local model, while no array of the second form does. Here having a local model means being a normalized nonnegative array and admitting some type $\Lambda$ , a probability mass function $\mu$ on $\Lambda$ , and nonnegative response functions $A_\ell(x,a)$ , $B_\ell(y,b)$ , each summing to $1$ over its output, such that

p(x,y,a,b)=\sum_{\ell\in\Lambda}\mu(\ell)\,A_\ell(x,a)\,B_\ell(y,b).

The sum is the infinite sum associated with the probability mass function; $\Lambda$ is not required to be finite.

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