\documentclass[11pt,letterpaper]{article}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}

\usepackage{amsmath,amssymb,amsthm,mathtools}
\usepackage{newpxtext}                 % Palatino text
\usepackage{newpxmath}                 % Palatino math
\usepackage[scaled=0.90]{FiraSans}     % headings, labels, title block
\renewcommand{\familydefault}{\rmdefault}
\linespread{1.06}
\usepackage[letterspace=80]{microtype}

\usepackage[letterpaper,left=1.15in,right=1.15in,top=1.1in,bottom=1.15in,headsep=0.32in,footskip=0.45in]{geometry}
\setlength{\parindent}{1.1em}
\setlength{\parskip}{0pt}

\usepackage{xcolor}
\definecolor{ink}{HTML}{1A1F2B}
\definecolor{navy}{HTML}{1F3A63}         % headings, labels
\definecolor{refcool}{HTML}{2C5AA0}      % cross-references, numbers, theorem bars
\definecolor{citewarm}{HTML}{B5403B}     % citations, subtitle, definition bars
\definecolor{muted}{HTML}{6B6A66}        % running heads, meta text
\definecolor{rulegray}{HTML}{D3D6DC}
\definecolor{thmback}{HTML}{F2F6FC}
\definecolor{lemback}{HTML}{F5F6F8}
\definecolor{lembar}{HTML}{6B7A90}
\definecolor{absback}{HTML}{F7F8FA}


\usepackage{graphicx,booktabs,array,tabularx,multicol}
\setlength{\emergencystretch}{2em}
\usepackage{enumitem}
\setlist{itemsep=1pt,parsep=0pt,topsep=3pt,partopsep=0pt}
\usepackage[font=small,labelfont={sf,bf,color=navy},labelsep=period,skip=6pt]{caption}
\usepackage[numbers,square,sort&compress]{natbib}
\renewcommand{\bibfont}{\small}
\setlength{\bibsep}{3pt plus 1pt}
\renewcommand{\bibsection}{\section*{References}\addcontentsline{toc}{section}{References}}
\usepackage[most]{tcolorbox}
\usepackage{titlesec,titletoc}
\usepackage{fancyhdr}
\usepackage{tikz}
\usetikzlibrary{positioning,arrows.meta,calc,fit,backgrounds}

\titleformat{\section}{\sffamily\Large\bfseries\color{navy}}{\textcolor{refcool}{\thesection}}{0.7em}{}
\titlespacing*{\section}{0pt}{3.2ex plus 1ex minus .2ex}{1.5ex plus .2ex}
\titleformat{\subsection}{\sffamily\large\bfseries\color{navy}}{\textcolor{refcool}{\thesubsection}}{0.6em}{}
\titlespacing*{\subsection}{0pt}{2.4ex plus .8ex minus .2ex}{1.0ex plus .2ex}
\titleformat{\subsubsection}{\sffamily\normalsize\bfseries\color{navy}}{\textcolor{refcool}{\thesubsubsection}}{0.5em}{}
\titleformat{\paragraph}[runin]{\sffamily\bfseries\color{navy}}{}{0pt}{}
\titlespacing*{\paragraph}{0pt}{1.4ex plus .5ex minus .2ex}{0.55em}

\setcounter{tocdepth}{1}
\titlecontents{section}[2.0em]{\addvspace{0.6pt}\sffamily\fontsize{8.4}{10.2}\selectfont}
  {\contentslabel[\textcolor{refcool}{\bfseries\thecontentslabel}]{2.0em}}{\hspace*{-2.0em}}
  {\titlerule*[0.6pc]{\textcolor{rulegray}{.}}\contentspage}

\pagestyle{fancy}
\fancyhf{}
\fancyhead[L]{\sffamily\footnotesize\color{muted}The Logical Anatomy of Optimization}
\fancyhead[R]{\sffamily\footnotesize\color{muted}\thepage}
\renewcommand{\headrule}{{\color{rulegray}\hrule height 0.5pt}}
\fancypagestyle{first}{\fancyhf{}\renewcommand{\headrule}{}\fancyfoot[C]{\sffamily\footnotesize\color{muted}\thepage}}

\newtheoremstyle{boxed}{0pt}{0pt}{\itshape}{}{\sffamily\bfseries\color{navy}}{.}{0.5em}
  {\thmname{#1}\thmnumber{ #2}\thmnote{\ \textmd{(#3)}}}
\newtheoremstyle{boxedrm}{0pt}{0pt}{\normalfont}{}{\sffamily\bfseries\color{navy}}{.}{0.5em}
  {\thmname{#1}\thmnumber{ #2}\thmnote{\ \textmd{(#3)}}}
\theoremstyle{boxed}
\newtheorem{theorem}{Theorem}[section]
\newtheorem{proposition}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}
\newtheorem{claim}[theorem]{Claim}
\newtheorem{conjecture}[theorem]{Conjecture}
\newtheorem{fact}[theorem]{Fact}
\newtheorem{observation}[theorem]{Observation}
\theoremstyle{boxedrm}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{assumption}[theorem]{Assumption}
\newtheorem{remark}[theorem]{Remark}
\newtheorem{example}[theorem]{Example}
\newtheorem{problem}[theorem]{Problem}
\newtheorem{question}[theorem]{Question}
\tcbset{thmbox/.style={enhanced,breakable,frame hidden,sharp corners,boxrule=0pt,
  left=8pt,right=8pt,top=5pt,bottom=5pt,before skip=9pt,after skip=9pt}}
\tcbset{coolbox/.style={thmbox,colback=thmback,borderline west={2.4pt}{0pt}{refcool}}}
\tcbset{slatebox/.style={thmbox,colback=lemback,borderline west={2.4pt}{0pt}{lembar}}}
\tcbset{warmbox/.style={thmbox,colback=white,borderline west={2.4pt}{0pt}{citewarm}}}
\tcbset{linebox/.style={blanker,breakable,left=8pt,before skip=7pt,after skip=7pt,borderline west={1pt}{0pt}{rulegray}}}
\tcolorboxenvironment{theorem}{coolbox}
\tcolorboxenvironment{proposition}{coolbox}
\tcolorboxenvironment{corollary}{coolbox}
\tcolorboxenvironment{conjecture}{coolbox}
\tcolorboxenvironment{lemma}{slatebox}
\tcolorboxenvironment{claim}{slatebox}
\tcolorboxenvironment{fact}{slatebox}
\tcolorboxenvironment{observation}{slatebox}
\tcolorboxenvironment{definition}{warmbox}
\tcolorboxenvironment{assumption}{warmbox}
\tcolorboxenvironment{remark}{linebox}
\tcolorboxenvironment{example}{linebox}
\tcolorboxenvironment{problem}{linebox}
\tcolorboxenvironment{question}{linebox}


\makeatletter
\renewenvironment{proof}[1][\proofname]{\par\pushQED{\qed}\normalfont\topsep6\p@\@plus6\p@\relax
  \trivlist\item[\hskip\labelsep{\sffamily\bfseries\color{navy}#1.}]\ignorespaces}{\popQED\endtrivlist\@endpefalse}
\makeatother
\renewcommand{\qedsymbol}{\textcolor{refcool}{\small$\blacksquare$}}

\newcommand{\pflab}[2]{{\color{refcool}\ensuremath{\langle#1\rangle}#2}}
\newenvironment{steps}{\begin{list}{}{%
    \setlength{\leftmargin}{2.2em}\setlength{\labelwidth}{2.0em}\setlength{\labelsep}{0.2em}%
    \setlength{\itemsep}{2pt}\setlength{\parsep}{1pt}\setlength{\topsep}{2pt}\setlength{\partopsep}{0pt}%
    \renewcommand{\makelabel}[1]{##1\hfil}}}{\end{list}}
\newcommand{\step}[2]{\item[\pflab{#1}{#2}.]}
\newcommand{\qedstep}[2]{\item[\pflab{#1}{#2}.]{\sffamily\small\color{navy}Q.E.D.}}
\newcommand{\pf}{\par{\sffamily\small\color{muted}Proof:}\ }
\newcommand{\sref}[2]{\pflab{#1}{#2}}
\newcommand{\xsref}[2]{\pflab{#1}{#2}}
\providecommand{\Assume}{{\sffamily\small\color{navy}Assume:}\ }
\providecommand{\Prove}{{\sffamily\small\color{navy}Prove:}\ }
\providecommand{\Let}{{\sffamily\small\color{navy}Let:}\ }
\providecommand{\Suffices}{{\sffamily\small\color{navy}Suffices:}\ }
\providecommand{\Case}{{\sffamily\small\color{navy}Case:}\ }
\newcommand{\pfsketch}{\par{\sffamily\small\color{muted}Proof sketch:}\ }
\providecommand{\markmainend}{}

\makeatletter
\newcommand{\RCA}{\mathsf{RCA}_0}
\newcommand{\WKL}{\mathsf{WKL}_0}
\newcommand{\ACA}{\mathsf{ACA}_0}
\newcommand{\ATR}{\mathsf{ATR}_0}
\newcommand{\PiCA}{\Pi^1_1\text{-}\mathsf{CA}_0}
\newcommand{\BISH}{\mathsf{BISH}}
\newcommand{\FAN}{\mathsf{FAN}}
\newcommand{\Tot}{T^1_2}
\newcommand{\lev}{\leq_{\mathrm{W}}}
\newcommand{\slev}{\leq_{\mathrm{sW}}}
\newcommand{\eqv}{\equiv_{\mathrm{W}}}
\newcommand{\seqv}{\equiv_{\mathrm{sW}}}
\newcommand{\pr}[1]{\mathsf{#1}}
\newcommand{\LPO}{\pr{LPO}}
\newcommand{\LLPO}{\pr{LLPO}}
\newcommand{\lm}{\pr{lim}}
\newcommand{\WKLp}{\pr{WKL}}
\newcommand{\IVT}{\pr{IVT}}
\newcommand{\MCT}{\pr{MCT}}
\newcommand{\CC}{\pr{CC}}
\newcommand{\XC}{\pr{XC}}
\newcommand{\Cch}{\pr{C}}
\newcommand{\CMin}{\pr{CMin}}
\newcommand{\GDL}{\pr{GDLim}}
\newcommand{\BFT}{\pr{BFT}}
\newcommand{\KKT}{\pr{KKT}}
\newcommand{\R}{\mathbb{R}}
\newcommand{\Q}{\mathbb{Q}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\Hil}{\mathcal{H}}
\newcommand{\ip}[2]{\langle #1, #2\rangle}
\newcommand{\norm}[1]{\lVert #1\rVert}
\newcommand{\abs}[1]{\lvert #1\rvert}
\newcommand{\dist}{\operatorname{dist}}
\newcommand{\argmin}{\operatorname*{argmin}}
\newcommand{\conv}{\operatorname{conv}}
\newcommand{\prox}{\operatorname{prox}}
\newcommand{\diam}{\operatorname{diam}}
\newcommand{\lenpath}{\operatorname{len}}
\newcommand{\fl}{\operatorname{fl}}
\newcommand{\eps}{\varepsilon}
\newcommand{\iter}[2]{#1^{(#2)}}
\newcommand{\defeq}{\mathrel{:=}}
\newcommand{\Pos}{\mathsf{P}}
\newcommand{\PLS}{\mathsf{PLS}}
\newcommand{\PPAD}{\mathsf{PPAD}}
\newcommand{\CLS}{\mathsf{CLS}}
\newcommand{\TFNP}{\mathsf{TFNP}}
\newcommand{\NP}{\mathsf{NP}}
\newcommand{\PPA}{\mathsf{PPA}}
\newcommand{\PPADS}{\mathsf{PPADS}}
\makeatother

\usepackage[colorlinks=true,linkcolor=refcool,citecolor=citewarm,urlcolor=refcool,
  pdftitle={The Logical Anatomy of Optimization},pdfauthor={Xiaoyu Li},pdfsubject={Reverse Mathematics, Proof Mining, and the Price of Convergence},pdfkeywords={reverse mathematics, Weihrauch complexity, proof mining, convex optimization, gradient descent, metastability, duality, bounded arithmetic}]{hyperref}
\usepackage[capitalise,nameinlink]{cleveref}
\crefname{appendix}{Appendix}{Appendices}
\crefname{problem}{Open Problem}{Open Problems}
\crefname{fact}{Fact}{Facts}

\begin{document}
\thispagestyle{first}

\noindent{\color{refcool}\rule{\linewidth}{2.2pt}}\par\vspace{7pt}
\noindent{\sffamily\footnotesize\color{muted}\lsstyle PREPRINT\quad\textbullet\quad October 2026}\par\vspace{8pt}
\noindent{\sffamily\bfseries\fontsize{23}{28}\selectfont\color{navy}The Logical Anatomy of Optimization\par}\vspace{7pt}
\noindent{\sffamily\large\color{citewarm}Reverse Mathematics, Proof Mining, and the Price of Convergence\par}\vspace{12pt}
\noindent\begin{tabular*}{\linewidth}{@{}l@{}}
{\sffamily\bfseries\color{ink}Xiaoyu Li} \\[1pt]
{\small University of New South Wales} \\[1pt]
{\sffamily\footnotesize\href{mailto:xiaoyulics@gmail.com}{\color{muted}xiaoyulics@gmail.com}}
\end{tabular*}

\vspace{10pt}

\begin{tcolorbox}[enhanced,colback=absback,frame hidden,sharp corners,boxrule=0pt,
  borderline west={3pt}{0pt}{refcool},left=11pt,right=11pt,top=7pt,bottom=7pt]
{\sffamily\bfseries\footnotesize\color{navy}\lsstyle ABSTRACT}\par\vspace{3pt}
\small Optimization theory proves three kinds of theorems: that optimal points exist, that algorithms converge to them,
and that optimality can be certified by duality. We measure how much mathematics each kind needs, using reverse
mathematics, Weihrauch complexity and proof mining, and assemble the answers, old and new, into one map stated in
the language of optimization. Compactness makes existence cost weak K\H{o}nig's lemma, but convexity (and, format by
format, tameness) makes it cheap: we show that $\RCA$ proves that convex functions on $[0,1]$ attain their minima
(and on $[0,1]^n$, for each fixed $n$, given a modulus of uniform continuity), and that $\RCA$ proves linear
programming duality and the minimax theorem for real data of every size. Convergence costs more: it follows from
results of Kohlenbach and Neumann that convergence of gradient descent for convex smooth functions on $\R$ is
equivalent to $\ACA$. We explain this by a selection principle: what costs is the particular minimizer the algorithm
selects, and uniqueness or an error bound removes the cost. Below convergence lies finitary information. Gradient
descent in $\R^d$ has at most $2C_dD/\eps$ fluctuations of size $\eps$, with $C_d$ depending only on $d$, which yields
rates of metastability; no such bound is dimension-free, by the span-restriction argument behind performance
estimation; and the limits of gradient descent on computable instances have d.c.e.\ coordinates, a proper subclass of
the limit-computable reals. The map also covers Ekeland's variational principle (up to $\PiCA$), separation theorems,
K\H{o}nig duality ($\ATR$), proof-mined rates for fixed-point iterations, and the feasible world, where local search
captures the $\NP$ search problems provably total in $T^1_2$ and approximate stationary points of smooth functions are
complete for $\CLS=\PPAD\cap\PLS$. We close with five principles and open problems.\par
\vspace{4pt}{\sffamily\footnotesize\color{navy}\textbf{Keywords:}}\ {\footnotesize reverse mathematics, Weihrauch complexity, proof mining, convex optimization, gradient descent, metastability, duality, bounded arithmetic}
\end{tcolorbox}


\vspace{2pt}
\begin{tcolorbox}[enhanced,colback=white,colframe=rulegray,boxrule=0.5pt,arc=2pt,left=10pt,right=10pt,top=5pt,bottom=4pt]
{\sffamily\bfseries\footnotesize\color{navy}\lsstyle CONTENTS}\par
\setlength{\multicolsep}{4pt plus 1pt minus 1pt}\begin{multicols}{2}
{\hypersetup{linkcolor=ink}\makeatletter\@starttoc{toc}\makeatother}
\end{multicols}
\end{tcolorbox}
\suppressfloats[t]
\clearpage

\input{intro}
\input{prelim}
\input{existence}
\input{convergence}
\input{proofmining}
\input{duality}
\input{feasible}
\input{synthesis}

% Bibliography embedded from main.bbl (plainnat); compiles with pdflatex alone.
\begin{thebibliography}{171}
\providecommand{\natexlab}[1]{#1}
\providecommand{\url}[1]{\texttt{#1}}
\expandafter\ifx\csname urlstyle\endcsname\relax
  \providecommand{\doi}[1]{doi: #1}\else
  \providecommand{\doi}{doi: \begingroup \urlstyle{rm}\Url}\fi

\bibitem[Aharoni et~al.(1992)Aharoni, Magidor, and
  Shore]{AharoniMagidorShore1992}
Ron Aharoni, Menachem Magidor, and Richard~A. Shore.
\newblock On the strength of {K}{\"o}nig's duality theorem for infinite
  bipartite graphs.
\newblock \emph{Journal of Combinatorial Theory, Series B}, 54\penalty0
  (2):\penalty0 257--290, 1992.
\newblock \doi{10.1016/0095-8956(92)90057-5}.

\bibitem[Aharoni et~al.(2011)Aharoni, Berger, Georgakopoulos, Perlstein, and
  Spr{\"u}ssel]{AharoniBergerGeorgakopoulosPerlsteinSpruessel2011}
Ron Aharoni, Eli Berger, Agelos Georgakopoulos, Amitai Perlstein, and Philipp
  Spr{\"u}ssel.
\newblock The {M}ax-{F}low {M}in-{C}ut theorem for countable networks.
\newblock \emph{Journal of Combinatorial Theory, Series B}, 101\penalty0
  (1):\penalty0 1--17, 2011.
\newblock \doi{10.1016/j.jctb.2010.08.002}.

\bibitem[Ambos-Spies et~al.(2000)Ambos-Spies, Weihrauch, and
  Zheng]{AmbosSpiesWeihrauchZheng2000WeaklyComputable}
Klaus Ambos-Spies, Klaus Weihrauch, and Xizhong Zheng.
\newblock Weakly computable real numbers.
\newblock \emph{Journal of Complexity}, 16\penalty0 (4):\penalty0 676--690,
  2000.
\newblock \doi{10.1006/jcom.2000.0561}.

\bibitem[Attouch et~al.(2013)Attouch, Bolte, and
  Svaiter]{AttouchBolteSvaiter2013}
Hedy Attouch, J{\'e}r{\^o}me Bolte, and Benar~Fux Svaiter.
\newblock Convergence of descent methods for semi-algebraic and tame problems:
  proximal algorithms, forward--backward splitting, and regularized
  {G}auss--{S}eidel methods.
\newblock \emph{Mathematical Programming}, 137\penalty0 (1--2):\penalty0
  91--129, 2013.

\bibitem[Avigad and Rute(2015)]{AvigadRute2015}
Jeremy Avigad and Jason Rute.
\newblock Oscillation and the mean ergodic theorem for uniformly convex
  {B}anach spaces.
\newblock \emph{Ergodic Theory and Dynamical Systems}, 35\penalty0
  (4):\penalty0 1009--1027, 2015.
\newblock \doi{10.1017/etds.2013.90}.

\bibitem[Avigad and Simic(2006)]{AvigadSimic2006}
Jeremy Avigad and Ksenija Simic.
\newblock Fundamental notions of analysis in subsystems of second-order
  arithmetic.
\newblock \emph{Annals of Pure and Applied Logic}, 139\penalty0
  (1--3):\penalty0 138--184, 2006.
\newblock \doi{10.1016/j.apal.2005.03.004}.

\bibitem[Baillon and Bruck(1996)]{BaillonBruck1996}
Jean-Bernard Baillon and Ronald~E. Bruck.
\newblock The rate of asymptotic regularity is {$O(1/\sqrt{n})$}.
\newblock In \emph{Theory and Applications of Nonlinear Operators of Accretive
  and Monotone Type}, volume 178 of \emph{Lecture Notes in Pure and Applied
  Mathematics}, pages 51--81. Dekker, New York, 1996.

\bibitem[Barak and Steurer(2014)]{BS14}
Boaz Barak and David Steurer.
\newblock Sum-of-squares proofs and the quest toward optimal algorithms.
\newblock In \emph{Proceedings of the International Congress of Mathematicians
  (ICM 2014), Seoul}, 2014.

\bibitem[Bauschke et~al.(2004)Bauschke, Matou{\v{s}}kov{\'a}, and
  Reich]{BauschkeMatouskovaReich2004Projection}
Heinz~H. Bauschke, Eva Matou{\v{s}}kov{\'a}, and Simeon Reich.
\newblock Projection and proximal point methods: convergence results and
  counterexamples.
\newblock \emph{Nonlinear Analysis}, 56:\penalty0 715--738, 2004.
\newblock \doi{10.1016/j.na.2003.10.010}.
\newblock URL \url{https://www.math.utoronto.ca/almut/MAT1000/P1P2-2004.pdf}.

\bibitem[Beame et~al.(2018)Beame, Fleming, Impagliazzo, Kolokolova, Pankratov,
  Pitassi, and Robere]{BFIKPPR18}
Paul Beame, Noah Fleming, Russell Impagliazzo, Antonina Kolokolova, Denis
  Pankratov, Toniann Pitassi, and Robert Robere.
\newblock Stabbing planes.
\newblock In \emph{9th Innovations in Theoretical Computer Science Conference
  (ITCS 2018)}, volume~94 of \emph{Leibniz International Proceedings in
  Informatics (LIPIcs)}, pages 10:1--10:20, 2018.
\newblock \doi{10.4230/LIPIcs.ITCS.2018.10}.

\bibitem[Beckmann and Buss(2009)]{BB09}
Arnold Beckmann and Samuel~R. Buss.
\newblock Polynomial local search in the polynomial hierarchy and witnessing in
  fragments of bounded arithmetic.
\newblock \emph{Journal of Mathematical Logic}, 9\penalty0 (1):\penalty0
  103--138, 2009.
\newblock \doi{10.1142/S0219061309000847}.

\bibitem[Berger and Ishihara(2005)]{BergerIshihara2005}
Josef Berger and Hajime Ishihara.
\newblock Brouwer's fan theorem and unique existence in constructive analysis.
\newblock \emph{Mathematical Logic Quarterly}, 51\penalty0 (4):\penalty0
  360--364, 2005.
\newblock \doi{10.1002/malq.200410038}.

\bibitem[Berger and Svindland(2016{\natexlab{a}})]{BergerSvindland2016FTAP}
Josef Berger and Gregor Svindland.
\newblock A separating hyperplane theorem, the fundamental theorem of asset
  pricing, and {Markov's} principle.
\newblock \emph{Annals of Pure and Applied Logic}, 167\penalty0 (11):\penalty0
  1161--1170, 2016{\natexlab{a}}.
\newblock \doi{10.1016/j.apal.2016.05.003}.

\bibitem[Berger and Svindland(2016{\natexlab{b}})]{BergerSvindland2016Infima}
Josef Berger and Gregor Svindland.
\newblock Convexity and constructive infima.
\newblock \emph{Archive for Mathematical Logic}, 55\penalty0 (7--8):\penalty0
  873--881, 2016{\natexlab{b}}.
\newblock \doi{10.1007/s00153-016-0502-y}.

\bibitem[Berger and Svindland(2018)]{BergerSvindland2018Fan}
Josef Berger and Gregor Svindland.
\newblock Brouwer's fan theorem and convexity.
\newblock \emph{Journal of Symbolic Logic}, 83\penalty0 (4):\penalty0
  1363--1375, 2018.
\newblock \doi{10.1017/jsl.2018.49}.

\bibitem[Berger and Svindland(2019)]{BergerSvindland2019UniqueMin}
Josef Berger and Gregor Svindland.
\newblock Convexity and unique minimum points.
\newblock \emph{Archive for Mathematical Logic}, 58\penalty0 (1--2):\penalty0
  27--34, 2019.
\newblock \doi{10.1007/s00153-018-0619-2}.

\bibitem[Berger and Svindland(2022)]{BergerSvindland2022Farkas}
Josef Berger and Gregor Svindland.
\newblock On {Farkas'} lemma and related propositions in {BISH}.
\newblock \emph{Annals of Pure and Applied Logic}, 173\penalty0 (2):\penalty0
  103059, 2022.
\newblock \doi{10.1016/j.apal.2021.103059}.

\bibitem[Berger et~al.(2006)Berger, Bridges, and
  Schuster]{BergerBridgesSchuster2006}
Josef Berger, Douglas Bridges, and Peter Schuster.
\newblock The fan theorem and unique existence of maxima.
\newblock \emph{Journal of Symbolic Logic}, 71\penalty0 (2):\penalty0 713--720,
  2006.
\newblock \doi{10.2178/jsl/1146620167}.

\bibitem[Bland(1977)]{Bland1977}
Robert~G. Bland.
\newblock New finite pivoting rules for the simplex method.
\newblock \emph{Mathematics of Operations Research}, 2\penalty0 (2):\penalty0
  103--107, 1977.

\bibitem[B{\"o}hm and Daniilidis(2022)]{BohmDaniilidis2022Ubiquitous}
Axel B{\"o}hm and Aris Daniilidis.
\newblock Ubiquitous algorithms in convex optimization generate self-contracted
  sequences.
\newblock \emph{Journal of Convex Analysis}, 29:\penalty0 119--128, 2022.

\bibitem[Bolte et~al.(2007)Bolte, Daniilidis, and
  Lewis]{BolteDaniilidisLewis2007}
J{\'e}r{\^o}me Bolte, Aris Daniilidis, and Adrian Lewis.
\newblock The {{\L}}ojasiewicz inequality for nonsmooth subanalytic functions
  with applications to subgradient dynamical systems.
\newblock \emph{SIAM Journal on Optimization}, 17\penalty0 (4):\penalty0
  1205--1223, 2007.

\bibitem[Brattka(2016)]{Brattka2016Historical}
Vasco Brattka.
\newblock Computability and analysis, a historical approach.
\newblock In Arnold Beckmann, Laurent Bienvenu, and Nata{\v{s}}a Jonoska,
  editors, \emph{Pursuit of the Universal (CiE 2016)}, Lecture Notes in
  Computer Science, pages 45--57. Springer, 2016.
\newblock \doi{10.1007/978-3-319-40189-8_5}.

\bibitem[Brattka and Gherardi(2011{\natexlab{a}})]{BrattkaGherardi2011BSL}
Vasco Brattka and Guido Gherardi.
\newblock Effective choice and boundedness principles in computable analysis.
\newblock \emph{The Bulletin of Symbolic Logic}, 17\penalty0 (1):\penalty0
  73--117, 2011{\natexlab{a}}.
\newblock \doi{10.2178/bsl/1294186663}.

\bibitem[Brattka and Gherardi(2011{\natexlab{b}})]{BrattkaGherardi2011JSL}
Vasco Brattka and Guido Gherardi.
\newblock Weihrauch degrees, omniscience principles and weak computability.
\newblock \emph{The Journal of Symbolic Logic}, 76\penalty0 (1):\penalty0
  143--176, 2011{\natexlab{b}}.
\newblock \doi{10.2178/jsl/1294170993}.

\bibitem[Brattka et~al.(2008)Brattka, Hertling, and
  Weihrauch]{BrattkaHertlingWeihrauch2008}
Vasco Brattka, Peter Hertling, and Klaus Weihrauch.
\newblock A tutorial on computable analysis.
\newblock In S.~Barry Cooper, Benedikt L{\"o}we, and Andrea Sorbi, editors,
  \emph{New Computational Paradigms: Changing Conceptions of What is
  Computable}, pages 425--491. Springer, 2008.

\bibitem[Brattka et~al.(2012{\natexlab{a}})Brattka, de~Brecht, and
  Pauly]{BrattkadeBrechtPauly2012}
Vasco Brattka, Matthew de~Brecht, and Arno Pauly.
\newblock Closed choice and a uniform low basis theorem.
\newblock \emph{Annals of Pure and Applied Logic}, 163\penalty0 (8):\penalty0
  986--1008, 2012{\natexlab{a}}.
\newblock \doi{10.1016/j.apal.2011.12.020}.

\bibitem[Brattka et~al.(2012{\natexlab{b}})Brattka, Gherardi, and
  Marcone]{BrattkaGherardiMarcone2012}
Vasco Brattka, Guido Gherardi, and Alberto Marcone.
\newblock The {B}olzano--{W}eierstrass theorem is the jump of weak
  {K}{\H{o}}nig's lemma.
\newblock \emph{Annals of Pure and Applied Logic}, 163\penalty0 (6):\penalty0
  623--655, 2012{\natexlab{b}}.
\newblock \doi{10.1016/j.apal.2011.10.006}.

\bibitem[Brattka et~al.(2019)Brattka, Le~Roux, Miller, and
  Pauly]{BrattkaLeRouxMillerPauly2019}
Vasco Brattka, St{\'e}phane Le~Roux, Joseph~S. Miller, and Arno Pauly.
\newblock Connected choice and the {Brouwer} fixed point theorem.
\newblock \emph{Journal of Mathematical Logic}, 19\penalty0 (1):\penalty0
  1950004, 2019.
\newblock \doi{10.1142/S0219061319500041}.

\bibitem[Brattka et~al.(2021)Brattka, Gherardi, and
  Pauly]{BrattkaGherardiPauly2021}
Vasco Brattka, Guido Gherardi, and Arno Pauly.
\newblock Weihrauch complexity in computable analysis.
\newblock In \emph{Handbook of Computability and Complexity in Analysis},
  Theory and Applications of Computability, pages 367--417. Springer, 2021.
\newblock \doi{10.1007/978-3-030-59234-9_11}.

\bibitem[Bravo and Cominetti(2018)]{BravoCominetti2018}
Mario Bravo and Roberto Cominetti.
\newblock Sharp convergence rates for averaged nonexpansive maps.
\newblock \emph{Israel Journal of Mathematics}, 227\penalty0 (1):\penalty0
  163--188, 2018.
\newblock \doi{10.1007/s11856-018-1723-z}.

\bibitem[Brown and Simpson(1986)]{BrownSimpson1986}
Douglas~K. Brown and Stephen~G. Simpson.
\newblock Which set existence axioms are needed to prove the separable
  {Hahn-Banach} theorem?
\newblock \emph{Annals of Pure and Applied Logic}, 31:\penalty0 123--144, 1986.
\newblock \doi{10.1016/0168-0072(86)90066-7}.

\bibitem[Buss and Kraj{\'\i}{\v{c}}ek(1994)]{BK94}
Samuel~R. Buss and Jan Kraj{\'\i}{\v{c}}ek.
\newblock An application of {B}oolean complexity to separation problems in
  bounded arithmetic.
\newblock \emph{Proceedings of the London Mathematical Society}, s3-69\penalty0
  (1):\penalty0 1--21, 1994.
\newblock \doi{10.1112/plms/s3-69.1.1}.

\bibitem[Buss et~al.(2014)Buss, Ko{\l}odziejczyk, and Thapen]{BKT14}
Samuel~R. Buss, Leszek~Aleksander Ko{\l}odziejczyk, and Neil Thapen.
\newblock Fragments of approximate counting.
\newblock \emph{The Journal of Symbolic Logic}, 79\penalty0 (2):\penalty0
  496--525, 2014.
\newblock \doi{10.1017/jsl.2013.37}.

\bibitem[Cenzer and Remmel(2005)]{CenzerRemmel2005}
Douglas Cenzer and Jeffrey~B. Remmel.
\newblock Proof-theoretic strength of the stable marriage theorem and other
  problems.
\newblock In Stephen~G. Simpson, editor, \emph{Reverse Mathematics 2001},
  volume~21 of \emph{Lecture Notes in Logic}, pages 67--103. Association for
  Symbolic Logic / Cambridge University Press, 2005.
\newblock \doi{10.1017/9781316755846.005}.

\bibitem[Chen et~al.(2009)Chen, Deng, and Teng]{CDT09}
Xi~Chen, Xiaotie Deng, and Shang-Hua Teng.
\newblock Settling the complexity of computing two-player {N}ash equilibria.
\newblock \emph{Journal of the ACM}, 56\penalty0 (3):\penalty0 1--57, 2009.
\newblock \doi{10.1145/1516512.1516516}.

\bibitem[Cheval and Leu{\c{s}}tean(2024)]{ChevalLeustean2024MathComp}
Hora{\c{t}}iu Cheval and Lauren{\c{t}}iu Leu{\c{s}}tean.
\newblock Linear rates of asymptotic regularity for {H}alpern-type iterations.
\newblock \emph{Mathematics of Computation}, 2024.
\newblock \doi{10.1090/mcom/3991}.

\bibitem[Cheval et~al.(2023)Cheval, Kohlenbach, and
  Leu{\c{s}}tean]{ChevalKohlenbachLeustean2023}
Hora{\c{t}}iu Cheval, Ulrich Kohlenbach, and Lauren{\c{t}}iu Leu{\c{s}}tean.
\newblock On modified {H}alpern and {T}ikhonov-{M}ann iterations.
\newblock \emph{Journal of Optimization Theory and Applications}, 197\penalty0
  (1):\penalty0 233--251, 2023.
\newblock \doi{10.1007/s10957-023-02192-6}.

\bibitem[Chv{\'a}tal(1973)]{Chv73}
Va{\v{s}}ek Chv{\'a}tal.
\newblock {E}dmonds polytopes and a hierarchy of combinatorial problems.
\newblock \emph{Discrete Mathematics}, 4\penalty0 (4):\penalty0 305--337, 1973.
\newblock \doi{10.1016/0012-365X(73)90167-2}.

\bibitem[Clote and Hirst(1998)]{CloteHirst1998}
Peter~G. Clote and Jeffry~L. Hirst.
\newblock Reverse mathematics of some topics from algorithmic graph theory.
\newblock \emph{Fundamenta Mathematicae}, 157\penalty0 (1):\penalty0 1--13,
  1998.
\newblock \doi{10.4064/fm-157-1-1-13}.

\bibitem[Cominetti et~al.(2014)Cominetti, Soto, and
  Vaisman]{CominettiSotoVaisman2014}
Roberto Cominetti, Jos{\'e}~A. Soto, and Jos{\'e} Vaisman.
\newblock On the rate of convergence of {K}rasnosel'ski{\u\i}-{M}ann iterations
  and their connection with sums of {B}ernoullis.
\newblock \emph{Israel Journal of Mathematics}, 199\penalty0 (2):\penalty0
  757--772, 2014.
\newblock \doi{10.1007/s11856-013-0045-4}.

\bibitem[Contreras and Cominetti(2023)]{ContrerasCominetti2023}
Juan~Pablo Contreras and Roberto Cominetti.
\newblock Optimal error bounds for non-expansive fixed-point iterations in
  normed spaces.
\newblock \emph{Mathematical Programming}, 199\penalty0 (1-2):\penalty0
  343--374, 2023.
\newblock \doi{10.1007/s10107-022-01830-7}.

\bibitem[Cook and Nguyen(2010)]{CN10}
Stephen Cook and Phuong Nguyen.
\newblock \emph{Logical Foundations of Proof Complexity}.
\newblock Cambridge University Press, 2010.
\newblock ISBN 9780521517294.
\newblock \doi{10.1017/CBO9780511676277}.

\bibitem[Cook et~al.(1987)Cook, Coullard, and Tur{\'a}n]{CCT87}
William~J. Cook, Collette~R. Coullard, and Gy{\"o}rgy Tur{\'a}n.
\newblock On the complexity of cutting-plane proofs.
\newblock \emph{Discrete Applied Mathematics}, 18\penalty0 (1):\penalty0
  25--38, 1987.
\newblock \doi{10.1016/0166-218X(87)90039-4}.

\bibitem[Dadush and Tiwari(2020)]{DT20}
Daniel Dadush and Samarth Tiwari.
\newblock On the complexity of branching proofs.
\newblock In \emph{35th Computational Complexity Conference (CCC 2020)}, volume
  169 of \emph{Leibniz International Proceedings in Informatics (LIPIcs)},
  pages 34:1--34:35, 2020.
\newblock \doi{10.4230/LIPIcs.CCC.2020.34}.

\bibitem[Daniilidis et~al.(2010)Daniilidis, Ley, and
  Sabourau]{DaniilidisLeySabourau2010}
Aris Daniilidis, Olivier Ley, and St{\'e}phane Sabourau.
\newblock Asymptotic behaviour of self-contracted planar curves and gradient
  orbits of convex functions.
\newblock \emph{Journal de Math{\'e}matiques Pures et Appliqu{\'e}es},
  94\penalty0 (2):\penalty0 183--199, 2010.
\newblock \doi{10.1016/j.matpur.2010.03.007}.

\bibitem[Daniilidis et~al.(2015)Daniilidis, David, Durand-Cartagena, and
  Lemenant]{DaniilidisDavidDurandCartagenaLemenant2015}
Aris Daniilidis, Guy David, Estibalitz Durand-Cartagena, and Antoine Lemenant.
\newblock Rectifiability of self-contracted curves in the {E}uclidean space and
  applications.
\newblock \emph{The Journal of Geometric Analysis}, 25\penalty0 (2):\penalty0
  1211--1239, 2015.
\newblock \doi{10.1007/s12220-013-9464-z}.

\bibitem[Daskalakis and Papadimitriou(2011)]{DP11}
Constantinos Daskalakis and Christos Papadimitriou.
\newblock Continuous local search.
\newblock In \emph{Proceedings of the Twenty-Second Annual ACM-SIAM Symposium
  on Discrete Algorithms (SODA 2011)}, pages 790--804, 2011.
\newblock \doi{10.1137/1.9781611973082.62}.

\bibitem[Daskalakis et~al.(2009)Daskalakis, Goldberg, and Papadimitriou]{DGP09}
Constantinos Daskalakis, Paul~W. Goldberg, and Christos~H. Papadimitriou.
\newblock The complexity of computing a {N}ash equilibrium.
\newblock \emph{SIAM Journal on Computing}, 39\penalty0 (1):\penalty0 195--259,
  2009.
\newblock \doi{10.1137/070699652}.

\bibitem[Daskalakis et~al.(2021)Daskalakis, Skoulakis, and Zampetakis]{DSZ21}
Constantinos Daskalakis, Stratis Skoulakis, and Manolis Zampetakis.
\newblock The complexity of constrained min-max optimization.
\newblock In \emph{Proceedings of the 53rd Annual ACM SIGACT Symposium on
  Theory of Computing (STOC 2021)}, pages 1466--1478, 2021.
\newblock \doi{10.1145/3406325.3451125}.

\bibitem[Dinis and Pinto(2021)]{DinisPinto2021JCA}
Bruno Dinis and Pedro Pinto.
\newblock Quantitative results on the multi-parameters proximal point
  algorithm.
\newblock \emph{Journal of Convex Analysis}, 28\penalty0 (3):\penalty0
  729--750, 2021.
\newblock \doi{10.68381/jca28041}.

\bibitem[Drori and Teboulle(2014)]{DroriTeboulle2014}
Yoel Drori and Marc Teboulle.
\newblock Performance of first-order methods for smooth convex minimization: a
  novel approach.
\newblock \emph{Mathematical Programming}, 145\penalty0 (1-2):\penalty0
  451--482, 2014.
\newblock \doi{10.1007/s10107-013-0653-0}.

\bibitem[Dzhafarov and Mummert(2022)]{DzhafarovMummert2022}
Damir~D. Dzhafarov and Carl Mummert.
\newblock \emph{Reverse Mathematics: Problems, Reductions, and Proofs}.
\newblock Theory and Applications of Computability. Springer, 2022.

\bibitem[Ekeland(1974)]{Ekeland1974}
Ivar Ekeland.
\newblock On the variational principle.
\newblock \emph{Journal of Mathematical Analysis and Applications}, 47\penalty0
  (2):\penalty0 324--353, 1974.

\bibitem[Fearnley et~al.(2021)Fearnley, Goldberg, Hollender, and
  Savani]{FGHS21}
John Fearnley, Paul~W. Goldberg, Alexandros Hollender, and Rahul Savani.
\newblock The complexity of gradient descent: {CLS} = {PPAD} $\cap$ {PLS}.
\newblock In \emph{Proceedings of the 53rd Annual ACM SIGACT Symposium on
  Theory of Computing (STOC 2021)}, pages 46--59, 2021.
\newblock \doi{10.1145/3406325.3451052}.

\bibitem[Fearnley et~al.(2024)Fearnley, Goldberg, Hollender, and
  Savani]{FGHS24}
John Fearnley, Paul~W. Goldberg, Alexandros Hollender, and Rahul Savani.
\newblock The complexity of computing {KKT} solutions of quadratic programs.
\newblock In \emph{Proceedings of the 56th Annual ACM Symposium on Theory of
  Computing (STOC 2024)}, pages 892--903, 2024.
\newblock \doi{10.1145/3618260.3649647}.

\bibitem[Fernandes and Ferreira(2002)]{FF02}
Ant{\'o}nio~M. Fernandes and Fernando Ferreira.
\newblock Groundwork for weak analysis.
\newblock \emph{The Journal of Symbolic Logic}, 67\penalty0 (2):\penalty0
  557--578, 2002.
\newblock \doi{10.2178/jsl/1190150098}.

\bibitem[Fern{\'a}ndez and Soltys(2013)]{FernandezSoltys2013}
Ariel~Germ{\'a}n Fern{\'a}ndez and Michael Soltys.
\newblock Feasible combinatorial matrix theory.
\newblock In Krishnendu Chatterjee and Ji{\v{r}}{\'\i} Sgall, editors,
  \emph{Mathematical Foundations of Computer Science 2013 (MFCS)}, Lecture
  Notes in Computer Science, pages 777--788. Springer, 2013.
\newblock \doi{10.1007/978-3-642-40313-2_68}.

\bibitem[Fern{\'a}ndez-Duque et~al.(2020)Fern{\'a}ndez-Duque, Shafer, and
  Yokoyama]{FernandezDuqueShaferYokoyama2020}
David Fern{\'a}ndez-Duque, Paul Shafer, and Keita Yokoyama.
\newblock Ekeland's variational principle in weak and strong systems of
  arithmetic.
\newblock \emph{Selecta Mathematica (N.S.)}, 26\penalty0 (5):\penalty0 Art. 68,
  2020.
\newblock \doi{10.1007/s00029-020-00597-z}.

\bibitem[Fern{\'a}ndez-Duque et~al.(2023)Fern{\'a}ndez-Duque, Shafer, Towsner,
  and Yokoyama]{FernandezDuqueShaferTowsnerYokoyama2023}
David Fern{\'a}ndez-Duque, Paul Shafer, Henry Towsner, and Keita Yokoyama.
\newblock Metric fixed point theory and partial impredicativity.
\newblock \emph{Philosophical Transactions of the Royal Society A},
  381\penalty0 (2248):\penalty0 20220012, 2023.
\newblock \doi{10.1098/rsta.2022.0012}.

\bibitem[Ferreira(1994)]{Fer94}
Fernando Ferreira.
\newblock A feasible theory for analysis.
\newblock \emph{The Journal of Symbolic Logic}, 59\penalty0 (3):\penalty0
  1001--1011, 1994.
\newblock \doi{10.2307/2275924}.

\bibitem[Fleming et~al.(2021)Fleming, G{\"o}{\"o}s, Impagliazzo, Pitassi,
  Robere, Tan, and Wigderson]{FGIPRTW21}
Noah Fleming, Mika G{\"o}{\"o}s, Russell Impagliazzo, Toniann Pitassi, Robert
  Robere, Li-Yang Tan, and Avi Wigderson.
\newblock On the power and limitations of branch and cut.
\newblock In \emph{36th Computational Complexity Conference (CCC 2021)}, volume
  200 of \emph{Leibniz International Proceedings in Informatics (LIPIcs)},
  pages 6:1--6:30, 2021.
\newblock \doi{10.4230/LIPIcs.CCC.2021.6}.

\bibitem[Flood et~al.(2022)Flood, Jura, Levin, and
  Markkanen]{FloodJuraLevinMarkkanen2022}
Stephen Flood, Matthew Jura, Oscar Levin, and Tyler Markkanen.
\newblock The computational strength of matchings in countable graphs.
\newblock \emph{Annals of Pure and Applied Logic}, 173\penalty0 (8):\penalty0
  103133, 2022.
\newblock \doi{10.1016/j.apal.2022.103133}.

\bibitem[Freund and Pischke(2026)]{FreundPischke2026QuasiFejerDynamical}
Anton Freund and Nicholas Pischke.
\newblock Effective rates for continuous-time quasi-{F}ej{\'e}r monotone
  dynamical systems, 2026.

\bibitem[Freund et~al.(2026)Freund, Pischke, and
  Uftring]{FreundPischkeUftring2026Avoiding}
Anton Freund, Nicholas Pischke, and Patrick Uftring.
\newblock Avoiding logical strength in real analysis, 2026.

\bibitem[Friedman(1975)]{Friedman1975}
Harvey Friedman.
\newblock Some systems of second order arithmetic and their use.
\newblock In \emph{Proceedings of the International Congress of Mathematicians
  (Vancouver, 1974)}, volume~1, pages 235--242. Canadian Mathematical Congress,
  1975.

\bibitem[Friedman(2009)]{Friedman2009FOMConstructiveAnalysis}
Harvey Friedman.
\newblock [{FOM}] constructive analysis.
\newblock Foundations of Mathematics (FOM) mailing list, 13 May 2009, 2009.
\newblock URL
  \url{https://web.archive.org/web/2020/https://cs.nyu.edu/pipermail/fom/2009-May/013613.html}.

\bibitem[Friedman et~al.(1983)Friedman, Simpson, and
  Smith]{FriedmanSimpsonSmith1983}
Harvey~M. Friedman, Stephen~G. Simpson, and Rick~L. Smith.
\newblock Countable algebra and set existence axioms.
\newblock \emph{Annals of Pure and Applied Logic}, 25\penalty0 (2):\penalty0
  141--181, 1983.
\newblock \doi{10.1016/0168-0072(83)90012-X}.

\bibitem[Fujiwara et~al.(2014)Fujiwara, Higuchi, and
  Kihara]{FujiwaraHiguchiKihara2014}
Makoto Fujiwara, Kojiro Higuchi, and Takayuki Kihara.
\newblock On the strength of marriage theorems and uniformity.
\newblock \emph{Mathematical Logic Quarterly}, 60\penalty0 (3):\penalty0
  136--153, 2014.
\newblock \doi{10.1002/malq.201300021}.

\bibitem[Gerhardy and Kohlenbach(2008)]{GerhardyKohlenbach2008TAMS}
Philipp Gerhardy and Ulrich Kohlenbach.
\newblock General logical metatheorems for functional analysis.
\newblock \emph{Transactions of the American Mathematical Society},
  360\penalty0 (5):\penalty0 2615--2660, 2008.
\newblock \doi{10.1090/S0002-9947-07-04429-7}.

\bibitem[Gherardi and Marcone(2009)]{GherardiMarcone2009}
Guido Gherardi and Alberto Marcone.
\newblock How incomputable is the separable {Hahn-Banach} theorem?
\newblock \emph{Notre Dame Journal of Formal Logic}, 50\penalty0 (4):\penalty0
  393--425, 2009.
\newblock \doi{10.1215/00294527-2009-018}.

\bibitem[Goh(2019)]{Goh2019KDT}
Jun~Le Goh.
\newblock Some computability-theoretic reductions between principles around
  {$\mathsf{ATR}_0$}, 2019.

\bibitem[G{\"o}{\"o}s et~al.(2019)G{\"o}{\"o}s, Kamath, Robere, and
  Sokolov]{GKRS19}
Mika G{\"o}{\"o}s, Pritish Kamath, Robert Robere, and Dmitry Sokolov.
\newblock Adventures in monotone complexity and {TFNP}.
\newblock In \emph{10th Innovations in Theoretical Computer Science Conference
  (ITCS 2019)}, volume 124 of \emph{Leibniz International Proceedings in
  Informatics (LIPIcs)}, pages 38:1--38:19, 2019.
\newblock \doi{10.4230/LIPIcs.ITCS.2019.38}.

\bibitem[G{\"o}{\"o}s et~al.(2022{\natexlab{a}})G{\"o}{\"o}s, Hollender, Jain,
  Maystre, Pires, Robere, and Tao]{GHJMPRT-CCC22}
Mika G{\"o}{\"o}s, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre,
  William Pires, Robert Robere, and Ran Tao.
\newblock Further collapses in {TFNP}.
\newblock In \emph{37th Computational Complexity Conference (CCC 2022)}, volume
  234 of \emph{Leibniz International Proceedings in Informatics (LIPIcs)},
  pages 33:1--33:15, 2022{\natexlab{a}}.
\newblock \doi{10.4230/LIPIcs.CCC.2022.33}.

\bibitem[G{\"o}{\"o}s et~al.(2022{\natexlab{b}})G{\"o}{\"o}s, Hollender, Jain,
  Maystre, Pires, Robere, and Tao]{GHJMPRT22}
Mika G{\"o}{\"o}s, Alexandros Hollender, Siddhartha Jain, Gilbert Maystre,
  William Pires, Robert Robere, and Ran Tao.
\newblock Separations in proof complexity and {TFNP}.
\newblock In \emph{2022 IEEE 63rd Annual Symposium on Foundations of Computer
  Science (FOCS)}, pages 1150--1161, 2022{\natexlab{b}}.
\newblock \doi{10.1109/FOCS54457.2022.00111}.

\bibitem[Gra{\c{c}}a and Zhong(2021)]{GracaZhong2021HyperbolicEquilibria}
Daniel~S. Gra{\c{c}}a and Ning Zhong.
\newblock The set of hyperbolic equilibria and of invertible zeros on the unit
  ball is computable.
\newblock \emph{Theoretical Computer Science}, 895:\penalty0 48--54, 2021.
\newblock \doi{10.1016/j.tcs.2021.09.028}.

\bibitem[Grigoriev(2001)]{Gri01}
Dima Grigoriev.
\newblock Linear lower bound on degrees of {P}ositivstellensatz calculus proofs
  for the parity.
\newblock \emph{Theoretical Computer Science}, 259\penalty0 (1--2):\penalty0
  613--622, 2001.
\newblock \doi{10.1016/S0304-3975(00)00157-2}.

\bibitem[Grigoriev and Vorobjov(2001)]{GV01}
Dima Grigoriev and Nicolai Vorobjov.
\newblock Complexity of {N}ull- and {P}ositivstellensatz proofs.
\newblock \emph{Annals of Pure and Applied Logic}, 113\penalty0
  (1--3):\penalty0 153--160, 2001.
\newblock \doi{10.1016/S0168-0072(01)00055-0}.

\bibitem[Gupta et~al.(2021)Gupta, Balakrishnan, and
  Ramdas]{GuptaBalakrishnanRamdas2021}
Chirag Gupta, Sivaraman Balakrishnan, and Aaditya Ramdas.
\newblock Path length bounds for gradient descent and flow.
\newblock \emph{Journal of Machine Learning Research}, 22\penalty0
  (68):\penalty0 1--63, 2021.
\newblock URL \url{https://jmlr.org/papers/v22/19-979.html}.

\bibitem[Hardin and Velleman(2001)]{HardinVelleman2001MVT}
Christopher~S. Hardin and Daniel~J. Velleman.
\newblock The mean value theorem in second order arithmetic.
\newblock \emph{Journal of Symbolic Logic}, 66\penalty0 (3):\penalty0
  1353--1358, 2001.
\newblock \doi{10.2307/2695111}.

\bibitem[Hirschfeldt(2014)]{Hirschfeldt2014}
Denis~R. Hirschfeldt.
\newblock \emph{Slicing the Truth: On the Computable and Reverse Mathematics of
  Combinatorial Principles}, volume~28 of \emph{Lecture Notes Series, Institute
  for Mathematical Sciences, National University of Singapore}.
\newblock World Scientific, 2014.

\bibitem[Hirst(1987)]{Hirst1987}
Jeffry~L. Hirst.
\newblock \emph{Combinatorics in Subsystems of Second Order Arithmetic}.
\newblock PhD thesis, The Pennsylvania State University, 1987.

\bibitem[Hirst(1990)]{Hirst1990}
Jeffry~L. Hirst.
\newblock Marriage theorems and reverse mathematics.
\newblock In \emph{Logic and Computation (Pittsburgh, PA, 1987)}, volume 106 of
  \emph{Contemporary Mathematics}, pages 181--196. American Mathematical
  Society, Providence, RI, 1990.
\newblock \doi{10.1090/conm/106/1057822}.

\bibitem[Hirst and Mummert(2017)]{HirstMummert2017}
Jeffry~L. Hirst and Carl Mummert.
\newblock Reverse mathematics of matroids.
\newblock In Adam Day, Michael Fellows, Noam Greenberg, Bakhadyr Khoussainov,
  Alexander Melnikov, and Frances Rosamond, editors, \emph{Computability and
  Complexity: Essays Dedicated to Rodney G. Downey on the Occasion of His 60th
  Birthday}, volume 10010 of \emph{Lecture Notes in Computer Science}, pages
  143--159. Springer, 2017.
\newblock \doi{10.1007/978-3-319-50062-1_12}.

\bibitem[Hoffman(1952)]{Hoffman1952}
Alan~J. Hoffman.
\newblock On approximate solutions of systems of linear inequalities.
\newblock \emph{Journal of Research of the National Bureau of Standards},
  49\penalty0 (4):\penalty0 263--265, 1952.

\bibitem[Humphreys and Simpson(1999)]{HumphreysSimpson1999}
A.~James Humphreys and Stephen~G. Simpson.
\newblock Separation and weak {K}{\"o}nig's lemma.
\newblock \emph{Journal of Symbolic Logic}, 64\penalty0 (1):\penalty0 268--278,
  1999.
\newblock \doi{10.2307/2586763}.

\bibitem[Hundal(2004)]{Hundal2004}
Hein~S. Hundal.
\newblock An alternating projection that does not converge in norm.
\newblock \emph{Nonlinear Analysis: Theory, Methods \& Applications},
  57\penalty0 (1):\penalty0 35--61, 2004.
\newblock \doi{10.1016/j.na.2003.11.004}.

\bibitem[Ishihara(1990)]{Ishihara1990HahnBanach}
Hajime Ishihara.
\newblock An omniscience principle, the {K}{\"o}nig lemma and the {Hahn-Banach}
  theorem.
\newblock \emph{Zeitschrift f{\"u}r Mathematische Logik und Grundlagen der
  Mathematik (Mathematical Logic Quarterly)}, 36\penalty0 (3):\penalty0
  237--240, 1990.
\newblock \doi{10.1002/malq.19900360307}.

\bibitem[Johnson et~al.(1988)Johnson, Papadimitriou, and Yannakakis]{JPY88}
David~S. Johnson, Christos~H. Papadimitriou, and Mihalis Yannakakis.
\newblock How easy is local search?
\newblock \emph{Journal of Computer and System Sciences}, 37\penalty0
  (1):\penalty0 79--100, 1988.
\newblock \doi{10.1016/0022-0000(88)90046-3}.

\bibitem[Jo{\'o}(2021)]{Joo2021}
Attila Jo{\'o}.
\newblock Proof of {N}ash-{W}illiams' intersection conjecture for countable
  matroids.
\newblock \emph{Advances in Mathematics}, 380:\penalty0 107608, 2021.
\newblock \doi{10.1016/j.aim.2021.107608}.

\bibitem[Julian and Richman(1984)]{JulianRichman1984}
William Julian and Fred Richman.
\newblock A uniformly continuous function on [0,1] that is everywhere different
  from its infimum.
\newblock \emph{Pacific Journal of Mathematics}, 111\penalty0 (2):\penalty0
  333--340, 1984.
\newblock \doi{10.2140/pjm.1984.111.333}.

\bibitem[Kihara(2012)]{Kihara2012PlanarContinua}
Takayuki Kihara.
\newblock Incomputability of simply connected planar continua.
\newblock \emph{Computability}, 1\penalty0 (2):\penalty0 131--152, 2012.
\newblock \doi{10.3233/COM-12012}.

\bibitem[Kihara and Pauly(2019)]{KiharaPauly2019TAMC}
Takayuki Kihara and Arno Pauly.
\newblock Finite choice, convex choice and sorting.
\newblock In T.~V. Gopal and Junzo Watada, editors, \emph{Theory and
  Applications of Models of Computation (TAMC 2019)}, volume 11436 of
  \emph{Lecture Notes in Computer Science}, pages 378--393. Springer, 2019.
\newblock \doi{10.1007/978-3-030-14812-6_23}.

\bibitem[Kohlenbach(1993{\natexlab{a}})]{Kohlenbach1993Chebycheff}
Ulrich Kohlenbach.
\newblock Effective moduli from ineffective uniqueness proofs. {An} unwinding
  of de {La Vall{\'e}e Poussin's} proof for {Chebycheff} approximation.
\newblock \emph{Annals of Pure and Applied Logic}, 64\penalty0 (1):\penalty0
  27--94, 1993{\natexlab{a}}.
\newblock \doi{10.1016/0168-0072(93)90213-W}.

\bibitem[Kohlenbach(1993{\natexlab{b}})]{Kohlenbach1993NFAO}
Ulrich Kohlenbach.
\newblock New effective moduli of uniqueness and uniform a priori estimates for
  constants of strong unicity by logical analysis of known proofs in best
  approximation theory.
\newblock \emph{Numerical Functional Analysis and Optimization}, 14\penalty0
  (5-6):\penalty0 581--606, 1993{\natexlab{b}}.
\newblock \doi{10.1080/01630569308816541}.

\bibitem[Kohlenbach(2001)]{Kohlenbach2001NFAO}
Ulrich Kohlenbach.
\newblock A quantitative version of a theorem due to
  {B}orwein-{R}eich-{S}hafrir.
\newblock \emph{Numerical Functional Analysis and Optimization}, 22\penalty0
  (5-6):\penalty0 641--656, 2001.
\newblock \doi{10.1081/NFA-100105311}.

\bibitem[Kohlenbach(2003)]{Kohlenbach2003JMAA}
Ulrich Kohlenbach.
\newblock Uniform asymptotic regularity for {M}ann iterates.
\newblock \emph{Journal of Mathematical Analysis and Applications},
  279\penalty0 (2):\penalty0 531--544, 2003.
\newblock \doi{10.1016/S0022-247X(03)00028-3}.

\bibitem[Kohlenbach(2005)]{Kohlenbach2005TAMS}
Ulrich Kohlenbach.
\newblock Some logical metatheorems with applications in functional analysis.
\newblock \emph{Transactions of the American Mathematical Society},
  357\penalty0 (1):\penalty0 89--128, 2005.
\newblock \doi{10.1090/S0002-9947-04-03515-9}.

\bibitem[Kohlenbach(2008)]{Kohlenbach2008APT}
Ulrich Kohlenbach.
\newblock \emph{Applied Proof Theory: Proof Interpretations and their Use in
  Mathematics}.
\newblock Springer Monographs in Mathematics. Springer, Berlin, Heidelberg,
  2008.
\newblock ISBN 978-3-540-77532-4.
\newblock \doi{10.1007/978-3-540-77533-1}.

\bibitem[Kohlenbach(2011)]{Kohlenbach2011AdvMath}
Ulrich Kohlenbach.
\newblock On quantitative versions of theorems due to {F}.{E}. {B}rowder and
  {R}. {W}ittmann.
\newblock \emph{Advances in Mathematics}, 226\penalty0 (3):\penalty0
  2764--2795, 2011.
\newblock \doi{10.1016/j.aim.2010.10.002}.

\bibitem[Kohlenbach(2019{\natexlab{a}})]{Kohlenbach2019ICM}
Ulrich Kohlenbach.
\newblock Proof-theoretic methods in nonlinear analysis.
\newblock In \emph{Proceedings of the International Congress of Mathematicians
  (ICM 2018), Rio de Janeiro, Vol. 2}, pages 61--82. World Scientific,
  2019{\natexlab{a}}.
\newblock \doi{10.1142/9789813272880_0045}.

\bibitem[Kohlenbach(2019{\natexlab{b}})]{Kohlenbach2019Moduli}
Ulrich Kohlenbach.
\newblock On the reverse mathematics and {Weihrauch} complexity of moduli of
  regularity and uniqueness.
\newblock \emph{Computability}, 8\penalty0 (3--4):\penalty0 377--387,
  2019{\natexlab{b}}.
\newblock \doi{10.3233/COM-180097}.

\bibitem[Kohlenbach(2020)]{Kohlenbach2020JNCA}
Ulrich Kohlenbach.
\newblock Quantitative analysis of a {H}alpern-type proximal point algorithm
  for accretive operators in {B}anach spaces.
\newblock \emph{Journal of Nonlinear and Convex Analysis}, 21:\penalty0
  2125--2138, 2020.

\bibitem[Kohlenbach(2021)]{Kohlenbach2021JCA}
Ulrich Kohlenbach.
\newblock Quantitative results on the proximal point algorithm in uniformly
  convex {B}anach spaces.
\newblock \emph{Journal of Convex Analysis}, 28\penalty0 (1):\penalty0 11--18,
  2021.
\newblock \doi{10.68381/jca28002}.

\bibitem[Kohlenbach(2022)]{Kohlenbach2022OptimLett}
Ulrich Kohlenbach.
\newblock On the proximal point algorithm and its {H}alpern-type variant for
  generalized monotone operators in {H}ilbert space.
\newblock \emph{Optimization Letters}, 16\penalty0 (2):\penalty0 611--621,
  2022.
\newblock \doi{10.1007/s11590-021-01738-9}.

\bibitem[Kohlenbach(2023)]{Kohlenbach2023Kreisel}
Ulrich Kohlenbach.
\newblock Kreisel's ``shift of emphasis'' and contemporary proof mining.
\newblock \emph{Studies in Logic}, 16\penalty0 (3):\penalty0 1--35, 2023.

\bibitem[Kohlenbach(2026)]{Kohlenbach2026EPTCS}
Ulrich Kohlenbach.
\newblock On the computational content of moduli of regularity and their
  logical strength.
\newblock In \emph{Proceedings LTT 2026}, volume 441 of \emph{Electronic
  Proceedings in Theoretical Computer Science}, pages 185--196, 2026.
\newblock \doi{10.4204/EPTCS.441.11}.

\bibitem[Kohlenbach and Leu{\c{s}}tean(2012)]{KohlenbachLeustean2012AdvMath}
Ulrich Kohlenbach and Lauren{\c{t}}iu Leu{\c{s}}tean.
\newblock Effective metastability of {H}alpern iterates in {CAT}(0) spaces.
\newblock \emph{Advances in Mathematics}, 231\penalty0 (5):\penalty0
  2526--2556, 2012.
\newblock \doi{10.1016/j.aim.2012.06.028}.

\bibitem[Kohlenbach and Oliva(2003)]{KohlenbachOliva2003APAL}
Ulrich Kohlenbach and Paulo Oliva.
\newblock Proof mining in {$L_1$}-approximation.
\newblock \emph{Annals of Pure and Applied Logic}, 121\penalty0 (1):\penalty0
  1--38, 2003.
\newblock \doi{10.1016/S0168-0072(02)00081-7}.

\bibitem[Kohlenbach and Pinto(2022)]{KohlenbachPinto2022JMAA}
Ulrich Kohlenbach and Pedro Pinto.
\newblock Quantitative translations for viscosity approximation methods in
  hyperbolic spaces.
\newblock \emph{Journal of Mathematical Analysis and Applications},
  507\penalty0 (2):\penalty0 125823, 2022.
\newblock \doi{10.1016/j.jmaa.2021.125823}.

\bibitem[Kohlenbach and Pinto(2026)]{KohlenbachPinto2026JCA}
Ulrich Kohlenbach and Pedro Pinto.
\newblock Fej{\'e}r monotone sequences revisited.
\newblock \emph{Journal of Convex Analysis}, 33\penalty0 (1-2):\penalty0
  75--90, 2026.
\newblock \doi{10.68381/jca33005}.

\bibitem[Kohlenbach and Pischke(2023)]{KohlenbachPischke2023PTRSA}
Ulrich Kohlenbach and Nicholas Pischke.
\newblock Proof theory and non-smooth analysis.
\newblock \emph{Philosophical Transactions of the Royal Society A:
  Mathematical, Physical and Engineering Sciences}, 381\penalty0
  (2248):\penalty0 20220015, 2023.
\newblock \doi{10.1098/rsta.2022.0015}.

\bibitem[Kohlenbach and Safarik(2014)]{KohlenbachSafarik2014}
Ulrich Kohlenbach and Pavol Safarik.
\newblock Fluctuations, effective learnability and metastability in analysis.
\newblock \emph{Annals of Pure and Applied Logic}, 165\penalty0 (1):\penalty0
  266--304, 2014.
\newblock \doi{10.1016/j.apal.2013.07.014}.
\newblock URL
  \url{https://www2.mathematik.tu-darmstadt.de/~kohlenbach/mind_ps_revised.pdf}.

\bibitem[Kohlenbach et~al.(2018)Kohlenbach, Leu{\c{s}}tean, and
  Nicolae]{KohlenbachLeusteanNicolae2018}
Ulrich Kohlenbach, Lauren{\c{t}}iu Leu{\c{s}}tean, and Adriana Nicolae.
\newblock Quantitative results on {F}ej{\'e}r monotone sequences.
\newblock \emph{Communications in Contemporary Mathematics}, 20\penalty0
  (2):\penalty0 1750015, 2018.
\newblock \doi{10.1142/S0219199717500158}.

\bibitem[Kohlenbach et~al.(2019)Kohlenbach, L{\'o}pez-Acedo, and
  Nicolae]{KohlenbachLopezAcedoNicolae2019}
Ulrich Kohlenbach, Genaro L{\'o}pez-Acedo, and Adriana Nicolae.
\newblock Moduli of regularity and rates of convergence for {Fej{\'e}r}
  monotone sequences.
\newblock \emph{Israel Journal of Mathematics}, 232\penalty0 (1):\penalty0
  261--297, 2019.
\newblock \doi{10.1007/s11856-019-1870-x}.

\bibitem[Ko{\l}odziejczyk and Thapen(2024)]{KT24dominance}
Leszek~Aleksander Ko{\l}odziejczyk and Neil Thapen.
\newblock The strength of the dominance rule, 2024.

\bibitem[Ko{\l}odziejczyk et~al.(2011)Ko{\l}odziejczyk, Nguyen, and
  Thapen]{KNT11}
Leszek~Aleksander Ko{\l}odziejczyk, Phuong Nguyen, and Neil Thapen.
\newblock The provably total {NP} search problems of weak second order bounded
  arithmetic.
\newblock \emph{Annals of Pure and Applied Logic}, 162\penalty0 (6):\penalty0
  419--446, 2011.
\newblock \doi{10.1016/j.apal.2010.12.002}.

\bibitem[Kontogiannis et~al.(2026)Kontogiannis, Panageas, and Pollatos]{KPP26}
Andreas Kontogiannis, Ioannis Panageas, and Vasilis Pollatos.
\newblock The computational complexity of avoiding strict saddle points in
  constrained optimization, 2026.

\bibitem[Kurdyka(1998)]{Kurdyka1998}
Krzysztof Kurdyka.
\newblock On gradients of functions definable in o-minimal structures.
\newblock \emph{Annales de l'Institut Fourier}, 48\penalty0 (3):\penalty0
  769--783, 1998.

\bibitem[Lasserre(2001)]{Las01}
Jean~B. Lasserre.
\newblock Global optimization with polynomials and the problem of moments.
\newblock \emph{SIAM Journal on Optimization}, 11\penalty0 (3):\penalty0
  796--817, 2001.
\newblock \doi{10.1137/S1052623400366802}.

\bibitem[Le and Cook(2012)]{LC12}
Dai Tri~Man Le and Stephen~A. Cook.
\newblock Formalizing randomized matching algorithms.
\newblock \emph{Logical Methods in Computer Science}, 8\penalty0 (3), 2012.
\newblock \doi{10.2168/LMCS-8(3:5)2012}.

\bibitem[Le~Roux and Pauly(2015)]{LeRouxPauly2015LMCS}
St{\'e}phane Le~Roux and Arno Pauly.
\newblock Finite choice, convex choice and finding roots.
\newblock \emph{Logical Methods in Computer Science}, 11\penalty0 (4):\penalty0
  Paper 6, 2015.
\newblock \doi{10.2168/LMCS-11(4:6)2015}.

\bibitem[Le~Roux and Ziegler(2008)]{LeRouxZiegler2008}
St{\'e}phane Le~Roux and Martin Ziegler.
\newblock Singular coverings and non-uniform notions of closed set
  computability.
\newblock \emph{Mathematical Logic Quarterly}, 54\penalty0 (5):\penalty0
  545--560, 2008.
\newblock \doi{10.1002/malq.200610058}.

\bibitem[Lee et~al.(2023)Lee, Boche, and Kutyniok]{LeeBocheKutyniok2023}
Yunseok Lee, Holger Boche, and Gitta Kutyniok.
\newblock Computability of optimizers, 2023.

\bibitem[Lemke and Howson(1964)]{LemkeHowson1964}
Carlton~E. Lemke and Joseph~T. Howson, Jr.
\newblock Equilibrium points of bimatrix games.
\newblock \emph{Journal of the Society for Industrial and Applied Mathematics},
  12\penalty0 (2):\penalty0 413--423, 1964.

\bibitem[Leu{\c{s}}tean(2007)]{Leustean2007JUCS}
Lauren{\c{t}}iu Leu{\c{s}}tean.
\newblock Rates of asymptotic regularity for {H}alpern iterations of
  nonexpansive mappings.
\newblock \emph{Journal of Universal Computer Science}, 13\penalty0
  (11):\penalty0 1680--1691, 2007.
\newblock \doi{10.3217/jucs-013-11-1680}.

\bibitem[Leu{\c{s}}tean and Pinto(2021)]{LeusteanPinto2021COAP}
Lauren{\c{t}}iu Leu{\c{s}}tean and Pedro Pinto.
\newblock Quantitative results on a {H}alpern-type proximal point algorithm.
\newblock \emph{Computational Optimization and Applications}, 79\penalty0
  (1):\penalty0 101--125, 2021.
\newblock \doi{10.1007/s10589-021-00263-w}.

\bibitem[Leu{\c{s}}tean et~al.(2018)Leu{\c{s}}tean, Nicolae, and
  Sipo{\c{s}}]{LeusteanNicolaeSipos2018JOGO}
Lauren{\c{t}}iu Leu{\c{s}}tean, Adriana Nicolae, and Andrei Sipo{\c{s}}.
\newblock An abstract proximal point algorithm.
\newblock \emph{Journal of Global Optimization}, 72\penalty0 (3):\penalty0
  553--577, 2018.
\newblock \doi{10.1007/s10898-018-0655-9}.

\bibitem[Lieder(2021)]{Lieder2021}
Felix Lieder.
\newblock On the convergence rate of the {H}alpern-iteration.
\newblock \emph{Optimization Letters}, 15\penalty0 (2):\penalty0 405--418,
  2021.
\newblock \doi{10.1007/s11590-020-01617-9}.

\bibitem[Lombardi et~al.(2020)Lombardi, Perrucci, and Roy]{LPR20}
Henri Lombardi, Daniel Perrucci, and Marie-Fran{\c{c}}oise Roy.
\newblock An elementary recursive bound for effective {P}ositivstellensatz and
  {H}ilbert's 17th problem.
\newblock \emph{Memoirs of the American Mathematical Society}, 263\penalty0
  (1277), 2020.
\newblock \doi{10.1090/memo/1277}.

\bibitem[Nemirovsky and Yudin(1983)]{NemirovskyYudin1983}
Arkadi~S. Nemirovsky and David~B. Yudin.
\newblock \emph{Problem Complexity and Method Efficiency in Optimization}.
\newblock Wiley-Interscience Series in Discrete Mathematics. Wiley, Chichester,
  New York, 1983.
\newblock ISBN 0471103454.

\bibitem[Neri and Pischke(2025)]{NeriPischke2025FMS}
Morenikeji Neri and Nicholas Pischke.
\newblock Proof mining and probability theory.
\newblock \emph{Forum of Mathematics, Sigma}, 13:\penalty0 e187, 2025.
\newblock \doi{10.1017/fms.2025.10138}.

\bibitem[Neri and Powell(2025)]{NeriPowell2025TAMSB}
Morenikeji Neri and Thomas Powell.
\newblock On quantitative convergence for stochastic processes: Crossings,
  fluctuations and martingales.
\newblock \emph{Transactions of the American Mathematical Society, Series B},
  12:\penalty0 974--1019, 2025.
\newblock \doi{10.1090/btran/229}.

\bibitem[Neri and Powell(2026)]{NeriPowell2026AAP}
Morenikeji Neri and Thomas Powell.
\newblock A quantitative {R}obbins-{S}iegmund theorem.
\newblock \emph{The Annals of Applied Probability}, 36\penalty0 (1):\penalty0
  636--651, 2026.
\newblock \doi{10.1214/25-AAP2242}.

\bibitem[Neri et~al.(2025)Neri, Pischke, and
  Powell]{NeriPischkePowell2025abstract}
Morenikeji Neri, Nicholas Pischke, and Thomas Powell.
\newblock An abstract effective convergence theorem for stochastic processes,
  with applications to stochastic approximation, 2025.

\bibitem[Neri et~al.(2026)Neri, Pischke, and
  Powell]{NeriPischkePowell2026fluct}
Morenikeji Neri, Nicholas Pischke, and Thomas Powell.
\newblock Generalized fluctuation bounds for stochastic algorithms in the
  presence of compactness, 2026.

\bibitem[Nesterov(2004)]{Nesterov2004}
Yurii Nesterov.
\newblock \emph{Introductory Lectures on Convex Optimization: A Basic Course}.
\newblock Kluwer Academic Publishers, 2004.

\bibitem[Neumann(2015)]{Neumann2015LMCS}
Eike Neumann.
\newblock Computational problems in metric fixed point theory and their
  {W}eihrauch degrees.
\newblock \emph{Logical Methods in Computer Science}, 11\penalty0 (4):\penalty0
  Paper 20, 2015.
\newblock \doi{10.2168/LMCS-11(4:20)2015}.

\bibitem[Nguyen(2008)]{Ngu08}
Phuong~The Nguyen.
\newblock \emph{Bounded Reverse Mathematics}.
\newblock PhD thesis, University of Toronto, Graduate Department of Computer
  Science, 2008.
\newblock URL
  \url{https://eccc.weizmann.ac.il/static/books/Bounded_Reverse_Mathematics}.

\bibitem[O'Donnell(2017)]{ODo17}
Ryan O'Donnell.
\newblock {SOS} is not obviously automatizable, even approximately.
\newblock In \emph{8th Innovations in Theoretical Computer Science Conference
  (ITCS 2017)}, volume~67 of \emph{Leibniz International Proceedings in
  Informatics (LIPIcs)}, pages 59:1--59:10, 2017.
\newblock \doi{10.4230/LIPIcs.ITCS.2017.59}.

\bibitem[Papadimitriou(1994)]{Pap94}
Christos~H. Papadimitriou.
\newblock On the complexity of the parity argument and other inefficient proofs
  of existence.
\newblock \emph{Journal of Computer and System Sciences}, 48\penalty0
  (3):\penalty0 498--532, 1994.
\newblock \doi{10.1016/S0022-0000(05)80063-7}.

\bibitem[Parrilo(2003)]{Par03}
Pablo~A. Parrilo.
\newblock Semidefinite programming relaxations for semialgebraic problems.
\newblock \emph{Mathematical Programming}, 96\penalty0 (2):\penalty0 293--320,
  2003.
\newblock \doi{10.1007/s10107-003-0387-5}.

\bibitem[Pauly(2010)]{Pauly2010Nash}
Arno Pauly.
\newblock How incomputable is finding {Nash} equilibria?
\newblock \emph{Journal of Universal Computer Science}, 16\penalty0
  (18):\penalty0 2686--2710, 2010.
\newblock \doi{10.3217/jucs-016-18-2686}.

\bibitem[Peng et~al.(2023)Peng, Peng, and Yamazaki]{PengPengYamazaki2023}
NingNing Peng, Weiguang Peng, and Takeshi Yamazaki.
\newblock Mixed {N}ash equilibria for continuous games and reverse mathematics.
\newblock \emph{Quaestiones Mathematicae}, 46\penalty0 (4):\penalty0 621--632,
  2023.
\newblock \doi{10.2989/16073606.2022.2035448}.

\bibitem[Peng and Yamazaki(2017)]{PengYamazaki2017}
Weiguang Peng and Takeshi Yamazaki.
\newblock Two kinds of fixed point theorems and reverse mathematics.
\newblock \emph{Mathematical Logic Quarterly}, 63\penalty0 (5):\penalty0
  454--461, 2017.
\newblock \doi{10.1002/malq.201600096}.

\bibitem[Pischke(2024)]{Pischke2024JML}
Nicholas Pischke.
\newblock Logical metatheorems for accretive and (generalized) monotone
  set-valued operators.
\newblock \emph{Journal of Mathematical Logic}, 24\penalty0 (2):\penalty0
  2350008, 2024.
\newblock \doi{10.1142/S0219061323500083}.

\bibitem[Pischke(2025)]{Pischke2025Optim}
Nicholas Pischke.
\newblock Generalized {F}ej{\'e}r monotone sequences and their finitary
  content.
\newblock \emph{Optimization}, 74\penalty0 (14):\penalty0 3771--3838, 2025.
\newblock \doi{10.1080/02331934.2024.2390114}.

\bibitem[Pischke and Kohlenbach(2022)]{PischkeKohlenbach2022NumAlg}
Nicholas Pischke and Ulrich Kohlenbach.
\newblock Quantitative analysis of a subgradient-type method for equilibrium
  problems.
\newblock \emph{Numerical Algorithms}, 90\penalty0 (1):\penalty0 197--219,
  2022.
\newblock \doi{10.1007/s11075-021-01184-9}.

\bibitem[Pischke and Powell(2026)]{PischkePowell2026JOTA}
Nicholas Pischke and Thomas Powell.
\newblock Asymptotic regularity of a generalised stochastic {H}alpern scheme.
\newblock \emph{Journal of Optimization Theory and Applications}, 210\penalty0
  (1):\penalty0 3, 2026.
\newblock \doi{10.1007/s10957-026-03032-z}.

\bibitem[Pudl{\'a}k(1997)]{Pud97}
Pavel Pudl{\'a}k.
\newblock Lower bounds for resolution and cutting plane proofs and monotone
  computations.
\newblock \emph{The Journal of Symbolic Logic}, 62\penalty0 (3):\penalty0
  981--998, 1997.
\newblock \doi{10.2307/2275583}.

\bibitem[Raghavendra and Weitz(2017)]{RW17}
Prasad Raghavendra and Benjamin Weitz.
\newblock On the bit complexity of sum-of-squares proofs.
\newblock In \emph{44th International Colloquium on Automata, Languages, and
  Programming (ICALP 2017)}, volume~80 of \emph{Leibniz International
  Proceedings in Informatics (LIPIcs)}, pages 80:1--80:13, 2017.
\newblock \doi{10.4230/LIPIcs.ICALP.2017.80}.

\bibitem[Rockafellar(1970)]{Rockafellar1970}
R.~Tyrrell Rockafellar.
\newblock \emph{Convex Analysis}.
\newblock Princeton University Press, 1970.

\bibitem[Sabach and Shtern(2017)]{SabachShtern2017}
Shoham Sabach and Shimrit Shtern.
\newblock A first order method for solving convex bilevel optimization
  problems.
\newblock \emph{SIAM Journal on Optimization}, 27\penalty0 (2):\penalty0
  640--660, 2017.
\newblock \doi{10.1137/16M105592X}.

\bibitem[Schoenebeck(2008)]{Sch08}
Grant Schoenebeck.
\newblock Linear level {L}asserre lower bounds for certain $k$-{CSP}s.
\newblock In \emph{2008 49th Annual IEEE Symposium on Foundations of Computer
  Science (FOCS)}, pages 593--602, 2008.
\newblock \doi{10.1109/FOCS.2008.74}.

\bibitem[Shafer(2012)]{Shafer2012}
Paul Shafer.
\newblock Menger's theorem in {$\Pi^1_1\text{-}\mathsf{CA}_0$}.
\newblock \emph{Archive for Mathematical Logic}, 51\penalty0 (3--4):\penalty0
  407--423, 2012.
\newblock \doi{10.1007/s00153-012-0269-8}.

\bibitem[Shioji and Tanaka(1990)]{ShiojiTanaka1990}
Naoki Shioji and Kazuyuki Tanaka.
\newblock Fixed point theory in weak second-order arithmetic.
\newblock \emph{Annals of Pure and Applied Logic}, 47\penalty0 (2):\penalty0
  167--188, 1990.
\newblock \doi{10.1016/0168-0072(90)90068-D}.

\bibitem[Simpson(1984)]{Simpson1984}
Stephen~G. Simpson.
\newblock Which set existence axioms are needed to prove the {Cauchy/Peano}
  theorem for ordinary differential equations?
\newblock \emph{Journal of Symbolic Logic}, 49\penalty0 (3):\penalty0 783--802,
  1984.
\newblock \doi{10.2307/2274131}.

\bibitem[Simpson(1994)]{Simpson1994}
Stephen~G. Simpson.
\newblock On the strength of {K}{\"o}nig's duality theorem for countable
  bipartite graphs.
\newblock \emph{Journal of Symbolic Logic}, 59\penalty0 (1):\penalty0 113--123,
  1994.
\newblock \doi{10.2307/2275254}.

\bibitem[Simpson(2009)]{Simpson2009SOSOA}
Stephen~G. Simpson.
\newblock \emph{Subsystems of Second Order Arithmetic}.
\newblock Perspectives in Logic. Cambridge University Press / Association for
  Symbolic Logic, 2 edition, 2009.
\newblock ISBN 978-0-521-88439-6.
\newblock \doi{10.1017/CBO9780511581007}.

\bibitem[Sipo{\c{s}}(2022)]{Sipos2022OptimLett}
Andrei Sipo{\c{s}}.
\newblock Quantitative inconsistent feasibility for averaged mappings.
\newblock \emph{Optimization Letters}, 16\penalty0 (6):\penalty0 1915--1925,
  2022.
\newblock \doi{10.1007/s11590-021-01812-2}.

\bibitem[Soltys and Cook(2004)]{SoltysCook2004}
Michael Soltys and Stephen Cook.
\newblock The proof complexity of linear algebra.
\newblock \emph{Annals of Pure and Applied Logic}, 130\penalty0
  (1--3):\penalty0 277--323, 2004.
\newblock \doi{10.1016/j.apal.2003.10.018}.

\bibitem[Specker(1949)]{Specker1949}
Ernst Specker.
\newblock Nicht konstruktiv beweisbare {S}{\"a}tze der {A}nalysis.
\newblock \emph{The Journal of Symbolic Logic}, 14\penalty0 (3):\penalty0
  145--158, 1949.
\newblock \doi{10.2307/2267043}.

\bibitem[Specker(1959)]{Specker1959}
Ernst Specker.
\newblock Der {S}atz vom {M}aximum in der rekursiven {A}nalysis.
\newblock In Arend Heyting, editor, \emph{Constructivity in Mathematics (Proc.
  Colloq. Amsterdam 1957)}, Studies in Logic and the Foundations of
  Mathematics, pages 254--265. North-Holland, Amsterdam, 1959.

\bibitem[Stepanov and Teplitskaya(2017)]{StepanovTeplitskaya2017}
Eugene Stepanov and Yana Teplitskaya.
\newblock Self-contracted curves have finite length.
\newblock \emph{Journal of the London Mathematical Society}, 96\penalty0
  (2):\penalty0 455--481, 2017.
\newblock \doi{10.1112/jlms.12068}.

\bibitem[Tao(2008)]{Tao2008ETDS}
Terence Tao.
\newblock Norm convergence of multiple ergodic averages for commuting
  transformations.
\newblock \emph{Ergodic Theory and Dynamical Systems}, 28\penalty0
  (2):\penalty0 657--688, 2008.
\newblock \doi{10.1017/S0143385708000011}.

\bibitem[Tarski(1951)]{Tarski1951}
Alfred Tarski.
\newblock \emph{A Decision Method for Elementary Algebra and Geometry}.
\newblock University of California Press, 2 edition, 1951.

\bibitem[Taylor et~al.(2017)Taylor, Hendrickx, and
  Glineur]{TaylorHendrickxGlineur2017}
Adrien~B. Taylor, Julien~M. Hendrickx, and Fran{\c{c}}ois Glineur.
\newblock Smooth strongly convex interpolation and exact worst-case performance
  of first-order methods.
\newblock \emph{Mathematical Programming}, 161\penalty0 (1-2):\penalty0
  307--345, 2017.
\newblock \doi{10.1007/s10107-016-1009-3}.

\bibitem[Towsner(2013)]{Towsner2013}
Henry Towsner.
\newblock Partial impredicativity in reverse mathematics.
\newblock \emph{Journal of Symbolic Logic}, 78\penalty0 (2):\penalty0 459--488,
  2013.
\newblock \doi{10.2178/jsl.7802070}.

\bibitem[Tzameret and Cook(2021)]{TC21}
Iddo Tzameret and Stephen~A. Cook.
\newblock Uniform, integral, and feasible proofs for the determinant
  identities.
\newblock \emph{Journal of the ACM}, 68\penalty0 (2):\penalty0 1--80, 2021.
\newblock \doi{10.1145/3431922}.

\bibitem[Weihrauch(2000)]{Weihrauch2000}
Klaus Weihrauch.
\newblock \emph{Computable Analysis: An Introduction}.
\newblock Texts in Theoretical Computer Science. An EATCS Series. Springer,
  Berlin, 2000.
\newblock \doi{10.1007/978-3-642-56999-9}.

\bibitem[Wittmann(1992)]{Wittmann1992}
Rainer Wittmann.
\newblock Approximation of fixed points of nonexpansive mappings.
\newblock \emph{Archiv der Mathematik}, 58\penalty0 (5):\penalty0 486--491,
  1992.

\bibitem[Zheng et~al.(2005)Zheng, Rettinger, and
  Barmpalias]{ZhengRettingerBarmpalias2005hMonotonically}
Xizhong Zheng, Robert Rettinger, and George Barmpalias.
\newblock h-monotonically computable real numbers.
\newblock \emph{Mathematical Logic Quarterly}, 51\penalty0 (2):\penalty0
  157--170, 2005.
\newblock \doi{10.1002/malq.200410016}.

\end{thebibliography}


\clearpage
\appendix
\crefalias{section}{appendix}\crefalias{subsection}{subappendix}\crefalias{subsubsection}{subsubappendix}
\addtocontents{toc}{\protect\addvspace{5pt}\protect\noindent{\protect\sffamily\protect\small\protect\bfseries\protect\color{muted}Appendix}\protect\par}
\noindent{\color{refcool}\rule{\linewidth}{1.6pt}}\par\vspace{8pt}
\noindent{\sffamily\bfseries\LARGE\color{navy}Appendix}\par\vspace{3pt}
\noindent{\sffamily\small\color{muted}The Logical Anatomy of Optimization}\par\vspace{6pt}
\noindent{\color{rulegray}\rule{\linewidth}{0.5pt}}\par\vspace{4pt}
\suppressfloats[t]
\input{appendix}
\input{appendix_lp}


\end{document}