Size of the Fourier-Motzkin eliminated system

One step of Fourier–Motzkin elimination replaces a system of $N$ inequalities by one indexed by the rows together with the ordered pairs of rows, that is by $N + N^2$ inequalities. Iterating from $m$ inequalities, the number of rows after $n$ eliminations therefore satisfies

The proof is an induction on $n$ using $N + N^2 + 1 \le (N+1)^2$, which is what makes the shifted quantity $\#+1$ the right one to bound: the bound squares at each step exactly as the exponent doubles.

Combined with SmaleNinth.lp_fourier_motzkin_decides, this makes the classical decision procedure for real linear feasibility quantitative. Feasibility of a system of $m$ inequalities in $n$ variables is equivalent to a conjunction of at most $(m+1)^{2^n}$ sign conditions, each of them an explicit polynomial expression in the entries of the system. For a fixed number of variables that is polynomial in the number of constraints, which is the general form of the fixed-dimension results and covers the two machine theorems of this mission as the cases $n = 1$ and $n = 2$.

It also marks precisely where the method fails to bear on the mission's goal. The exponent $2^n$ is doubly exponential in the number of variables, whereas Smale's ninth problem asks for a number of arithmetic operations polynomial in the number of constraints and variables together. Any strongly polynomial algorithm must therefore avoid materialising the eliminated systems.