A Sharp Local-Question Threshold for GHZ-Equatorial Completeness in Four-Player XOR Games
Ziao Tang, Chengkai Zhu, Ge Bai, Xin Wang, Ranyiliu Chen
quant-ph
Aug 11, 2026 · v1
math-ph
TL;DR
The main threshold theorem and its obstruction-space corollary are formalized in Lean 4 using Mathlib and the Lean-QIT library, with an accompanying repository.
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.
Problem
The question is the smallest number of active questions per player at which a four-player XOR game with commuting-operator value one can fail to have a perfect GHZ-equatorial strategy. Such a strategy uses the four-qubit GHZ state with equatorial measurements.
Approach
For at most three questions per player, every integral incidence obstruction is lifted to an ordered noncommutative refutation, using primitive circuits, forest matchings, and ternary Hamming geometry. For four questions, a Klein four-group Cayley game is constructed. Refutations of every length are ruled out with an even-subgroup normal form and degree-one and degree-two Magnus coefficients. The principal theorem is formalized in Lean 4 with Mathlib and Lean-QIT, and its proof terms are checked by the Lean kernel.
Results
Every such game with at most three active questions per player and commuting-operator value one has a perfect GHZ-equatorial strategy. A uniform eight-clause game with four questions per player has commuting-operator value one but inconsistent phase equations, so four is the sharp threshold. The main theorem is kernel-checked in Lean, though some intermediate lemmas are not reproduced verbatim.
