Probabilistically checkable proofs for the Existential Theory of the Reals

We prove a PCP theorem for the existential theory of the reals, showing that MAX-ETR-INV is $\exists\mathbb{R}$-hard to approximate to within some constant factor. The existential theory of the reals (ETR) is a decision problem asking if there exists a set of real-valued variables satisfying some constraints involving polynomials and inequalities, and $\exists\mathbb{R}$ is the complexity class of problems polynomial-time reducible to ETR. Many important geometric problems are known to be $\exists\mathbb{R}$-complete. $\exists\mathbb{R}$-hardness results frequently work by a reduction from the $\exists\mathbb{R}$-complete problem ETR-INV, which asks if there is a an assignment of real variables each in the interval $[\frac12, 2]$ satisfying some constraints of form $x=1$, $xy=1$ and $x+y=z$. MAX-ETR-INV is a related optimization problem that asks, given a set of constraints of form $x=1$, $xy=1$, and $x+y=z$, for a feasible (that is, satisfiable with variables in $[\frac12, 2]$) subset of those constraints of the largest possible size. We show that there is some constant $\epsilon>0$ such that it is $\exists\mathbb{R}$-hard to approximate MAX-ETR-INV better than a $1-\epsilon$ factor. This means that even a non-deterministic polynomial-time algorithm can't approximate MAX-ETR-INV better than this factor unless $\exists\mathbb{R}=\text{NP}$. We also give a polynomial-time $8$-factor approximation algorithm and a non-deterministic-polynomial-time $2$-factor approximation algorithm for MAX-ETR-INV.