Completeness conjecture for matrix and universal tracial satisfiability

Let $\mathcal{L}$ be the class of binary constraint system games, and let $\operatorname{SAT}_{matrix}(\mathcal{L})$ and $\operatorname{SAT}_{\mathcal{R}^{\mathcal{U}}}(\mathcal{L})$ denote the corresponding satisfiability problems for finite-dimensional matrix strategies and universal tracial strategies, respectively. The complexity classes $\mathrm{RE}$ and $\Pi^0_2$ are the recursively enumerable and second-level arithmetical hierarchy classes.

Completeness conjecture. In parts (a) and (b) of the cited dichotomy theorem, $\operatorname{SAT}_{matrix}(\mathcal{L})$ is $\mathrm{RE}$-complete, and $\operatorname{SAT}_{\mathcal{R}^{\mathcal{U}}}(\mathcal{L})$ is $\Pi^0_2$-complete.

The preceding results establish undecidability and the relevant lower bounds, while the MIP*=RE theorem and subsequent work establish the corresponding completeness results for arbitrary binary constraint systems. The conjecture asserts that these upper and lower bounds are also tight for the class $\mathcal{L}$ considered here.