Exact single-resource reduction for rational bipartite systems

Open

QAlgorithms.Papers.Independent.Intakethird100.P78.rational_target_exact_permutation_reduction

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

prove2quantum

Let $P(a,b\mid x,y)$ be a normalized nonnegative bipartite no-signaling law on finite nonempty alphabets $X,Y,A,B$ , and assume every entry is rational. There exist a common denominator $d\ge2$ , permutations $f^{xy}$ of $[d]$ , and input-local relabelings $r_A^x:[d]\to A$ and $r_B^y:[d]\to B$ for which

P(a,b\mid x,y)=\frac1d\bigl|\{u\in[d]:r_A^x(u)=a,\ r_B^y(f^{xy}(u))=b\}\bigr| \quad\text{for all }x,y,a,b.

Thus a single permutation resource in $\mathcal D$ simulates $P$ exactly. Padding a common denominator to at least two includes deterministic targets.

The source sentence prints $\mathcal R$ ; the construction supplies $\mathcal D$ , which is the corrected class used here. Independent moderation of this source correction 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, exact rational case of Lemma 5: one D resource and input-local
relabelings reproduce a rational target exactly. Printed R is changed to D:
the constructed D(P) has arbitrary denominator-sized outputs, not binary
outputs. A denominator of one is padded to at least two. Independent
source-correction moderation is pending. -/
theorem rational_target_exact_permutation_reduction
    {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) (hrational : IsRational P.prob) :
    ∃ (d : ℕ) (F : X → Y → Equiv.Perm (Fin d))
      (alice : X → Fin d → A) (bob : Y → Fin d → B),
      1 < d ∧ HasCommonProbabilityDenominator P.prob d ∧
        relabeledKernel F alice bob = P.prob := by sorry

end QAlgorithms.Papers.Independent.Intakethird100.P78

end

Source

Bipartite Units of Non-Locality, arXiv:0808.0651v4, PDF p. 8, Unnumbered exact rational case in the proof of Lemma 5 (corrected class label)

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$ . Assume additionally that for every $x,y,a,b$ there exists $q\in\mathbb Q$ whose image in $\mathbb R$ equals $P(x,y,a,b)$ . Then there exist 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 for every $x,y,a,b$ there exists $k\in\mathbb N$ with $P(x,y,a,b)=k/d$ , and, at every entry,

P(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}

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