Read-back: SmaleNinth.bss_decides_one_variable_lp

The statement asserts the existence of one fixed program $P$ and one fixed natural-number constant $C$, chosen before anything else, that work uniformly for every instance. Precisely, the quantifier order is:

$P$ run on the encoded instance halts with output $\text{result}$ within $C \cdot (m+1)$ steps, and $\text{result} = \mathrm{true}$ if and only if the set $\{x \in \mathbb{R}^{1} \mid A x \ge b\}$ is nonempty. The boolean $\text{result}$ is existentially quantified inside the instance quantifiers, so it may depend on the instance; the "iff" conjunct pins it to the truth value of feasibility. Here $m$ ranges over all naturals, including $m = 0$.

The machine model. A program $P$ is a finite list of instructions for a register machine whose configuration is a program counter $\mathrm{pc} \in \mathbb{N}$ together with a bi-infinite tape $x : \mathbb{Z} \to \mathbb{R}$ of real registers. The instructions are: load a constant ($x[d] := c$ for an arbitrary real $c$ hard-coded in the instruction), the four field operations $x[d] := x[i] \mathbin{\text{op}} x[j]$ on fixed integer addresses $d, i, j$ (with division totalized so that $y / 0 = 0$), a left shift (new $x[k] =$ old $x[k+1]$) and a right shift (new $x[k] =$ old $x[k-1]$) of the entire tape, a conditional jump ("if $x[i] \le 0$ set $\mathrm{pc} := \text{target}$, else $\mathrm{pc} := \mathrm{pc}+1$"), and two halting instructions, accept and reject. Every non-jump, non-halt instruction advances the program counter by one. A configuration whose program counter points at accept or reject, or points outside the program list entirely, is a fixed point of the step function (the step leaves it unchanged).

What "decides in time $T$" means. Writing $s_t$ for the configuration reached after exactly $t$ applications of the step function starting from program counter $0$ and initial tape $x$, the predicate asserted here is:

with $T = C \cdot (m+1)$. Note this requires the program counter to sit on an accept/reject instruction of $P$ at some time $t \le T$: a run whose counter merely falls off the end of the program never counts as halting with an output. Each executed instruction — arithmetic operation, shift, jump, or comparison — costs one step; the bound counts steps, so the running time is at most $C(m+1)$, i.e. linear in $m$ with the same multiplicative constant $C$ for every instance. (Nothing constrains $C$ beyond being some natural number; the bound at $m = 0$ is $C \cdot 1 = C$.)

The input encoding ($n = 1$ case of encodeLP). The initial tape is: cell $0$ holds the real number $m$; cell $1$ holds the real number $1$ (the value of $n$); cells $2, 3, \dots, m+1$ hold the column entries $A_{1,1}, A_{2,1}, \dots, A_{m,1}$ (the row-major listing of the $m \times 1$ matrix, entry $A_{i,1}$ in cell $i + 1$ for $i = 1, \dots, m$); cells $m+2, \dots, 2m+1$ hold $b_1, \dots, b_m$; every other cell of the bi-infinite tape is $0$, including all cells with negative index. When $m = 0$ the matrix and vector blocks are empty, so the tape is $0$ everywhere except cell $1$, which holds $1$.

The decided set. polyhedron $A\ b$ is the set $\{x : \mathrm{Fin}\,1 \to \mathbb{R} \mid b \le Ax\}$, where $Ax$ is the matrix–vector product and $\le$ is componentwise; for $n = 1$ this is, identifying $x$ with a single real,

Nonemptiness of this set is exactly one-variable LP feasibility: $\exists\, x \in \mathbb{R}$ satisfying all $m$ inequalities. In the edge case $m = 0$ there are no inequalities, the condition $b \le Ax$ is vacuously true, the set is all of $\mathbb{R}^1$ and hence nonempty — so on the ($m = 0$)-instance's near-blank tape the program is required to reach accept within $C$ steps.

In summary: the theorem claims a single BSS-style program over $\mathbb{R}$ (with unit-cost exact real arithmetic and arbitrary real machine constants) and a single constant $C$ such that, for every number of constraints $m$ and every real one-variable system $a_i x \ge b_i$ ($i = 1, \dots, m$) presented in the tape encoding above, the program halts on accept or reject within $C(m+1)$ steps, halting on accept precisely when the system has a real solution.