% =====================================================================
\section{Introduction}\label{sec:intro}
% =====================================================================

Optimization theory proves three kinds of theorems. \emph{Existence} theorems say that an optimal point exists:
a continuous function on a compact set attains its minimum; a coercive lower semicontinuous convex functional on
a Hilbert space has a minimizer. \emph{Convergence} theorems say that an algorithm reaches one: gradient descent,
the proximal point method, the Krasnosel'ski\u{\i}--Mann and Halpern iterations. \emph{Certification} theorems
say that optimality can be verified: Lagrange and Fenchel duality, separating hyperplanes, the minimax theorem,
K\H{o}nig's theorem and max-flow/min-cut. Optimizers know that these three kinds of statements behave differently.
Existence is cheap to state and often cheap to prove; convergence comes with rates for some quantities and not for
others; certificates are finite objects in finite dimensions and delicate ones in infinite dimensions.

This paper makes the difference precise, using three rulers from mathematical logic:
\begin{itemize}[nosep]
  \item \emph{reverse mathematics} \cite{Simpson2009SOSOA,Hirschfeldt2014,DzhafarovMummert2022}, which measures the
  set-existence axioms a theorem needs;
  \item \emph{Weihrauch complexity} \cite{BrattkaGherardiPauly2021}, which measures how hard it is to compute a
  witness uniformly in the data;
  \item \emph{proof mining} \cite{Kohlenbach2008APT}, which extracts the quantitative content (rates, bounds,
  metastability) that a proof implicitly carries.
\end{itemize}
Each ruler has been applied to optimization before, often deeply. The extreme value theorem is the textbook
example of a statement equivalent to weak K\H{o}nig's lemma. Proof mining began partly in Chebyshev approximation
\cite{Kohlenbach1993Chebycheff} and has produced explicit rates for Krasnosel'ski\u{\i}--Mann, Halpern, proximal
point and other Fej\'er-type methods of convex optimization \cite{Kohlenbach2019ICM}. Neumann classified fixed-point problems for nonexpansive maps in the Weihrauch
lattice \cite{Neumann2015LMCS}, Kohlenbach calibrated moduli of regularity in reverse mathematics
\cite{Kohlenbach2019Moduli}, Fern\'andez-Duque, Shafer and Yokoyama calibrated Ekeland's variational principle
\cite{FernandezDuqueShaferYokoyama2020}, and bounded arithmetic characterized local search \cite{BK94}. But these
results are scattered over several literatures that rarely cite each other, and they are stated in languages
that optimizers do not use. What has been missing is a single map on which the three kinds of theorems can be
compared, in the language of optimization, together with an explanation of the patterns on the map. This paper
provides both, and proves new results where the map had holes.

\input{fig_map}

\paragraph{The map.}
\Cref{fig:map} places the main principles of optimization in the hierarchy of subsystems of second-order
arithmetic. Three patterns stand out, and each is the subject of a part of the paper.

\begin{enumerate}[leftmargin=1.5em]
\item \emph{Convexity and tameness collapse existence} (\cref{sec:existence}). A continuous function on $[0,1]$
attains its maximum; this is equivalent to $\WKL$, and there are computable functions with no computable maximizer.
A \emph{convex} function on $[0,1]$ attains its minimum provably in $\RCA$, and so does a convex function on
$[0,1]^n$ that comes with a modulus of uniform continuity (\cref{thm:convex-rca}); every computable convex function
has a computable minimizer, and convex minimization is Weihrauch equivalent to convex choice
(\cref{prop:cmin-weihrauch}). Existence of optima for polynomial problems of fixed format is provable in $\RCA$ by
Tarski transfer (\cref{prop:tarski}). At the other end, Ekeland's variational principle, the engine of modern
variational analysis, is equivalent to $\PiCA$ in its general forms (\cref{fact:beyond}).
\item \emph{Convergence costs a jump, because convergence selects} (\cref{sec:convergence}). Already in dimension
one, convergence of gradient descent for convex $L$-smooth functions is equivalent to $\ACA$, the strength of the
monotone convergence theorem (\cref{thm:A}, implicit in work of Kohlenbach and Neumann). The reason is not that
minimizers are hard to find, but that the algorithm commits to a particular one, in dimension one the projection of
its starting point onto the solution set, and this selection is as hard as the halting problem; anchored methods make
the same choice in every dimension (\cref{thm:D}). Uniqueness and
error bounds remove the cost (\cref{thm:B}). Between rates and convergence, the iterates of gradient descent carry a
dimension-dependent but otherwise uniform bound on fluctuations (\cref{thm:E}), and in dimension at least two the
coordinates of their limits on computable instances are exactly the d.c.e.\ reals (\cref{thm:F}).
\item \emph{Duality climbs the hierarchy with the infinitary content of the certificate} (\cref{sec:duality}).
Finite linear programming duality is provable in $\RCA$ (\cref{thm:lp-rca}); separation and Hahn--Banach are
equivalent to $\WKL$, and strict separation from a separably closed set to $\ACA$; K\H{o}nig's duality theorem for
countable bipartite graphs is equivalent to $\ATR$, and the extended forms of K\H{o}nig's and Menger's theorems reach
$\PiCA$.
\end{enumerate}

Two further parts complete the picture. \Cref{sec:proofmining} is a guide to proof mining in optimization and
explains, through Kohlenbach's metatheorems, why dimension-free complexity bounds are so common in convex
optimization: they are what proofs that never use compactness of the ambient space must produce.
\Cref{sec:feasible} turns to the finite world, where bounded arithmetic plays the role of second-order arithmetic:
the $\NP$ search problems provably total in $T^1_2$ are exactly those reducible to local search problems
\cite{BK94}, finding approximate stationary points of smooth functions (equivalently, approximate fixed points of
gradient descent) is complete for $\CLS=\PPAD\cap\PLS$ \cite{FGHS21}, and cutting planes, branch-and-cut and
sum-of-squares are proof systems.

\paragraph{What is new.}
The paper is partly a survey and partly a research article. The survey part restates known calibrations in the
language of optimization, with precise references; in particular \cref{thm:A,thm:D,thm:B} are known in substance from
the work of Kohlenbach, L\'opez-Acedo, Nicolae and Neumann. \Cref{tab:new} lists the results that we prove, with the
nearest prior result for each, as far as we could determine it. The two that we regard as genuinely new theorems are
\cref{thm:convex-rca}(a) and \cref{thm:lp-rca}; the others are observations or corollaries whose interest lies in the
connections they make.

\begin{table}[t]
\centering
\footnotesize
\renewcommand{\arraystretch}{1.15}
\begin{tabularx}{\linewidth}{@{}>{\raggedright\arraybackslash}p{0.27\linewidth}>{\raggedright\arraybackslash}X>{\raggedright\arraybackslash}p{0.3\linewidth}@{}}
\toprule
Result & Nearest prior work & What is added \\
\midrule
\Cref{thm:convex-rca}(a): $\RCA$ proves that convex functions on $[0,1]$ attain their minima &
informal remark of Friedman \cite{Friedman2009FOMConstructiveAnalysis}; $\IVT$ and the mean value theorem in $\RCA$
\cite{Simpson2009SOSOA,HardinVelleman2001MVT} & a proof, without any modulus hypothesis \\
\Cref{thm:convex-rca}(b): the same on $[0,1]^n$, given a modulus & computable points of convex sets
\cite{LeRouxZiegler2008} & reduction to dimension one; the modulus is the remaining gap (\cref{prob:uniform-n}) \\
\Cref{thm:lp-rca}: LP duality and minimax in $\RCA$, all sizes & Farkas $\Leftrightarrow\LPO$ in BISH
\cite{BergerSvindland2022Farkas}; Weihrauch degree of linear inequalities \cite{Pauly2010Nash} & the sign-pattern
argument; uniform in the size \\
\Cref{prop:tarski}: Tarski transfer & folklore (the reals of $\RCA$ form a real closed field) & optimization
corollaries for fixed formats \\
\Cref{prop:cmin-weihrauch}: $\CMin_n\seqv\XC_n$ & implicit in Neumann's constructions \cite{Neumann2015LMCS} & explicit
statement and a direct proof \\
\Cref{prop:kkt1}: $\KKT_1\seqv\IVT$ & $\BFT_1\seqv\IVT$ \cite{BrattkaLeRouxMillerPauly2019,Neumann2015LMCS} & the
exact KKT problem; \cref{prob:kkt} \\
\Cref{thm:E}: fluctuations and dimension & path-length bounds
\cite{DaniilidisDavidDurandCartagenaLemenant2015,GuptaBalakrishnanRamdas2021,BohmDaniilidis2022Ubiquitous}; norm
non-convergence in $\ell^2$ \cite{BauschkeMatouskovaReich2004Projection} & proof-mining reading; finite-dimensional
lower bound; comparison with generic bounds \\
\Cref{thm:F}: limits of gradient descent & \cite{AmbosSpiesWeihrauchZheng2000WeaklyComputable,
ZhengRettingerBarmpalias2005hMonotonically,Neumann2015LMCS} & the characterization for gradient descent \\
\bottomrule
\end{tabularx}
\caption{Results proved in this paper and their nearest predecessors.}
\label{tab:new}
\end{table}

\paragraph{Five principles.}
The results suggest five principles, which we state informally and revisit in \cref{sec:synthesis}.
\begin{enumerate}[label=\textbf{P\arabic*.},nosep,leftmargin=2.2em]
\item \emph{Convexity and tameness substitute for compactness.} They lower the cost of existence from $\WKL$ to
$\RCA$ (for convex functions: in dimension one, and in each fixed dimension given a modulus of uniform continuity;
for polynomial problems: format by format), in classical reverse mathematics as in Bishop's constructive mathematics.
\item \emph{Selection is the price of convergence.} Gradient descent (in dimension one) and anchored methods (in every
dimension) choose a particular minimizer, the projection of the starting point or anchor, and this choice is
$\lm$-hard even when finding some minimizer is non-uniformly computable.
\item \emph{Uniqueness and regularity are computational resources.} A modulus of uniqueness or regularity is
exactly the datum that turns convergence into a rate.
\item \emph{Bounds on values are cheap, convergence of iterates is not.} The uniform rates for function values and
gradients follow from finitely many inequalities and have $\Pi^0_1$ proofs; convergence of iterates is a $\Pi^0_3$
statement and comes, in general, only with metastability. (This is a heuristic, not a theorem: logical form alone does
not decide whether a bound exists.)
\item \emph{Dimension is the price of compactness.} Bounds extracted from proofs that use compactness of the space
depend on its dimension, and for gradient descent this dependence is unavoidable.
\end{enumerate}

\paragraph{Organization.}
\Cref{sec:prelim} introduces the logical toolkit for optimizers and the convex toolkit for logicians.
\Cref{sec:existence,sec:convergence} treat existence and convergence, \cref{sec:proofmining} proof mining,
\cref{sec:duality} duality, and \cref{sec:feasible} the feasible world. \Cref{sec:synthesis} collects the principles
and open problems. \Cref{app:formal} records formalization details, \cref{app:experiments} the computations behind
\cref{fig:specker}, and \cref{app:lp} the full proof of \cref{thm:lp-rca}.

\paragraph{AI disclosure.}
This paper was written with Claude Opus~5.5 (Anthropic), working as an agent in Claude Code. The author
posed the question of how reverse mathematics bears on optimization. Claude chose the results, proved them, wrote
the text and drew the figures. Separate Claude agents searched the literature, checked the citations against their
sources, attacked the new results and reviewed the paper as referees, and the paper was revised to address their
findings. The constructions behind \cref{fig:specker} and the staircase bound were checked numerically. No part of
this paper is formally verified. The author is responsible for the content.