All known examples for double exponential lower bounds for real quantifier elimination involves polynomial inequalities with degree $>1$.


Is there an example of double exponentiality with polyhedral inequalities where polyhedral inequalities refers degree is at most $1$?


**Conjecture**: There is none and if you have $t$ quantifications with $n$ variables per quantification and $m$ constraints the complexity is $O(poly(n^{O(t)}m))$.


Perhaps the complexity is even $O(poly(ntm))$.



Lower bound for polyhedral real quantifier elimination
I believe the following is a counterexample to the stronger $O(\mathrm{poly}(n,t,m))$ conjecture. Start with variables $x\_i$ for $1 \leq i \leq n$ and $t\_{ij}$ for $1 \leq i < j \leq n$. Consider the formula
$$\phi=\exists t\_{12} \ldots \exists t\_{n-1,n}\left(\bigwedge\_i x\_i = \sum\_{j<i} t\_{ji} - \sum\_{j>i} t\_{ij}\right) \wedge\left(\bigwedge\_{i,j}0 \leq t\_{ij} \leq 1\right).$$
Eliminate the $t\_{ij}$. Then $\phi$ holds if and only if $(x\_1, \ldots, x\_n)$ is in the Minkowski sum of the $\binom{n}{2}$ vectors $e\_i - e\_j$. This Minkowski sum is a permutahedron with one defining equality and $2^{n}-2$ defining inequalities. 


The number of variables $\binom{n}{2}+n$, number of atomic formulas $n^2$ and largest number of terms in one atomic formula $n$ are all polynomial in $n$, but $2^n-2$ is not.


Still thinking about if I can beat $O(\mathrm{poly}(n^t, m))$ or get double exponential. 


**Example of the above:** Let $n=4$. Then $\phi$ is the quantified conjunction of the $4^2$ atomic formulas:
$$x\_1 = -t\_{12}-t\_{13}-t\_{14}$$
$$x\_2 = t\_{12}-t\_{23}-t\_{24}$$
$$x\_3 = t\_{13} + t\_{23} - t\_{34}$$
$$x\_4 = t\_{14} + t\_{24} + t\_{34}$$
$$0 \le t\_{12} \le 1,\ \ 0 \le t\_{13} \le 1,\ \ 0 \le t\_{14} \le 1$$
$$0 \le t\_{23} \le 1,\ \ 0 \le t\_{24} \le 1,\ \ 0 \le t\_{34} \le 1$$


And $\phi$ holds iff the conjunction of the following $2^4-1$ atomic formulas holds:
$$x\_1 + x\_2 + x\_3 + x\_4 = 0$$
$$-2 \le \ \ \ x\_2 \ \ \ \le 1$$
$$-1 \le \ \ \ x\_3 \ \ \ \le 2$$
$$\ \ 0 \le \ \ \ x\_4 \ \ \ \le 3$$
$$-2 \le \ \ x\_2 + x\_3 \ \ \le 2$$
$$-1 \le \ \ x\_2 + x\_4 \ \ \le 3$$
$$\ \ 0 \le \ \ x\_3 + x\_4 \ \ \le 4$$
$$\ \ 0 \le x\_2 + x\_3 + x\_4 \le 3$$


