The coRE-hardness conjecture for distinguishing commuting quantum game values

Let $\mathcal{G}$ be a game, and let $\omega_{\mathrm{qc}}(\mathcal{G})$ denote its commuting quantum value. Consider the promise problem in which

$$\omega_{\mathrm{qc}}(\mathcal{G})=1\qquad\text{or}\qquad\omega_{\mathrm{qc}}(\mathcal{G})\leq \frac{1}{4}.$$

CoRE-hardness conjecture. Deciding which of these two cases holds is $\mathrm{coRE}$-hard; equivalently, $\mathrm{MIP}^{\mathrm{co}}=\mathrm{coRE}$.

This conjecture supplies the hardness premise needed to construct games whose finite-level NPA scores substantially exceed their true commuting quantum values. Its status is not resolved in the supplied source.