Two-variable LP in quadratic time on the real RAM

There are a single program $R$ of the real pointer machine of Definitions.Def_SmaleNinth_RealRAM and a constant $C$ such that, for every $m$, every $A \in \mathbb{R}^{m\times 2}$ and every $b \in \mathbb{R}^m$, the machine started with memory encodeLP A b halts within $C(m+1)^2$ steps and accepts exactly when the system $a_i x + b_i y \ge c_i$, $i < m$, has a solution in $\mathbb{R}^2$.

The algorithm is Fourier–Motzkin elimination fused with the one-variable sweep. Eliminating the second variable replaces the system by a one-variable system consisting of the rows with vanishing second coefficient together with one combined row for each pair of rows whose second coefficients have opposite signs. Rather than materialising that system, whose size is quadratic, the program runs a double loop over all ordered pairs of rows and feeds each derived constraint directly into the running interval $[L, R]$ maintained by the one-variable procedure, together with the presence flags and the infeasibility flag. Pairs that produce no constraint are fed the vacuous inequality $0 \ge 0$, so every pass performs the same bounded amount of work.

This is the case $n = 2$ of fixed-dimension linear programming. Megiddo and Dyer showed that for each fixed number of variables the problem is solvable in time linear in the number of constraints, by prune-and-search; the bound above is the weaker quadratic one that the naive elimination gives, and it is stated on the same machine model and input convention as the mission's goal, so the two are directly comparable. Together with the one-variable result it makes the first two rungs of the fixed-dimension ladder available in the model in which Smale's ninth problem is posed here.

Formalization note. The program has 90 instructions. The correctness proof separates the machine-independent part — the abstract state, its update along one constraint, and the correctness of the verdict, reused from the one-variable development — from the machine part, where a reachability calculus with one lemma per instruction is used to verify the initialisation, the row-reading and case analysis that computes the constraint fed at each pair, the update block, the two nested loops, and the final decision.