Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Metadata
slug: klobus-2016-chained-monogamy-realizability
bibkey: klobus2016communication
doi: 10.1007/s10701-015-9983-5
url: https://arxiv.org/abs/1408.1223v2
triage: theorem
motivation_gids:
  - D5/S3/QuantumBounds/ChainedMonogamySignalingRealizability.result

Realizability of the correlators of boxes violating chained monogamy

Problem

W. Kłobus, M. Oszmaniec, R. Augusiak, A. Grudka, Communication strength of correlations violating monogamy relations, Found. Phys. 46 (2016) 620–634, arXiv:1408.1223v2, Section 5:

Although we cannot prove it as in the case , we conjecture that all possible values of the correlators in and that satisfy inequalities (\ref{ElPrat}) can always be realized with some signaling probability distribution for which .

A box is a family of distributions on , , with one setting for the third party, all one- and three-party expectation values zero, and a common value of . with the chained Bell expression $I^M_{AB}=\sum_k(\langle A_kB_k\rangle+\langle A_{k+1}B_k\rangle)A_M=-A_0\Delta\in[0,2]$. The coordinates are , , , (), , , and (ElPrat) is for all .

Motivation

The paper derives the monogamy relation $|I^M_{AB}|+2|\langle B_0E\rangle|\le2M$ of nonsignaling boxes from three-variable inequalities and reads a violation by as forced signaling: the correlators in at least one pair , must differ, and each pair defines a binary classical channel. The communication strength of the violation is the least over violating boxes of the largest capacity of these channels. The conjecture identifies the set over which this minimization runs: the correlator vectors cut out by (ElPrat). The frozen declaration D5/S3/QuantumBounds/ChainedMonogamySignalingRealizability.result proves it.

Gap

Issue #12401 classifies the conjecture as Tier 1 and records the checks made before any Lean:

  • arXiv:1408.1223 v2 is the latest version and states the conjecture; Crossref, OpenAlex and INSPIRE report no citing work;
  • results on monogamy of nonsignaling correlations (Toner, quant-ph/0601172; Augusiak–Demianowicz–Pawłowski–Tura–Acín, arXiv:1307.6390; Ramanathan–Horodecki, arXiv:1402.4453; Augusiak, arXiv:1611.00651) and on communication cost (Montina–Wolf, arXiv:1312.6290) fix aggregate Bell values of nonsignaling boxes, not every coordinate of a signaling box; a later account by W. Kłobus (2023 summary of professional accomplishments, §4.3.3) gives a lower bound on the communication strength and no proof of the conjecture.

These are seat-reported and orchestrator-reported readings, not-found-in-searched-scope; they do not establish exhaustive worldwide novelty. The realizable correlator triples of three variables with zero odd moments form a tetrahedron; this is the case of Huber–Marić, arXiv:1311.2002v2, Theorem 3, and of the cut polytope of (arXiv:1706.06182v2, §4), and is used in step 1 of the Route.

Route

  1. For and , the function is a probability distribution with correlators , , and vanishing one- and three-party means.
  2. Let $T=\sum_{i=1}^{M-1}|x_A^i-y_B^i|+\sum_{i=1}^{M-2}|x_B^{i+1}-y_A^i| +|y_A^{M-1}+y_B^0|$. Choosing every sign in (ElPrat) against its term gives .
  3. Put . At and take ; at the other take ; at and , , the prescribed with ; at the prescribed with ; and elsewhere.
  4. The box realizes the coordinates, for all , and .

Falsifier

The kernel-checked result states, for every , every and all coordinate sequences with values in on their index ranges that satisfy (ElPrat), that some box (indexed by natural numbers, a probability distribution on Bool × Bool × Bool at every setting pair with ) has vanishing one- and three-party means, a common , , and the prescribed coordinates. It reads at the setting pair : relabels the outcome of , which does not change a correlator of and . The case is the conjecture; for (ElPrat) differs from the paper’s printed list (see Triage).

Evidence

Exact Fraction arithmetic (issue #12401): the box of Route step 3 realizes 1440 random admissible coordinate vectors with entries in for and , checking nonnegativity, normalization, the common , all correlators and ; a box with one entry changed by is rejected by the same verifier. A second construction puts and every at its extreme, which gives the largest for the given coordinates, ; it realizes 1000 further admissible samples by mixing with the box for , and on 15827 non-admissible samples its value of is below , as the converse direction predicts. (The box of Route step 3 is defined by the formula for only on admissible data: outside them can exceed and a probability becomes negative.)

The canonical source is D5/S3/QuantumBounds/ChainedMonogamySignalingRealizability.lean. Its public declarations are IsBox, OddMomentsVanish, corrAB, corrAE, corrBE, chainR, ElPrat, CoordinateBounds, Realizes, claim and result; the outcome sign is the frozen D5/S3/Combinatorics/IsingUniquenessSets.sgn. The frozen module state has statement identity sha256:457daf112b0653b47d2b60cd8593fed7c8f4c0b80f3970f0369a70f48cea1665. The result declaration has statement identity sha256:189745a8f3608dc5f2cf3c74b97968e0de7b0d9ee8126daa88b6ff6a30963cba. The Freeze event is sha256:29c7ef363071c78eeee2044226eeba96ec3dc9f0cc8cc7cb0aeffd286a53bf75; its project-level frozen prerequisite is the Freeze event of D5/S3/Combinatorics/IsingUniquenessSets. The proof uses only the standard axioms propext, Classical.choice and Quot.sound; no sorry, native_decide, or new axiom.

Triage

Tier 1 published conjecture; resolution Proved by D5/S3/QuantumBounds/ChainedMonogamySignalingRealizability.result. proof_shape: content; admission_basis: open-problem-resolution (issue #12401). Utility kind none (a statement for every , every and every admissible coordinate vector).

What the settlement shows

  • Proved by result: every coordinate vector in satisfying (ElPrat) is realized by a box of the paper’s class with a common and , for all and .
  • Proved inside the proof of result: (ElPrat) implies the single inequality ; the realizing box can be taken with .
  • Mechanism (read off the proof; not stated in Lean): the setting pairs decouple. Each pair only has to realize a point of the correlator tetrahedron, and the only link between pairs is the common . For fixed coordinates the largest is , attained with , so (ElPrat) is exactly the condition that this maximum reaches ; since , also .
  • Follows from it (not stated in Lean): with the paper’s derivation of (ElPrat) as a necessary condition (l. 704–716), the set of coordinate vectors of is exactly the (ElPrat) polytope inside , so the communication strength is a minimization over this explicit polytope. At the realizing box need not signal; for every realizing box signals.
  • Checked by reading (orchestrator, issue #12401): the paper’s printed list (l. 468–471, labels niert1–niert4) has the signs of reversed in niert2 and niert3; the point satisfies all four printed inequalities at but has , so it is not realizable. (ElPrat) at is the corrected list.
  • Open here: the value of for (the minimization of the largest channel capacity over the polytope); whether the paper’s reported values of for were computed with the printed or with the correct inequalities (not checked); and the analogous realizability question when the common-value assumption on is dropped, as the paper does for at the end of Section 4.

ASSUMED-UNVERIFIED

The literature checks do not establish worldwide priority; the 2023 summary by W. Kłobus and the Huber–Marić results are seat-reported readings. The Lean kernel verifies the encoded statement and its axiom closure; its correspondence to the paper, including the reading of the class , of and of the setting , is checked by reading the source and the definitions.