% =====================================================================
\section{Existence: what it costs to have a minimizer}\label{sec:existence}
% =====================================================================

The first question an optimizer asks is whether the problem has a solution. The classical answer is
compactness. This section shows that compactness is expensive, and that the two structural assumptions that
optimization relies on most, convexity and semialgebraic tameness, make it unnecessary: convexity in dimension one,
and in each fixed dimension once a modulus of uniform continuity is given; tameness format by format.

\subsection{The baseline: compactness costs weak K\H{o}nig's lemma}\label{subsec:compactness}

\begin{fact}\label{fact:evt}
\leavevmode
\begin{enumerate}[nosep,label=\textup{(\alph*)}]
\item Over $\RCA$, $\WKL$ is equivalent to the maximum principle: every continuous $f\colon[0,1]\to\R$ attains its
supremum \textup{\cite[Theorem I.10.3 and \S IV.2]{Simpson2009SOSOA}}. Each of ``every such $f$ is bounded'' and
``every such $f$ is uniformly continuous'' is also equivalent to $\WKL$.
\item Finding a maximizer of $f\in C[0,1]$ is strongly Weihrauch equivalent to $\Cch_{[0,1]}\seqv\WKLp$
\textup{\cite{Brattka2016Historical}, \cite[Theorem 8.3]{BrattkaGherardiPauly2021}}. There is a computable
$f\colon[0,1]\to\R$ that attains its maximum only at non-computable points (Lacombe; Specker
\cite{Specker1959}).
\item Brouwer's fixed point theorem for $[0,1]^n$, $n\ge2$, is equivalent to $\WKL$
\textup{\cite{ShiojiTanaka1990}} and to $\WKLp$ in the Weihrauch lattice \textup{\cite{BrattkaLeRouxMillerPauly2019}};
for $n=1$ it is provable in $\RCA$ and Weihrauch equivalent to $\IVT$. Peano's existence theorem for ordinary differential
equations is equivalent to $\WKL$, while the existence of Osgood's \emph{maximal} solution is equivalent to $\ACA$
\textup{\cite{Simpson1984}}.
\end{enumerate}
\end{fact}

Item (c) already shows a pattern that will recur: existence of \emph{some} solution costs $\WKL$, while
existence of a solution that is \emph{extremal} among all solutions (a selection) costs $\ACA$.

\subsection{Convexity collapses the cost}\label{subsec:convex-existence}

For convex functions the situation changes completely. The minimizers of a convex function form a convex
set, and convex sets are much easier to hit than arbitrary closed sets.

\begin{theorem}\label{thm:convex-rca}
\leavevmode
\begin{enumerate}[nosep,label=\textup{(\alph*)}]
  \item $\RCA$ proves that every convex continuous function $f\colon[0,1]\to\R$ attains its minimum.
  \item For each standard $n\ge1$, $\RCA$ proves that every convex function $f\colon[0,1]^n\to\R$ with a modulus
  of uniform continuity attains its minimum.
\end{enumerate}
\end{theorem}

Here ``for each standard $n$'' means that there is a separate proof for each concrete number $n=1,2,3,\dots$; the
statement with $n$ as a variable is \cref{prob:uniform-n}. Compare with \cref{fact:evt}(a): in dimension one,
convexity drops the logical cost from $\WKL$ to $\RCA$. In dimension $n\ge2$ the modulus in (b) is a genuine
hypothesis: for general continuous functions its existence is equivalent to $\WKL$, and whether convexity alone
provides it is part of \cref{prob:uniform-n}. What (b) shows is that, once a modulus is available, convexity removes
every other use of compactness. Friedman remarked informally that maximum principles become provable in $\RCA$ under
``geometric'' hypotheses of this kind \cite{Friedman2009FOMConstructiveAnalysis}; we did not find a published proof.
A sibling result is that the mean value theorem holds in $\RCA$ \cite{HardinVelleman2001MVT}.

\begin{proof}
(a) \emph{A modulus.} Let $f$ be convex and continuous on $[0,1]$. Convexity gives $f\le M_+\defeq
\max(f(0),f(1))$ and $f(x)\ge2f(\frac12)-f(1-x)\ge2f(\frac12)-M_+$, so we can fix a rational
$M\ge\max(1,\,2(M_+-f(\frac12)))$, which bounds the oscillation of $f$. By the three-chord inequality, $f$ is
$(M/\delta)$-Lipschitz on $[\delta,1-\delta]$. The code of $f$ (in the sense of \cite[II.6]{Simpson2009SOSOA})
contains, for every $\eps$, a neighbourhood condition witnessing continuity at $0$; searching for it gives a
radius $r_0(\eps)$ with $\abs{f(x)-f(0)}<\eps$ for $x\in[0,r_0(\eps)]$, and similarly $r_1(\eps)$ at $1$. Given
$\eps$, put $\delta=\min(\frac12,r_0(\eps/2),r_1(\eps/2))$ and $\eta=\min(\delta/2,\eps\delta/(2M))$, and let
$\abs{x-y}<\eta$. If $\min(x,y)<\delta/2$, both points lie in $[0,\delta]$ and $\abs{f(x)-f(y)}<\eps$ by
continuity at $0$; the case $\max(x,y)>1-\delta/2$ is symmetric; otherwise both points lie in
$[\delta/2,1-\delta/2]$, where $f$ is $(2M/\delta)$-Lipschitz, and again $\abs{f(x)-f(y)}<\eps$. So $f$ has a
modulus of uniform continuity, and $m=\inf f$ exists.

\emph{A minimizer.} We argue by cases; the case distinction is classical logic, not comprehension.
If $f(q)=m$ for some rational $q$, we are done. Otherwise $f(q)>m$ for every rational $q$. For rational $q$
consider the $\Sigma^0_1$ statements
\[
  R(q):\ \exists r\in\Q\cap(q,1]\; f(r)<f(q),\qquad
  \Lambda(q):\ \exists r\in\Q\cap[0,q)\; f(r)<f(q).
\]
At least one holds, because $f(q)>m=\inf_{r\in\Q}f(r)$. They cannot both hold, because $r_1<q<r_2$ with
$f(r_1),f(r_2)<f(q)$ contradicts convexity. So $\{q:R(q)\}$ exists by $\Delta^0_1$ comprehension, and bisection
($l_0=0$, $u_0=1$; replace $l$ by the midpoint $c$ if $R(c)$, otherwise replace $u$ by $c$) gives nested
intervals with $R(l_k)$ and $\Lambda(u_k)$; note that $R(0)$ and $\Lambda(1)$ hold. Let $x$ be the common limit.
If $f(x)>m$, pick a rational $r$ with $f(r)<f(x)$, say $r>x$. For large $k$ we have $u_k<r$, and $\Lambda(u_k)$
gives $r'<u_k$ with $f(r')<f(u_k)$; convexity on $[r',r]$ gives $f(u_k)\le\max(f(r'),f(r))$, hence
$f(u_k)\le f(r)$, and in the limit $f(x)\le f(r)<f(x)$, a contradiction. The case $r<x$ is symmetric.

(b) By induction on the standard number $n$. Write points of $[0,1]^n$ as $(t,y)$ with $t\in[0,1]$. The function
$\varphi(t)=\inf_{y\in[0,1]^{n-1}}f(t,y)$ exists in $\RCA$ (it is computed from the modulus $\omega$ of $f$ by
finite grids), has modulus $\eps\mapsto\omega(\eps/2)$, and is convex, because partial minimization preserves
convexity. By (a), $\varphi$ attains its minimum at some $t^\ast$, and $\varphi(t^\ast)=\inf f$. The function
$f(t^\ast,\cdot)$ is convex on $[0,1]^{n-1}$ with modulus $\omega$, so by the induction hypothesis it attains its
minimum at some $y^\ast$, and $f(t^\ast,y^\ast)=\varphi(t^\ast)=\inf f$.
\end{proof}

The proof of (a) is the classical proof that the intermediate value theorem holds in $\RCA$
\cite[II.6.6]{Simpson2009SOSOA}, transplanted from sign changes to slopes. It is non-uniform in an essential way:
whether some rational is a minimizer cannot be decided from $f$. The uniform content is measured by Weihrauch
reducibility, and here the answer can be read off from Neumann's work on fixed points of nonexpansive maps.

\begin{proposition}\label{prop:cmin-weihrauch}
Let $\CMin_n$ be the problem of finding a minimizer of a convex $f\in C([0,1]^n)$. Then $\CMin_n\seqv\XC_n$
for every $n\ge1$; in particular $\CMin_1\seqv\CC_{[0,1]}\seqv\IVT$. Consequently the problems $\CMin_n$ form a
strictly increasing chain below $\WKLp$, and every computable convex function on $[0,1]^n$ has a computable
minimizer.
\end{proposition}

\begin{proof}
($\CMin_n\slev\XC_n$.) From $f$ one computes $m=\min f$, and $\argmin f=\{x:f(x)\le m\}$ is co-c.e.\ closed,
uniformly: its complement is the union of the rational boxes $B$ with $\min_{\bar B}f>m$, which can be
enumerated. It is nonempty and convex.

($\XC_n\slev\CMin_n$.) This direction is implicit in Neumann's proof that convex choice reduces to the
Browder--G\"ohde--Kirk fixed point problem \cite[Theorem 5.1]{Neumann2015LMCS}: his map
$g=\sum_k2^{-k-1}P_{h_k}$, a weighted average of projections onto half-spaces with intersection $A$, equals
$I-\nabla\Phi$ for the convex $1$-smooth function $\Phi=\sum_k2^{-k-1}\frac12\dist(\cdot,h_k)^2$, whose minimizers
are exactly the points of $A$. For completeness we give a direct construction. Let $A\subseteq[0,1]^n$ be
nonempty, closed and convex, given by an enumeration $U_0,U_1,\dots$ of rational open boxes with union
$[0,1]^n\setminus A$. The set $K_s=[0,1]^n\setminus(U_0\cup\dots\cup U_s)$ is a finite union of closed, possibly
degenerate, rational boxes (cut every axis at all box end points), so $P_s=\conv K_s$ is the convex hull of
finitely many rational points. The $P_s$ decrease and contain $A$. They also shrink to $A$: given $\delta>0$,
compactness gives $s$ with $K_s\subseteq A_\delta\defeq\{x:\dist(x,A)\le\delta\}$, and since $A_\delta$ is
convex, $P_s\subseteq A_\delta$. Let
\[
  f(x)=\sum_{s\ge0}2^{-s-1}\dist(x,P_s).
\]
Each summand is convex and $1$-Lipschitz, and the distance from a rational point to a rational polytope is
computable exactly (it solves a convex quadratic program with rational data), so $f$ is computable, uniformly in
the enumeration. Moreover $f\ge0$ and $f(x)=0$ iff $x\in\bigcap_sP_s=A$, so every minimizer of $f$ lies in $A$.

The remaining statements are known facts about convex choice: $\XC_1=\CC_{[0,1]}\seqv\IVT$
\cite[Theorem 6.2]{BrattkaGherardi2011BSL}, \cite[Theorem 7.34]{BrattkaGherardiPauly2021};
$\XC_n<_{\mathrm W}\XC_{n+1}$ \cite{LeRouxPauly2015LMCS}; and every nonempty co-c.e.\ closed convex subset of
$\R^n$ contains a computable point \cite[Theorem 5.2]{LeRouxZiegler2008}. For a computable convex $f$ on
$[0,1]^n$, the last statement also follows from \cref{thm:convex-rca}(b): such an $f$ has a computable modulus of
uniform continuity, so (b) applies in the $\omega$-model of computable sets, whose reals are the computable reals.
\end{proof}

The first-order optimality condition behaves in the same way. We record it here, although it is the computable
counterpart of the problem studied in \cref{subsec:cls}.

\input{feasible_kkt}

\subsection{Tameness collapses the cost too}\label{subsec:tame}

A second structural assumption makes compactness unnecessary for a completely different reason. Polynomial and
semialgebraic optimization problems of fixed format are statements of first-order real algebra, and Tarski's
theorem turns them into consequences of finitely many algebraic axioms, each of which $\RCA$ can verify.

\begin{proposition}[Tarski transfer; folklore]\label{prop:tarski}
Let $\theta$ be a sentence in the first-order language of ordered rings that is true in $\R$. Then $\RCA$
proves $\theta$, with its quantifiers interpreted over the coded real numbers. In particular, for each standard
$n$ and $d$, $\RCA$ proves:
\begin{enumerate}[nosep,label=\textup{(\alph*)}]
\item every polynomial of degree at most $d$ in $n$ variables attains its minimum on $[0,1]^n$, and, for each
standard $k$, on every nonempty bounded set defined by at most $k$ non-strict polynomial inequalities of degree at
most $d$;
\item linear programming duality, and von Neumann's minimax theorem, for real data of size $m\times n$, for each
standard $m$;
\item every finite game with at most $n$ players and $n$ pure strategies each has a mixed Nash equilibrium.
\end{enumerate}
\end{proposition}

\begin{proof}
The theory $\mathrm{RCF}$ of real closed fields is complete \cite{Tarski1951}, so $\mathrm{RCF}\vdash\theta$.
A formal derivation uses finitely many axioms of $\mathrm{RCF}$: the ordered field axioms, the existence of square
roots of non-negative elements, and the existence of roots of polynomials of finitely many odd degrees. $\RCA$
proves each of these for its real numbers (the last two by the intermediate value theorem, which holds in $\RCA$
\cite[II.6.6]{Simpson2009SOSOA}). Equality of reals is a congruence for $+$, $\times$ and $<$ provably in $\RCA$,
so the derivation can be replayed in $\RCA$ with first-order quantifiers read as quantifiers over codes of reals.
Statements (a)--(c), for fixed sizes, are first-order sentences true in $\R$.
\end{proof}

The proposition is a meta-theorem: it gives one proof for each format, and says nothing about the statements
with $n$ and $d$ as variables, which are not first-order sentences. For linear programming we prove the uniform
statement in \cref{thm:lp-rca}; for polynomials and games the uniform question is open
(\cref{prob:uniform-n}). The fact behind the proposition, that the reals of $\RCA$ form a real closed field, is
standard; we record the optimization corollaries because they show that tameness, like convexity, replaces a
compactness argument, here by a finite algebraic one.

\subsection{Uniqueness}\label{subsec:uniqueness}

Uniqueness makes solutions computable. A unique point of a co-c.e.\ closed subset of a computably compact space is
computable, uniformly in the set \cite[Corollary 8.9]{BrattkaGherardi2011BSL}; so a continuous function on
$[0,1]^n$ with a unique minimizer has a computable minimizer, uniformly. In reverse mathematics the situation is
more delicate: $\WKL$ proves that a function with at most one zero has a modulus of uniqueness, and already for
Lipschitz functions on $[0,1]$ with exactly one zero the \emph{uniform} uniqueness statement implies $\WKL$
\cite[Theorem 4.1]{Kohlenbach2019Moduli}. In Bishop's constructive mathematics, the existence of minima of
uniformly continuous functions with at most one minimum point is equivalent to the fan theorem
\cite{BergerIshihara2005,BergerBridgesSchuster2006}, and for quasi-convex functions it is provable outright
\cite{BergerSvindland2019UniqueMin}. Uniqueness is also the classical source of explicit rates, through
Kohlenbach's moduli of uniqueness \cite{Kohlenbach1993Chebycheff}; we return to this in
\cref{subsec:regularity,subsec:approx}.

\subsection{Beyond compact spaces and continuous functions}\label{subsec:beyond}

Optimization in infinite dimensions, with lower semicontinuous objectives or with constraints given only by
negative information, climbs the hierarchy quickly.

\begin{fact}\label{fact:beyond}
Over $\RCA$:
\begin{enumerate}[nosep,label=\textup{(\alph*)}]
\item \emph{Lower semicontinuity.} ``Every lower semicontinuous $f\colon[0,1]\to[0,\infty)$ attains its
minimum'' is equivalent to $\ACA$, for lower semicontinuous functions coded by labelled rational balls as in
\cite{FernandezDuqueShaferYokoyama2020} (combine Theorem 8.2, Proposition 9.3 and Lemma 7.2 there); the calibration
depends on this coding.
\item \emph{Projections.} The existence of the orthogonal projection onto every closed subspace (the closure of
the span of a sequence) of a separable Hilbert space is equivalent to $\ACA$; the existence of the distance
$d(x,M)$ is equivalent to the existence of the projection $P_Mx$, provably in $\RCA$
\cite[Theorems 12.3 and 12.5]{AvigadSimic2006}. The existence of the norm of every bounded linear functional,
which is the optimal value $\sup_{\norm x\le1}\abs{f(x)}$, and the Riesz representation theorem are each
equivalent to $\ACA$ \cite[Theorem 13.4]{AvigadSimic2006}.
\item \emph{Ekeland's variational principle} \cite{Ekeland1974}. For a lower semicontinuous potential $f$ on a
complete separable metric space, the principle has a weak (``free'') form, asserting $\eps$-critical points, and
a strong (``localized'') form, asserting them below a given point. Fern\'andez-Duque, Shafer and Yokoyama
\cite[Section 11]{FernandezDuqueShaferYokoyama2020} prove: the free form for continuous $f$ on compact spaces is
equivalent to $\WKL$; weakening the localized form in exactly two of the three ways (free, compact space,
continuous $f$), or restricting it to compact spaces alone, gives $\ACA$; and the free form, the localized form, and even the localized form for continuous
functions are equivalent to $\PiCA$.
\item \emph{Caristi's fixed point theorem}, a close relative of Ekeland's principle, is equivalent to $\WKL$ or
$\ACA$ in restricted forms, and for Baire or Borel maps to the transfinite leftmost path principle $\mathsf{TLPP}_0$,
which lies strictly between $\ATR$ and $\PiCA$ \cite{FernandezDuqueShaferTowsnerYokoyama2023,Towsner2013,PengYamazaki2017}.
\item \emph{Games.} $\ACA$ proves that every continuous game on compact spaces has a mixed Nash equilibrium, and
weak compactness of probability measures on compact spaces is equivalent to $\ACA$
\cite{PengPengYamazaki2023}.
\end{enumerate}
\end{fact}

Item (c) is the most striking calibration in the area. The localized Ekeland principle for \emph{continuous}
functions is, in the authors' words, the first statement about continuous functions stemming from analysis that is
equivalent to $\PiCA$. Since Ekeland's principle is the engine of much of modern variational analysis (existence of
approximate minimizers with sharp optimality conditions, subdifferential calculus, the Bishop--Phelps theorem), its
strength is a measure of how far variational analysis is from the predicative mathematics of $\ACA$. Item (b)
shows a phenomenon that we meet again in \cref{thm:B}: for strictly convex problems, the optimal \emph{value}
determines the optimal \emph{point} effectively.

\subsection{The constructive picture}\label{subsec:constructive}

Bishop-style constructive mathematics measures the same theorems by intuitionistic logic and omniscience
principles, and its results run parallel to the ones above. That every uniformly continuous positive function on
$[0,1]$ has a positive infimum is a well-known equivalent of a form of Brouwer's fan theorem (it fails in recursive
mathematics \cite{JulianRichman1984}; see \cite{BergerSvindland2018Fan} and its references); for quasi-convex
functions on compact convex subsets of $\R^n$ this is provable without the fan theorem
\cite{BergerSvindland2016Infima}, and convexity yields a ``convex fan theorem'' (co-convex bars are uniform)
\cite{BergerSvindland2018Fan}. A separating hyperplane theorem for convex sets and the fundamental theorem of asset
pricing are each equivalent to Markov's principle \cite{BergerSvindland2016FTAP}, and Farkas' lemma as an exclusive
alternative is equivalent to $\LPO$, although enough of it survives to give constructive versions of linear
programming optimality criteria and of the minimax theorem \cite{BergerSvindland2022Farkas}. The common moral is
principle P1 of the introduction: convexity does the work that compactness, or omniscience, does in general.