One permutation resource approximates any finite bipartite no-signaling law

Open

QAlgorithms.Papers.Independent.Intakethird100.P78.permutation_box_approximates_bipartite

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

prove2quantum

Let $P(a,b\mid x,y)$ be a bipartite no-signaling conditional probability law on finite nonempty input alphabets $X,Y$ and output alphabets $A,B$ . For every $\varepsilon>0$ , there exist a rational normalized no-signaling law $Q$ , a common denominator $d\ge2$ for its probabilities, permutations $f^{xy}$ of $[d]$ , and local relabelings $r_A^x:[d]\to A$ and $r_B^y:[d]\to B$ , such that

Q(a,b\mid x,y)=\frac1d\bigl|\{u\in[d]:r_A^x(u)=a,\ r_B^y(f^{xy}(u))=b\}\bigr|, \qquad \delta(Q,P)<\varepsilon.

Here $\delta$ is worst-input total variation, and a common denominator means that every entry of $Q$ is a nonnegative integer divided by $d$ . The relabelings access only the corresponding local input and local resource output.

The formula gives a single-resource simulation followed by local relabelings. The proof paragraph's printed class label $\mathcal R$ is corrected to $\mathcal D$ , in agreement with the lemma and its construction; independent moderation is pending.

Preamble

import Definitions.Def_QAlgorithms_Papers_Independent_Intakethird100_P78

Formal statement

noncomputable section

open scoped BigOperators

namespace QAlgorithms.Papers.Independent.Intakethird100.P78

attribute [local instance] Classical.propDecidable Classical.decEq

/-- PDF p.8, Lemma 5 and its one-resource construction: for any positive
accuracy choose a rational normalized no-signaling approximant, then a
single permutation box and local relabelings that reproduce it exactly.
The common denominator is padded to at least two. The proof paragraph's
printed R is the class-label typo corrected to D here. Independent
source-correction moderation is pending. -/
theorem permutation_box_approximates_bipartite
    {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B]
    [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B]
    (P : BipartiteSystem X Y A B) (epsilon : ℝ) (hepsilon : 0 < epsilon) :
    ∃ (Q : BipartiteSystem X Y A B) (d : ℕ)
      (F : X → Y → Equiv.Perm (Fin d))
      (alice : X → Fin d → A) (bob : Y → Fin d → B),
      1 < d ∧ IsRational Q.prob ∧ HasCommonProbabilityDenominator Q.prob d ∧
        relabeledKernel F alice bob = Q.prob ∧
        simulationDistance Q.prob P.prob < epsilon := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P78

end

Source

Bipartite Units of Non-Locality, arXiv:0808.0651v4, PDF p. 8, Lemma 5: a permutation box approximates any bipartite no-signaling system

Read-back

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

Let $X,Y,A,B$ be finite, nonempty types, and let $P(x,y,a,b)$ be a real-valued array with nonnegative entries such that $\sum_{a\in A}\sum_{b\in B}P(x,y,a,b)=1$ for every $x,y$ , $\sum_bP(x,y,a,b)=\sum_bP(x,y',a,b)$ for every $x,y,y',a$ , and $\sum_aP(x,y,a,b)=\sum_aP(x',y,a,b)$ for every $x,x',y,b$ . For every real $\varepsilon>0$ , there exist another array $Q$ satisfying these same nonnegativity, normalization, and two marginal-independence conditions, a natural number $d>1$ , a permutation $F_{x,y}$ of $I_d=\{0,\ldots,d-1\}$ for every $x,y$ , and maps $\alpha_x:I_d\to A$ and $\beta_y:I_d\to B$ , such that every entry of $Q$ equals a rational number and, for each $x,y,a,b$ , there exists $k\in\mathbb N$ with $Q(x,y,a,b)=k/d$ . These choices also satisfy, for every $x,y,a,b$ ,

Q(x,y,a,b)= \sum_{u\in I_d} \begin{cases} \dfrac1d,&\alpha_x(u)=a\ \text{and}\ \beta_y(F_{x,y}(u))=b,\\ 0,&\text{otherwise}, \end{cases}

and

\sup_{(x,y)\in X\times Y} \frac12\sum_{a\in A}\sum_{b\in B} |Q(x,y,a,b)-P(x,y,a,b)|<\varepsilon.

The nonempty output types $A$ and $B$ are allowed to be singletons.

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