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
- For and , the function is a probability distribution with correlators , , and vanishing one- and three-party means.
- 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 .
- Put . At and take ; at the other take ; at and , , the prescribed with ; at the prescribed with ; and elsewhere.
- 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.