Model sanity, real RAM: one-variable LP in linear time

On the real pointer machine of Definitions.Def_SmaleNinth_RealRAM (real registers, integer pointer registers, a memory indexed by $\mathbb{Z}$, unit cost per instruction, indirect addressing through pointers), one-variable linear programming feasibility is decidable in linear time.

Precisely: there are a single program $R$ and a constant $C$ such that for every $m$, every $A \in \mathbb{R}^{m \times 1}$ and every $b \in \mathbb{R}^m$, the machine started with memory encodeLP A b halts within $C\,(m+1)$ steps, and it accepts exactly when the system $a_i x \ge b_i$, $i < m$, has a solution $x \in \mathbb{R}$.

The algorithm is the obvious sweep: maintain the running lower bound $L = \max\{b_i/a_i : a_i > 0\}$, the running upper bound $R = \min\{b_i/a_i : a_i < 0\}$, presence flags for the two, and a flag recording whether some constraint with $a_i = 0$ and $b_i > 0$ has been seen; the system is feasible iff no such constraint occurs and $L \le R$ whenever both bounds are present. Each constraint costs $O(1)$ instructions because the coefficient $a_i$ and the right-hand side $b_i$ are reached through two pointers that are incremented once per step.

This is the exact counterpart, in the random-access model, of the milestone statement SmaleNinth.bss_decides_one_variable_lp, which is false in the fixed-address tape model: there the two halves of a constraint sit $m$ cells apart and a crossing-sequence argument forces $\Omega(m^2)$ steps (SmaleNinth.bss_one_variable_lp_no_linear_program). Together the two statements separate the two machine models at linear time and show that the quadratic overhead of the compiler SmaleNinth.ram_to_bss_quadratic_nonneg is not an artifact of the construction.