Lower bound for polyhedral real quantifier elimination 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))$.
 A: 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$$
