A Sharp Local-Question Threshold for GHZ-Equatorial Completeness in Four-Player XOR Games

Chengkai Zhu; Ge Bai; Ranyiliu Chen; Xin Wang; Ziao Tang

A Sharp Local-Question Threshold for GHZ-Equatorial Completeness in Four-Player XOR Games

T0 review · 0 major / 3 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Four-player XOR games with at most three active questions per player have a perfect GHZ-equatorial strategy whenever their commuting-operator value is one; at four questions, the Klein four-group game separates the two properties.

desk verdict Sharp k=4 threshold for four-player XOR MERP completeness, with a solid proof apparatus and a Lean formalization that deserves a referee despite reproducibility nits. read the letter →

arxiv 2608.11139 v1 pith:F7VS24RT submitted 2026-08-11 quant-ph math-phmath.MP

Ziao Tang , Chengkai Zhu , Ge Bai , Xin Wang , Ranyiliu Chen This is my paper · ORCID

classification quant-phmath-phmath.MP MSC 81P4020F0505C70

keywords four-playerXORgamesGHZ-equatorialstrategiesMERPcommuting-operatorvalueprimitivecircuitsKleinfour-groupgameMagnusexpansionternaryHammingcube

verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

What is the smallest number of active questions per player at which a perfectly winnable four-player XOR game can stop being realizable on the four-qubit GHZ state with equatorial measurements? The paper's answer is three. Every four-player XOR game with at most three active questions per player and commuting-operator value one—perfect winnability in the commuting-operator model—admits a perfect GHZ-equatorial strategy, meaning perfect play reduces to consistency of additive phase equations. At four active questions per player, a single example, the Klein four-group game, has commuting-operator value one yet inconsistent phase equations, so no GHZ-equatorial strategy exists. Four is therefore the sharp local-question threshold, and the paper identifies the exact mechanism: abelian phase obstructions lift to ordered noncommutative refutations up to three questions, while the Klein translation pattern produces an abelian obstruction with no ordered noncommutative refutation of any length.

What carries the argument

The argument runs through two obstruction spaces attached to a reduced support $E$: the abelian space $L_E$ of parity images of integer incidence relations among the clause rows, and the noncommutative space $R_E$ generated by parity vectors of balanced words, ordered clause words in which every player's projected word freely reduces to the identity. A parity-permuted refutation, an element of $L_E$ with odd target parity, blocks a perfect GHZ-equatorial strategy; a true refutation, a balanced word with odd target parity, blocks commuting-operator value one. The positive half proves $L_E=R_E$ for every $E\subseteq[3]^4$ via an exact circuit-lifting theorem: every primitive support-minimal circuit, a minimal integer dependence with coprime coefficients, is realized by a balanced word with the same signed multiplicities, using signed-occurrence forest matchings to build the order and ternary Hamming geometry to eliminate the exceptional ten-clause supports. The negative half shows that in the Klein four-group game a parity-permuted refutation exists while no true refutation of any length does, using an even-subgroup free normal form and degree-one and degree-two Magnus coefficients to produce an integral parity certificate.

What would settle it

Because the positive half concerns only supports inside the finite set $[3]^4$, an exhaustive computation of the two obstruction spaces $L_E$ and $R_E$ over all reduced supports with at most three active questions per player would settle Theorem 1.1(i): any support with $L_E \neq R_E$ would be a counterexample. For the negative half, exhibiting any balanced word over the eight Klein clauses in which an odd number of $O_0$ clauses occur and each player's projected word freely reduces to the identity would refute the all-length obstruction and with it Theorem 1.1(ii).

Watch

Extended reading notes

Core claim

The central claim, stated as Theorem 1.1, is an exact equivalence at three questions and a separation at four. For every finite four-player XOR game in which each player has at most three active questions, the paper proves that commuting-operator value one holds if and only if the game has a perfect MERP strategy, a realization on the four-qubit GHZ state with equatorial single-qubit observables such that clause satisfaction becomes a set of additive angle equations. Conversely, the paper constructs the Klein four-group game, with four active questions per player and eight uniformly weighted clauses, whose commuting-operator value is one but whose phase equations are inconsistent. Because the three-question direction is affirmative and the four-question direction admits a counterexample, the paper concludes that four is the smallest number of active questions per player at which such a separation can occur.

Load-bearing premise

The load-bearing premise is the extremal counting claim that no ten-clause support on the full $3^4$ grid, with all four players using all three questions, can be a primitive minimal dependence when the clauses' neighborhoods cover all 81 question tuples; if one exceptional configuration were missed, the proof that every value-one three-question game has a GHZ-equatorial strategy would have a gap.

Editorial extensions

If this is right

For games with at most three active questions per player, perfect commuting-operator play and perfect GHZ-equatorial play are the same property: no exotic operator-algebraic construction is needed at value one.
The Klein four-group game is a separation example at four active questions: its phase system is inconsistent, so the GHZ-equatorial model cannot realize it, even though commuting-operator value one persists.
On every ternary four-partite support the abelian and noncommutative obstruction spaces coincide, so every parity-permuted refutation can be ordered into a genuine refutation; in particular any abelian obstruction at three questions pushes the commuting-operator value strictly below one.
The threshold statement is structural: it depends only on the reduced support and target vector, not on the positive clause weights or on whether the distribution over clauses is uniform.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

The paper leaves open whether the Klein game admits a perfect finite-dimensional tensor-product strategy; settling it either way would sharpen the meaning of the four-question threshold.
A plausible extension of the Magnus argument is that any group whose Cayley translation pattern forces a phase contradiction yields a value-one game without GHZ-equatorial strategies, not just elementary abelian 2-groups.
A natural extension would be a stability theorem: for at most three active questions and value $1-\varepsilon$, a GHZ-equatorial strategy of value at least $1-f(\varepsilon)$ with an explicit rate would carry the structural result into the noisy regime.
Because the support class $[3]^4$ is finite, the equality $L_E=R_E$ could be converted into a finite certificate family, making the three-question boundary in principle decidable by exhaustive support-level verification.

Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Desk Editor's Note

read the letter

Bottom line: this paper closes the four-player boundary case that was explicitly open after the two-question regime and the three-player collapse. It proves that three active questions per player are still safe—commuting-operator value one forces a perfect GHZ-equatorial strategy—and builds the Klein four-group game at four questions that separates the two. Four is sharp. That is genuinely new, and the main theorem is well supported.

The proof is the real work. The circuit-lifting argument on four ternary pages is intricate but coherent: primitive circuits localized to at most ten clauses, signed-occurrence forest matchings to order the occurrences, and ternary Hamming geometry to kill the exceptional configurations. I checked the two most fragile spots. Proposition A.7's exclusion of a ten-ball cover: the Gram matrix computation, the ternary Hamming-code coset counting, and the connectivity/edge-count contradiction all line up. And the degree-two Magnus certificate in Theorem 4.2: the weighted equation table cancels correctly and forces v even against v odd. I did not find a gap.

The soft spots are minor and mostly about verification hygiene. The Lean formalization is a real asset—no sorry/admit, and a statement-by-statement correspondence—but the repository has no commit hash, and several load-bearing statements (Theorem 3.1, Proposition A.7) are marked 'Supporting' rather than 'Direct' in Lean, while the all-length obstruction's general Magnus lemma is 'Alternative.' So the kernel-checked claim is slightly narrower than the manuscript suggests. That is a reproducibility caveat, not a demonstrated mathematical error. The authors are honest about it in the appendix.

Also worth noting: the discussion is candid about what the result does not settle—whether the Klein game has a finite-dimensional non-MERP perfect strategy, and quantitative robustness below the threshold. The citation pattern to WHKN19/WH23/WHK23 is appropriate, with no red flags. The use of an AI-assisted harness is disclosed; the math stands on its own.

Who is this for? Anyone working on MERP completeness, XOR games, or noncommutative obstruction spaces. The appendix is dense but the main text is readable. I would send it to a serious referee, not desk reject. My only request would be a pinned commit hash and a clearer mapping of which Lean statements are verbatim versus supporting.

Referee Report

0 major / 3 minor

Summary. The paper determines the exact threshold in the number of active questions per player at which perfect commuting-operator strategies for four-player XOR games can fail to admit a GHZ-equatorial (MERP) realization. Theorem 1.1 states that every four-player XOR game with at most three active questions per player and commuting-operator value one admits a perfect MERP strategy, while the Klein four-group game with four active questions per player has commuting-operator value one but no perfect MERP strategy. The positive direction is proved by reducing to the identity L_E = R_E for every support E subset [3]^4, obtained through an exact circuit-lifting theorem for primitive support-minimal circuits, with signed-occurrence forest matchings and ternary Hamming-geometry exclusions handling the ordering problem. The sharpness direction is proved through a Cayley-game analysis and a degree-two Magnus-expansion obstruction showing that the Klein game admits a PREF but no true refutation of any length. An appendix provides the extremal Hamming-cube exclusions and a Lean 4 formalization correspondence.

Significance. If correct, the paper resolves a natural boundary problem left open after the three-player collapse theorem of Bene Watts and Helton and the MERP-PREF duality of Bene Watts, Harrow, Kanwar, and Natarajan. The four-player, three-question completeness theorem and the four-question separation are both sharp, and the proof introduces transferable techniques: exact lifting of integral incidence circuits into ordered noncommutative refutations, and all-length obstructions via Magnus coefficients. I checked the two most delicate points—the ten-point Hamming exclusion in Proposition A.7 and the weighted Magnus sum in Theorem 4.2—and found the arguments internally consistent. The accompanying Lean development, with a statement-by-statement correspondence and no sorry or admit declarations, is a substantial verification asset, although the repository lacks a commit hash and some key statements are marked as supporting rather than direct.

minor comments (3)

[Appendix C] The GitHub repository [TZB+es] is cited without a commit hash, and Table 2 marks Proposition A.7 and Theorem 3.1 as 'Supporting' rather than 'Direct'; since these are the main combinatorial and lifting inputs, please pin the repository revision and clarify the exact formal status, or soften the claim that the principal threshold theorem is fully formalized.
[Section 5] In the final paragraph of Section 5, 'An robust game-algebra methods may provide a useful framework' should read 'Robust game-algebra methods may provide a useful framework'.
[Section 4.2] The weighted-sum table in Theorem 4.2 is central but presented without derivation; adding a short verification that the listed coefficients annihilate the P family and leave exactly 8R12, 8(Q13 - Q23 - Q31 + Q32), and 8(-S31 + S32) would make the proof substantially easier to audit.

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: Theorem 1.1 is proved from internal combinatorics plus external dualities; the Lean artifacts are outputs, not inputs.

full rationale

The derivation chain is self-contained relative to established external results. The positive half reduces to Corollary 3.2 (LE = RE), which is proved internally by Propositions 3.4 through 3.13 together with the Hamming-geometry exclusions of Appendix A; the only imported inputs are the MERP-PREF and strategy-refutation dualities of Proposition 2.2, cited to WHKN19, WH23, and WHK23, which are prior external works by other authors and are stated as background theorems rather than derived from the target claim. The Klein-game separation is proved internally: the PREF is exhibited in Eq. (2.10), and Theorem 4.2 gives an all-length Magnus obstruction with explicit Lemmas 4.3 and 4.4. The sharpness claim follows by combining these two internally proved directions. The Lean 4 development is an output artifact checked by an external kernel; Appendix C marks Theorem 3.1 and Proposition A.7 as 'Supporting' rather than 'Direct', which is a formalization-status caveat (as is the absence of a commit hash for the repository in [TZB+es]), not a circular dependence. No fitted parameter is renamed as a prediction and no load-bearing premise is justified solely by self-citation; the self-citations [ZTZ+26, TZB+es] concern the formal infrastructure, not the mathematical content of the threshold theorem.

Assumptions & free parameters 0 free parameters · 6 assumptions · 0 invented entities

The central claim rests on established XOR-game dualities, classical Magnus and free-group theory, and an explicit ternary Hamming code; none of these hide the target result. There are no fitted constants or ad hoc numerical choices, and no new physical entities are postulated. The reader must take the cited dualities of Proposition 2.2 as background, and the claimed Lean kernel-checks cannot be independently pinned because the manuscript does not reference a specific commit hash.

assumptions (6)

domain assumption MERP-PREF and strategy-refutation dualities (Proposition 2.2).
Imported from [WHKN19, Theorems 21-22] and [WH23, Theorem 2.1]/[WHK23, Sec. 3.5.1]. The chains omega_co=1 iff b in R_E^perp iff b in L_E^perp iff perfect MERP in Theorem 1.1(i) and the value-one conclusion for the Klein game rest on these as background theorems.
standard math Degree-one and degree-two Magnus coefficient identities for words equal to 1 in a free group (Lemma 4.4).
Classical Magnus expansion results [Mag37, MKS76]; used in Theorem 4.2 to derive integral parity constraints that contradict odd target parity for refutations of arbitrary length.
standard math Reidemeister-Schreier normal form: the even subgroup of the free product of Z2 groups is freely generated by t_q = x_q x_0 (Lemma 4.3).
Standard combinatorial group theory [MKS76]; the proof uses the homomorphism from the free product to Z2 whose kernel is the even subgroup, with Schreier transversal {1, x_0}.
standard math The ternary Hamming code C = {(a,b,a+b,a+2b)} is a perfect single-error-correcting code of minimum distance three (Proposition A.7).
The code is explicitly constructed and its coset structure is argued in Appendix A.7; the perfect-code property is used to conclude that every radius-one ball intersects each coset exactly once and that a 10-ball cover yields exactly nine double points.
domain assumption Commuting-operator strategies are modeled by bounded self-adjoint involutions on a single Hilbert space with operators of distinct players commuting (Section 2.1).
Standard model of commuting-operator strategies from [NPA08, CLS17]; underpins equation (2.1) and the definition of omega_co.
standard math Lean kernel standard axioms: propext, Classical.choice, Quot.sound, plus seven native_decide bridge axioms enumerated in Appendix C.
The formalization is claimed to rely on these logical and computational-reflection axioms only; the paper states that no sorry, admit, or manually declared axiom is present.

how reviews work

0 comments

Cite this review

Pith. "Pith review of A Sharp Local-Question Threshold for GHZ-Equatorial Completeness in Four-Player XOR Games." pith.science (2026). https://pith.science/paper/F7VS24RT

@misc{pith2026260811139,
  author       = {Pith},
  title        = {Pith review of: A Sharp Local-Question Threshold for GHZ-Equatorial Completeness in Four-Player XOR Games},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/F7VS24RT}},
  note         = {Machine review of arXiv:2608.11139}
}

read the original abstract

We determine the smallest number of active questions per player at which a four-player binary exclusive-or (XOR) game of commuting-operator value one need not admit a Greenberger--Horne--Zeilinger (GHZ) equatorial realization. Such a realization uses the four-qubit GHZ state and equatorial qubit observables, reducing perfect play to additive phase equations. We prove that every four-player XOR game with commuting-operator value one and at most three active questions per player has a perfect GHZ-equatorial strategy. Conversely, we construct a uniform eight-clause game with four active questions per player whose commuting-operator value is one but whose phase equations are inconsistent. Thus four is the sharp local-question threshold. The positive result follows by lifting every integral incidence obstruction to an ordered noncommutative refutation, using primitive circuits, forest matchings, and ternary Hamming geometry. For the separating game, a Klein four-group incidence relation obstructs the phase system, while an even-subgroup normal form and degree-one and degree-two Magnus coefficients exclude refutations of arbitrary length.

Figures

Figures reproduced from arXiv: 2608.11139 by the authors.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

24 extracted references · 20 canonical work pages

[3]

David , title =

Mermin, N. David , title =. Physical Review Letters , volume =. 1990 , doi =

work page 1990
[1]

, title =

Bell, John S. , title =. Physics Physique Fizika , volume =. 1964 , doi =

work page 1964
[2]

and Horne, Michael A

Clauser, John F. and Horne, Michael A. and Shimony, Abner and Holt, Richard A. , title =. Physical Review Letters , volume =. 1969 , doi =

1969
[4]

and Horne, Michael A

Greenberger, Daniel M. and Horne, Michael A. and Shimony, Abner and Zeilinger, Anton , title =. American Journal of Physics , volume =. 1990 , doi =

work page 1990
[5]

and Wolf, Michael M

Werner, Reinhard F. and Wolf, Michael M. , title =. Physical Review A , volume =. 2001 , doi =

work page 2001
[6]

Consequences and Limits of Nonlocal Strategies , booktitle =

Cleve, Richard and H. Consequences and Limits of Nonlocal Strategies , booktitle =. 2004 , doi =. quant-ph/0404076 , archivePrefix =

arXiv 2004
[7]

Unbounded Violation of Tripartite Bell Inequalities , journal =

P. Unbounded Violation of Tripartite Bell Inequalities , journal =. 2008 , doi =

work page 2008
[8]

Explicit Lower and Upper Bounds on the Entangled Value of Multiplayer

Bri. Explicit Lower and Upper Bounds on the Entangled Value of Multiplayer. Communications in Mathematical Physics , volume =. 2013 , doi =

work page 2013

Show all 24 references

[9]

A Convergent Hierarchy of Semidefinite Programs Characterizing the Set of Quantum Correlations , journal =

Navascu. A Convergent Hierarchy of Semidefinite Programs Characterizing the Set of Quantum Correlations , journal =. 2008 , doi =

2008
[10]

Journal of Mathematical Physics , volume =

Cleve, Richard and Liu, Li and Slofstra, William , title =. Journal of Mathematical Physics , volume =. 2017 , doi =

2017
[11]

Forum of Mathematics, Pi , volume =

Slofstra, William , title =. Forum of Mathematics, Pi , volume =. 2019 , doi =

2019
[12]

Communications of the ACM , volume =

Ji, Zhengfeng and Natarajan, Anand and Vidick, Thomas and Wright, John and Yuen, Henry , title =. Communications of the ACM , volume =. 2021 , doi =. 2001.04383 , archivePrefix =

2021 arXiv
[13]

and Kanwar, Gurtej and Natarajan, Anand , title =

Watts, Adam Bene and Harrow, Aram W. and Kanwar, Gurtej and Natarajan, Anand , title =. 10th Innovations in Theoretical Computer Science Conference , series =. 2019 , doi =. 1801.00821 , archivePrefix =

2019 arXiv
[14]

William , title =

Watts, Adam Bene and Helton, J. William , title =. Communications in Mathematical Physics , volume =. 2023 , doi =

2023
[15]

William and Klep, Igor , title =

Watts, Adam Bene and Helton, J. William and Klep, Igor , title =. Annales Henri Poincar. 2023 , doi =

2023
[16]

2024 , eprint =

Zhao, Yuming , title =. 2024 , eprint =

2024
[17]

Journal f

Magnus, Wilhelm , title =. Journal f. 1937 , doi =

1937
[18]

Magnus, Wilhelm and Karrass, Abraham and Solitar, Donald , title =
[19]

and Demaine, Erik D

Akitaya, Hugo A. and Demaine, Erik D. and Hesterberg, Adam and Liu, Quanquan C. , title =. Graph Drawing and Network Visualization , series =. 2018 , doi =

2018
[20]

Automated Deduction---

de Moura, Leonardo and Ullrich, Sebastian , title =. Automated Deduction---. 2021 , doi =

2021
[21]

Proceedings of the 9th

The. Proceedings of the 9th. 2020 , doi =

2020
[22]

2026 , eprint =

Zhu, Chengkai and Tang, Ziao and Zhen, Guocheng and Cao, Yimeng and Zhao, Yusheng and Chen, Ranyiliu and Zhao, Xuanqiang and Zhang, Lei and Wang, Xin , title =. 2026 , eprint =

2026
[23]

Tang, Ziao and Zhu, Chengkai and Bai, Ge and Wang, Xin and Chen, Ranyiliu , title =. 2026. URL: https://github.com/QuAIR/Four-Player-XOR-Games , howpublished =

2026
[24]

arXiv preprint arXiv:2606.19348 , year =

DeepSeek-V4: Towards Highly Efficient Million-Token Context Intelligence , author =. arXiv preprint arXiv:2606.19348 , year =

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.

[1] [3]

David , title =

Mermin, N. David , title =. Physical Review Letters , volume =. 1990 , doi =

work page 1990

[2] [1]

, title =

Bell, John S. , title =. Physics Physique Fizika , volume =. 1964 , doi =

work page 1964

[3] [2]

and Horne, Michael A

Clauser, John F. and Horne, Michael A. and Shimony, Abner and Holt, Richard A. , title =. Physical Review Letters , volume =. 1969 , doi =

1969

[4] [4]

and Horne, Michael A

Greenberger, Daniel M. and Horne, Michael A. and Shimony, Abner and Zeilinger, Anton , title =. American Journal of Physics , volume =. 1990 , doi =

work page 1990

[5] [5]

and Wolf, Michael M

Werner, Reinhard F. and Wolf, Michael M. , title =. Physical Review A , volume =. 2001 , doi =

work page 2001

[6] [6]

Consequences and Limits of Nonlocal Strategies , booktitle =

Cleve, Richard and H. Consequences and Limits of Nonlocal Strategies , booktitle =. 2004 , doi =. quant-ph/0404076 , archivePrefix =

arXiv 2004

[7] [7]

Unbounded Violation of Tripartite Bell Inequalities , journal =

P. Unbounded Violation of Tripartite Bell Inequalities , journal =. 2008 , doi =

work page 2008

[8] [8]

Explicit Lower and Upper Bounds on the Entangled Value of Multiplayer

Bri. Explicit Lower and Upper Bounds on the Entangled Value of Multiplayer. Communications in Mathematical Physics , volume =. 2013 , doi =

work page 2013