% =====================================================================
\section{Formalization notes}\label{app:formal}
% =====================================================================

We record the points at which the proofs of \cref{thm:A,thm:D,thm:lp-rca} use facts about $\RCA$ that are
standard but easy to overlook.

\begin{enumerate}[leftmargin=1.5em]
\item \emph{Iterates exist.} By \eqref{eq:pair}, $g$ is $L$-Lipschitz (add the two upper inequalities at $(x,y)$ and
$(y,x)$ and use co-coercivity). So an approximation of $x_{k+1}$ to precision $2^{-n}$ needs only an approximation of
$x_k$ to precision $2^{-n-c}$, for a constant $c$ depending on $L$, and one value of $g$ at a rational point. The
iterates are therefore defined by primitive recursion on a $\Delta^0_1$ table of values of $g$, and no $\Pi^0_2$
induction is needed to show that they exist. ``The gradient-descent sequence converges'' then refers to this sequence.
\item \emph{The function $f_y$.} For $x$ in a bounded interval, the series defining $f_y$ and $f_y'$ converge
uniformly with an explicit modulus (the tail after $s$ terms is at most $2^{-s}$ times a bound on $(y_s-x)^2$), so the
pair $(f_y,f_y')$ exists as a pair of codes of continuous functions in $\RCA$, and \eqref{eq:pair} with $L=2$ holds
because it holds for every partial sum and is preserved under limits.
\item \emph{Comparison arguments.} The statements ``$x_k\le z$ for all $k$'' in the proofs of \cref{thm:A,thm:D} are
$\Pi^0_1$ and are proved by $\Pi^0_1$ induction, which is available in $\RCA$.
\item \emph{The final search.} To decide $m\in\operatorname{ran}(h)$ from $x_\infty$, search for $n$ with
$\hat x-y_n<2^{-m-2}$, where $\hat x$ is the approximation of $x_\infty$ to precision $2^{-m-3}$ supplied by its
code. The search terminates because $y_n\to x_\infty$, and any $n$ found satisfies $x_\infty-y_n<2^{-m-1}$.
\item \emph{Bounded comprehension.} In \cref{thm:lp-rca}, the sign pattern of finitely many reals is obtained by
bounded $\Sigma^0_1$ comprehension, which is provable in $\RCA$ \cite[II.3]{Simpson2009SOSOA}; everything else is
first-order reasoning about finitely many explicitly given reals.
\end{enumerate}

% =====================================================================
\section{The computations behind \texorpdfstring{\cref{fig:specker}}{Figure 2}}\label{app:experiments}
% =====================================================================

The instance in \cref{fig:specker} is gradient descent with step $1/2$ from $x_0=0$ on the function $f_y$ of
\eqref{eq:fy}, for the data $y_s=\sum_{r\le s}b_r$, where $b_r=10^{-4}(r+1)^{-3/2}$ plus a jump $2^{-m-1}$ at stages
$r=0,30,300,3000,30000$ with $m=1,3,4,5,6$. The background term keeps $(y_s)$ strictly increasing; the late jumps
imitate the enumeration of small elements of a computably enumerable set. All quantities are computed in $80$-digit
decimal arithmetic. The series for $f_y$ and $f_y'$ are truncated after $210$ terms, which changes them by less than
$10^{-63}$; the limit $x_\infty=\sup_sy_s$ is computed from the data, including the tail of the background term.
Over the $10^5$ steps shown, $f(x_k)-f^\ast$ stays far below the bound $LD^2/(2k)$ of \cref{lem:basic}(c), and the
gradient decays to about $10^{-10}$, while $x_\infty-x_k$ stays at $0.117$. The scripts are available with the
source of this paper.