% =====================================================================
\section{Linear programming duality in \texorpdfstring{$\RCA$}{RCA0}: the details}\label{app:lp}
% =====================================================================

This appendix expands the proof of \cref{thm:lp-rca}. Throughout we work in $\RCA$; the sizes $m$ and $n$ are
arbitrary natural numbers, possibly non-standard, and the data $A,b,c$ are finite sequences of reals, coded as usual
by a single set. Only $\Sigma^0_1$ induction (equivalently $\Pi^0_1$ induction) and bounded $\Sigma^0_1$
comprehension are used.

\paragraph{Step 1: formal polynomials and their values.}
Integer polynomials in finitely many variables are finite objects, coded by natural numbers. Evaluation at a finite
sequence of reals is defined by primitive recursion on the polynomial, and $\RCA$ proves, by $\Pi^0_1$ induction on
the size of the polynomials involved, that evaluation is a ring homomorphism: the value of $p+q$ is the sum of the
values, and similarly for products. (Each of these is a statement $\forall p,q\,\Pi^0_1$, because equality of reals is
$\Pi^0_1$.) Consequently every identity between integer polynomials that holds formally, i.e.\ that is a
true equality of finite objects after expansion into monomials, transfers to the corresponding identity between reals.
The determinant of an $r\times r$ matrix is the value of the Leibniz polynomial, a sum of $r!$ terms; this is a finite
sum and exists for every $r$. The identities we need are formal identities with the size $r$ as a parameter:
expansion along a row or column, multilinearity, Cramer's rule in the form $\det(B)\,x_B=\big(\det B^{(i\leftarrow
b)}\big)_i$, and the description of the entries of a simplex tableau as quotients of minors of the bordered matrix.
Their usual proofs are combinatorial arguments about finite objects: they are $\Delta_0(\exp)$ identities proved by
bijections and sign-reversing involutions on the symmetric group $S_r$, so $\mathsf{I}\Delta_0+\exp$, which is
contained in $\mathsf{I}\Sigma_1$, the first-order part of $\RCA$, suffices (compare the much finer analysis of linear
algebra in weak theories by Soltys and Cook \cite{SoltysCook2004}). This is also why the textbook proofs of duality
by induction on $m+n$ cannot be used directly: for non-standard sizes such an induction would range over formulas
that quantify over real vectors, i.e.\ over sets, and $\RCA$ has no induction for them. The sign oracle below
replaces that induction by a single application of comprehension.

\paragraph{Step 2: the sign oracle.}
Put the primal problem in equality form with slack variables, $[A\ I]\,(x,s)=b$, $(x,s)\ge0$. Let $\mathcal E$ be the
finite list of integer polynomials in the entries of $(A,b,c)$ consisting of: the entries $b_i$; all minors of the
bordered matrices of Phase~I (constraint matrix with rows multiplied by $\pm1$ and artificial columns, right-hand side,
Phase~I cost row) and of Phase~II (constraint matrix, right-hand side, cost row), for every choice of the row signs;
and all expressions $\mu_1\mu_2-\mu_3\mu_4$ with $\mu_1,\dots,\mu_4$ such minors. The length of $\mathcal E$ is bounded
by an explicit (exponential) function of $m+n$. The values $v_e$ ($e\in\mathcal E$) form a finite sequence of reals,
and ``$v_e>0$'' and ``$v_e<0$'' are $\Sigma^0_1$ uniformly in $e$. By bounded $\Sigma^0_1$ comprehension
\cite[II.3]{Simpson2009SOSOA} the finite sets $\{e:v_e>0\}$ and $\{e:v_e<0\}$ exist, so the sign function
$\sigma\colon\mathcal E\to\{-1,0,1\}$ with $\sigma(e)=\operatorname{sign}(v_e)$ exists as a finite object. This is the
only point at which the proof is not uniform in the data.

\paragraph{Step 3: the symbolic run.}
The two-phase simplex method with Bland's smallest-index rule \cite{Bland1977} is a primitive recursive procedure that
takes $\sigma$ (and $m,n$) as input and manipulates bases, i.e.\ finite sets of column indices. At a basis $B$ every
quantity the method inspects is the sign of a tableau entry, of a reduced cost, or of a difference of two ratios in a
ratio test; by Step~1 each of these signs equals $\sigma(e)$ or $\sigma(e)\sigma(e')$ for explicitly computable
$e,e'\in\mathcal E$ (for ratios, multiply out the positive denominators). Ties are decided by $\sigma(e)=0$, and
Bland's rule breaks them by the smallest index. So the run, a finite sequence of bases $B_0,B_1,\dots$ together with
the outcome, is defined by primitive recursion from $\sigma$. By $\Delta^0_0$ induction (in the parameter $\sigma$) on
$t$, the sign data of $B_t$ certify feasibility: $\sigma(\Delta_{B_t})\neq0$ and $\sigma(\mu_i)\sigma(\Delta_{B_t})\ge0$
for the minors $\mu_i$ that give the basic variables by Cramer's rule; the induction step is the usual verification
that a pivot chosen by the ratio test preserves feasibility, which is an identity between quotients of minors together
with the signs supplied by $\sigma$. Because $\sigma$ agrees with the true signs, each $B_t$ is a basis that is
feasible for the real data.

\paragraph{Step 4: termination.}
Bland's proof that his rule never revisits a basis considers a hypothetical cycle, the largest index that enters
and leaves in it, and two tableaux of the cycle; the identity that the cost row of one tableau is orthogonal to the
direction defined by the entering column of the other, together with the signs forced by the rule, gives a
contradiction. All of this concerns finitely many reals given by quotients of minors and their signs, so it is
available in $\RCA$ by Steps~1 and~3. Hence no basis repeats, and by the finite pigeonhole principle (provable in
$\mathsf{I}\Sigma_1$) each phase stops after at most $\binom{n+2m}{m}$ pivots.

\paragraph{Step 5: Phase I.}
Multiply the rows with $\sigma(b_i)=-1$ by $-1$ and add one artificial variable per row. The artificial basis is
feasible, and Phase~I minimizes the sum of the artificial variables. Phase~I cannot be unbounded, since an improving
ray would make the sum of the non-negative artificial variables negative. Its optimal value is $0$, because the primal
is feasible and the value is a lower bound for the sum of artificials at any feasible point. Artificial variables that
remain basic at level $0$ are pivoted out by degenerate pivots on non-zero entries of their rows in original columns;
such entries exist because $[A\ I]$ has rank $m$, and their non-zeroness is again read off $\sigma$. This yields a
feasible basis of the sign-flipped system, which is also a basis of the original system $[A\ I]$ with the same basic
solution; Phase~II is run on the original, unflipped system, so that the dual vector below is expressed in the
original coordinates.

\paragraph{Step 6: Phase II and the conclusion.}
Phase~II stops either at an optimal basis, where no column can improve the objective, or with an improving column $j$
whose entries are all non-positive. In the second case the column yields a ray $r\ge0$ with $Ar\le0$ along which the objective increases without
bound. This contradicts weak duality: for a dual feasible $y\ge0$ and every primal feasible $x$,
$c^\top x\le y^\top Ax\le y^\top b$, an inequality between finitely many reals. In the first case let $B$ be the final
basis. Cramer's rule gives the basic solution $x^\ast$ and $y^{\ast\top}=c_B^\top B^{-1}$ as explicit quotients of minors;
the optimality condition on the reduced costs says exactly that $A^\top y^\ast\ge c$ (structural columns) and
$y^\ast\ge0$ (slack columns), and $c^\top x^\ast=c_B^\top B^{-1}b=b^\top y^\ast$ is a formal identity.

\paragraph{Step 7: minimax.}
Let $P\in\R^{m\times n}$, $m,n\ge1$, be a payoff matrix (the row player maximizes $p^\top Pq$, the column player
minimizes it). Choose a rational
$t>1+\max_{ij}\abs{P_{ij}}$ (from approximations of the entries) and put $Q=P+t$, which has positive entries. The
linear programs $\max\{\mathbf 1^\top x:Qx\le\mathbf 1,x\ge0\}$ and $\min\{\mathbf 1^\top y:Q^\top y\ge\mathbf 1,
y\ge0\}$ are dual to each other and both feasible ($x=0$, and $y$ a large multiple of $\mathbf 1$), so by Steps~2--6
they have optimal solutions with a common value $\theta$, and $\theta>0$ because $Q^\top y^\ast\ge\mathbf 1$ forces
$y^\ast\neq0$. Then $q=x^\ast/\theta$ and $p=y^\ast/\theta$ are mixed
strategies with $p^\top Q\ge\theta^{-1}\mathbf 1^\top$ and $Qq\le\theta^{-1}\mathbf 1$, so the game $Q$ has value
$\theta^{-1}$ and the game $P$ has value $\theta^{-1}-t$, attained by $p$ and $q$. All steps are uniform in $m$ and $n$.
\qed

\paragraph{Remark.}
Fourier--Motzkin elimination gives an alternative route: one application of bounded $\Sigma^0_1$ comprehension to the
pre-enumerated (doubly exponential) list of the polynomials that Fourier--Motzkin elimination produces yields Farkas'
lemma in $\RCA$, and duality follows by the usual homogenization. It avoids Phase~I and anticycling at the cost of a
larger list.