MIP^co = coRE

In 2020, a landmark result by Ji, Natarajan, Vidick, Wright, and Yuen showed that MIP*, the class of languages that can be decided by a classical verifier interacting with multiple computationally unbounded provers sharing entanglement in the tensor product model, is equal to RE. We show that the class MIPco, a complexity class defined similarly to MIP*, except that the provers share entanglement in the commuting operator model, is equal to the class coRE. This shows that giving the provers two different models of entanglement leads to two completely different computational powers for interactive proof systems. Our main result, in addition to providing another disproof of the Connes embedding problem, Kirchberg's problem, and Tsirelson's problem, also yields several corollaries in continuous model theory and the theory of noncommutative polynomials that do not follow immediately from the MIP*=RE theorem. Along the way, we introduce several innovations to compatibility theory and the commuting operator model of entanglement which we list below:
We introduce a new equivalence condition for RE/coRE-complete problems, which we call the weakly compressible condition. In addition to non-local games, this new condition could also potentially be applicable to other classes of promise problems.
Additionally, we prove that any two-party correlation in the commuting operator model can be approximated using a \textit{tracially embeddable strategy}, a class of strategies defined on a finite tracial von Neumann algebra, which we define in this thesis. Using this characterization, we show that many known theorems in the tensor product model, such as the so-called "rounding" theorem by Vidick [JMP 2022], as well as the quantum soundness of the quantum tensor code test from Ji et al. [FOCS 2022] extend naturally to the commuting operator model.
We also give the first information-theoretic parallel repetition proof for non-local games in the commuting operator model of entanglement. This is done by combining the anchored parallel repetition proof by Bavarian et al. [SIAM J. Comput. 2022] along with the relative entropy framework given by Araki [PRIMS 1977]. We also define several analogues of information-theoretic tools for the tracial von Neumann algebra setting, such as mutual information and relative entropy, which may be of independent interest.
By using these innovations, we prove MIP^*=RE and MIPco=coRE simultaneously by showing that the compression theorem from the original MIP^*=RE proof satisfies the same completeness and soundness guarantees in the commuting operator model. This shows that both MIP* and MIPco satisfy this condition through the compression theorem, and thereby establish that the uncomputability of MIP* and MIPco can be proved under a unified framework (despite these two complexity classes being different). Notably, this approach also gives an alternative proof of the MIP*=RE theorem, which does not rely on the preservation of the entanglement bound. By using this compression theorem, we show that deciding whether a game has its tensor product value equal to its commuting operator value is equivalent to the halting problem. This shows that there are infinitely many examples of "Bell test" which distinguish between the tensor product model and the commuting operator model (although this also means that one cannot use a computer to perform a brute-force search for such a Bell test.). We also give a more streamlined proof of the compression theorem for non-local games by incorporating the synchronous framework used by Mousavi et al. [STOC 2022], as well as the improved Pauli basis test introduced by de la Salle [ArXiv:2204.07084].