No linear-time BSS program for one-variable LP feasibility

This is the negative form of the one-variable model-sanity statement: in the machine model of the mission, a fixed program cannot decide one-variable linear feasibility in time linear in the number of constraints.

The assertion. For every program $P$ over the reals in the fixed instruction set (real constants, field arithmetic at fixed addresses, two-sided tape shifts, a sign-test branch) and every constant $C$, there exist $m$ and a one-variable system $a_i x \ge b_i$ ($i = 1, \dots, m$) such that $P$, started on the standard encoding, does not halt with the correct verdict within $C(m+1)$ steps.

Why. Every instruction addresses cells at fixed offsets from the head, so a program is a window of fixed width $2W+1$ sliding along the tape one cell per shift. The coefficient $a_i$ and the right-hand side $b_i$ sit $m$ cells apart. In $C(m+1)$ steps some boundary between the two blocks is crossed at most $C+1$ times, so the computation is determined across that boundary by the window contents at those crossings, a transcript of at most $(C+1)(2W+1)$ real numbers. On corner instances (coefficients $x \in \mathbb{R}^p$ and right-hand sides equal to $x$, plus a sentinel constraint $x \le 1$) equal transcripts allow cutting and pasting the two runs into the mixed instance $(x, x')$, which must then be declared feasible, forcing $x' \le x$ and symmetrically $x = x'$. Hence the transcript is injective on an open subset of $\mathbb{R}^p$ with $p > (C+1)(2W+1)$; but near a generic input the transcript is a $C^1$ function of the input, and a $C^1$ map into a space of smaller dimension is injective on no open set.

Context. The quadratic budget $C(m+1)^2$ is attainable (SmaleNinth.bss_decides_one_variable_lp_quadratic), so this theorem pins the complexity of the one-variable problem in this model at $\Theta(m^2)$. It is the positive-statement form of the disproof of SmaleNinth.bss_decides_one_variable_lp, published so that other lower bounds can import it.