\section{Introduction}
\label{sect:intro}

The LIGO/Virgo Collaboration has recently released the second Gravitational Wave Transient Catalog \citep[GWTC-2, ][]{lvc2020cat}. Together with results from the first two observing runs \citep[GWTC-1, ][]{lvc2019cat}, the full gravitational-wave (GW) catalog is comprised of more than $50$ events, and is transforming our understanding of black holes (BHs) and neutron stars (NSs) across cosmic space and time \citep{lvc2020catb,lvc2020catc}.  Despite this wealth of information, the origin of many of these binary mergers, particularly the binary BHs (BBHs) mergers, remains highly uncertain.

Various formation scenarios for BBH mergers have been proposed over the years, including isolated binary star evolution \citep[e.g.,][]{bel16b,demi2016,gm2018,Breivik2020}, dynamical formation in dense star clusters \citep[e.g.,][]{askar17,baner18,fragk2018,Rodriguez2018,sams18,ham2019,krem2019}, mergers in triple and quadruple systems \citep[e.g.,][]{antoper12,ll18,GrishinPerets2018,Rodriguez2018a,fragg2019,flp2019,fragk2019,liu2019,FragioneLoeb2020,MartinezFragione2020}, mergers of compact binaries in galactic nuclei \citep[e.g.,][]{bart17,sto17,rasskoc2019,mck2020}, and mergers of primordial black holes \citep[e.g.,][]{sasaki2016}. While several formation scenarios can account for some or even all of the BBH merger rate \citep{2021RNAAS...5...19R}, the contribution of different channels must be disentangled using a combination of the mass, spin, redshift, and eccentricity distributions as the number of detected events increases \citep[e.g.,][]{olea09,Fishbachetal2017,gondan2018,perna2019,WongBreivik2020,2021ApJ...910..152Z}.

The majority of the BBHs in GWTC-2 are consistent with having equal mass components \citep{lvc2020catb}. This is also consistent with theoretical models of BBH formation through either isolated binary evolution or dynamical formation, which prefer BBH mergers with mass ratios near unity \citep[e.g.,][]{bel16b,Rodriguez2016}. Nevertheless, GW190412, a BBH with mass ratio of nearly four-to-one, provides evidence for the existence of mergers with small mass ratios. It has been proposed that these systems can be formed through isolated binary evolution \citep[e.g.,][]{OlejakFishbach2020} or as a result of repeated mergers in star clusters \citep[e.g.,][]{2020ApJ...896L..10R}.

Another channel that can potentially produce BBH mergers with smaller mass ratios is the Lidov-Kozai (LK) mechanism in triple systems \citep{Kozai1962,Lidov1962}. In this scenario, a tertiary companion on a sufficiently inclined outer orbit could drive the inner binary to extreme eccentricities, leading to efficient gravitational radiation and orbital decay. In this Letter, we study in detail the mass ratio distribution of BBH mergers induced by tertiary companions in triple systems and compare them to the mass ratio distributions from detailed binary population synthesis and star cluster dynamics. We show that the triple channel predicts a flatter mass ratio distribution than either isolation binary or dynamical formation scenarios, and occupies a distinct region of the of total mass, mass ratio, and spin parameter space for merging BBHs, which can be used to disentangle the triple contribution to the overall observed GW sources.

The Letter is organized as follows. In Section~\ref{sect:methods}, we present our method to build populations of merging binary black holes. In Section~\ref{sect:results}, we compare the distributions of total masses and mass ratios for different channels. Finally, in Section~\ref{sect:concl}, we discuss the implications of our results and draw our conclusions.

\section{Models of Merging Binaries}
\label{sect:methods}

We compare three populations of merging BBHs: those created from mergers from ``isolated'' stellar binaries, those from stellar triples where the merger is induced by the third companion due to secular interactions, and those formed through three- and four-body encounters in dense star clusters.  As much as possible, the three sets of results presented here strive to use identical prescriptions for the evolution of massive stars.  To that end, both the binary and triple evolution are generated using the \texttt{COSMIC} software package for population synthesis \citep{Breivik2020}. The BBHs from GCs are taken from the models presented in \cite{Kremer2020}, which used nearly identical physical assumptions for the evolution of massive stars. See \ref{sec:gcs} for specific differences as well as further details about the cluster models.

As with any population synthesis study, the choice of initial conditions can change the resulting distributions by several orders of magnitude.  As such, any claims regarding the difference between formation channels must be made using \emph{the same} initial conditions and physical choices.  The binary and triple initial conditions we use here are taken from the same population, whose orbital periods, masses, and mass ratios are chosen to be consistent with observations of stellar triples in galactic fields. This is consistent with observational studies of stellar multiplicity, which suggest that the typical massive O star (the progenitors of BHs) have more than one companion on average \citep{Moe2017,Moe2019}.  We sample a range of stellar metallicities, from $Z=0.0001$ to $0.03$ and, and cosmologically sample both the binaries and triples from the same star formation and metallicity enrichment distributions. See Appendix A for more details. As in our previous work, we cleanly delineate between ``binary'' and ``triple'' BBH mergers by only considering as triple-induced mergers those systems whose inner binary would \emph{not} have merged within a Hubble time due in the absence of a tertiary companion.  In other words, our triple population is specifically limited to those whose mergers are due to the LK effect.

In addition to the astrophysical populations of merging BBHs, we are also interested in the population of BBHs detectable by advanced GW observatories.  Here we follow the technique presented in \cite{Rodriguez2019}.  We assign each BBH a detectability weight defined as

\begin{equation}
    w_{\rm det} \equiv f_d (m_1,m_2,z) \frac{dVc}{dz} \frac{dt_s}{dt_o} ~,
    \label{eqn:gwweight}
\end{equation}

\noindent where $f_d$ is the fraction of sources with masses $m_1$ and $m_2$ merging at redshift $z$ that are detectable (defined as a signal-to-noise ratio of 8 or higher) by a three-detector network operating at the design sensitivity of Advanced LIGO \citep{Abbott2018}.  $\frac{dVc}{dz}$ is the amount of co-moving volume in a slice of the universe at redshift $z$, and $\frac{dt_s}{dt_o} \equiv \frac{1}{1+z}$ is the difference in co-moving time between the merger redshift and the observer at $z=0$.  We use the IMRPhenomD GW approximant for computing GW detectability \citep{2016PhRvD..93d4006H,2016PhRvD..93d4007K}. Each of the detectable quantities presented here are weighted using \eqref{eqn:gwweight}.

\section{Results}
\label{sect:results}

\begin{figure*}
\includegraphics[width=0.96\textwidth]{massratio_pdf.pdf}
\caption{Distribution of mass ratios for different BBH formation channels. The merging sample is weighted by star (cluster) formation history for the field (cluster) mergers (left) and detectability (right), to produce realistic astrophysical and detectable populations in the local universe. In addition to the field binary (solid blue) and field triple (dashed black) distributions, we also include the mass ratio distributions from GC clusters using data presented in \cite{Kremer2020}, split into 1G (dotted orange) and 2G (dotted green) channels. The median and 90\% regions for the mass ratios from the Power-law model from GWTC-2 (solid purple line and purple shading) is presented in the left panel.}
\label{fig:massratio}
\end{figure*}

\begin{figure*}
\centering
\includegraphics[]{mtot_q_contours.pdf}
\caption{Contour plots for mass ratio--total mass distributions for different channels. The contours show the regions containing 99.5 (solid), 90 (dashed), and 60 (dotted) percent of all data points. The left column shows astrophysically weighted samples while the right column shows the same samples weighted by detectability. In each row, the field triple channel (black) is compared to the field binary (top, red), cluster 1G (middle, orange), and cluster 2G (bottom, green) channels. Also included in the right column is the detection of GW190412 during O3a \citep{theligoscientificcollaboration2020}. Note the differing range in the y-axis of each row.}
\label{fig:mtot_q}
\end{figure*}

\begin{figure}
\includegraphics[]{zams_triples.pdf}
\caption{Top: median and 50 percentile initial inner binary mass ratio as a function of inner semi-major axis. Bottom: normalized distribution of inner semi-major axis prior to stellar evolution for all initial triples in the sample (solid blue), merging binaries (dash-dotted red), and merging triples (dashed green). }
\label{fig:a1i}
\end{figure}

\begin{figure}
\includegraphics[]{compare_cut.pdf}
\caption{Distribution of mass ratios for two different cuts to the triple sample. The dotted black line matches that of the left panel of Figure \ref{fig:massratio}. The solid blue line represents the sample where all stars which may have experienced LK-driven Roche Lobe overflow are discarded.}
\label{fig:rlof}
\end{figure}

For the purposes of comparison between the different channels, we delineate between Field Binary, Field Triple, Cluster 1G, and Cluster 2G mergers. Cluster 1G mergers are dynamically-assembled mergers which involved only first-generation BHs (those created from stellar collapse), whereas Cluster 2G mergers involve at least one second-generation BH. We do not distinguish between binary and triple mergers in clusters, as the triple companion was shown to have minimal effect on both the mass and mass ratio distribution \citep{MartinezFragione2020}.

In Figure \ref{fig:massratio}, we compare the mass ratio ($q=m_2/m_1$ for $m_1>m_2$) distributions of BH mergers events from the four populations. On the left side, we show the field (cluster) population weighted by star (cluster) formation history. On the right, we further weight the populations by detectability. On the left side, we also show the power law model (with an arbitrary normalization) for $q$ from the \textsc{Power Law + Peak} model ($\beta_q=1.3^{+1.6}_{-1.3}$) fits from GWTC-2 \citep{lvc2020catb} with the purple line and shaded purple band. Using the \textsc{Broken Power Law} model ($\beta_q=1.4^{+1.7}_{-1.4}$) instead of the \textsc{Power Law + Peak} model gives nearly identical results.

We find that the mass ratio distribution for the field binaries here agree well with previous results \citep[e.g.,][]{Zevin2020}. The cluster 1G and 2G distributions are both shaped by binary-mediated dynamical interactions in the cores of dense stellar systems, which will typically exchange lower-mass components of binaries in favor of producing equal mass BBHs \cite[e.g.,][]{1993ApJ...415..631S}. Thus, there is a preference for equal mass mergers in the 1G case and for mergers with $q\sim0.5$ in the 2G case, as the heaviest BH in the cluster, typically the remnant of a 1G merger, will be roughly twice the mass of the next heaviest BH. Remarkably, we find that the mass ratio distribution for triples is largely flat between roughly 0.3 and 1.0.  This is particularly true compared to binaries, which means that--given the same initial conditions--the LK mechanism preferentially enhances the merger rate of lower mass ratio systems. \cite{2021arXiv210301963S} demonstrated that octupole-order effects in hierarchical triple evolution cause the merger fraction to increase as the mass ratio of the inner binary is decreased. As a result, the mass ratio distribution produced through this channel produces low mass ratio mergers compared to the isolated binary channel when using self-consistent initial conditions. Furthermore, we find that this mass ratio distribution is the one that most closely tracks the inferred distribution function from GWTC-2 \citep{lvc2020catb}. Going from the astrophysical population to the detectable population, many of the same general trends are present, though all the distributions are slightly biased towards equal mass ratios.

In Figure \ref{fig:mtot_q}, we present the same mass ratio distributions as above against the total binary masses of each merging system as contour plots, where we show the regions containing 60\% (dotted), 90\% (dashed), and 99.5\% (solid) of the sample. The left column shows the astrophysical population and the right shows the detectable population. In each row, we compare the field triple populations (black contours) to the field binary (red contours), cluster 1G (yellow contours), and cluster 2G (green contours) populations. We also include in the right column in each row GW190412 \citep{theligoscientificcollaboration2020}.

Many of the general features from Figure \ref{fig:massratio} are also present here, such as the large number of triple mergers with low mass ratios. In the top row, we show that when comparing mergers with $q\lesssim0.5$, triple mergers tend to have a higher total binary mass compared to the field binary mergers, with the center of the total mass ratio distribution at $\sim50-60\msun$ for triples, whereas binaries appear to always have total mass less than $\sim40\msun$. In the middle row, this observation still roughly holds when comparing the field triple and cluster 1G mergers, where it is clear that the mergers produced by the triple channel tend to have a lower mass ratio. Finally, the bottom row demonstrates that the peak of the cluster 2G distribution nearly occupies the same portion of $M_{\rm tot}-q$ space as the field triples. However, note that if BHs are born with negligible spin \citep{Fuller2019a}, as is assumed in this study and in the GC models \citep{Kremer2020}, then these two populations will be easily distinguished by the spins of the components, since the primary 2G BH should have a spin $\chi\sim0.7$. If BHs are born with significant ($\chi \gtrsim 0.2$) spins from stellar collapse, then the relative contribution of hierarchical mergers from GCs will be greatly diminished \citep[e.g.,][]{Rodriguez2019,FragioneLoeb2020b}. Finally, we observe that GW190412 is consistent (with $99\%$ confidence) with either an isolated triple or 2G origin based solely on its position in $m_{\rm tot}-q$ space. The detection announcement of GW190412 also reported a confident detection of the spin of the primary BH $\chi_1=0.44_{-0.22}^{+0.16}$ while the spin of the secondary BH is largely unconstrained \citep{theligoscientificcollaboration2020}. If BHs are born with high spin, then by the logic above, our models would suggest an isolated triple origin is a more likely explanation between the two.

As stated previously, we found that the majority of merging binaries undergo at least one common envelope phase, whereas only $0.1\%$ merging triples do. In the top panel of Figure \ref{fig:a1i}, we show the median and 50 percentile of the initial mass ratio distribution of our sample as a function of semi-major axis. We show in the bottom panel the distribution of ZAMS inner semi-major axis for our total initial sample (solid blue), as well as the ZAMS inner semi-major axis of the systems that merge as a binary (dash-dotted red) and as a triple (dashed green). In the bottom panel, it can be seen that the two merging populations sample different areas of the initial inner semi-major axis distribution, which also have different initial mass ratios. Whereas the merging binaries tend to have smaller initial semi-major axes, with a very apparent enhancement at $\sim0.1\,\rm{au}$, the triples have a much larger range of initial semi-major axes. Accordingly, the merging triples tend to have smaller initial mass ratios than the binaries. These different mass ratio distributions are then sculpted by further binary stellar evolution and these subtle differences are further amplified, most notably through common envelope phases. In our sample, only a single triple system experienced a common envelope phase, whereas the majority of the binaries ($77.6\%$) experience a common envelope phase.

In this study we considered only the useful triples. In principle, it is possible that the "non-useful" triples, or those whose inner binary would have merged regardless of the tertiary companion, could still enhance the rate of triple mergers within the local Universe. We find that $15.3\%$ of the binary mergers take place within a stable triple system. However, only $0.03\%$ of these mergers take place in a triple system in which the LK mechanism would not be quenched due to relativistic pericenter precession \citep[see also Figure 4 of][]{Rodriguez2018a}. As a result, we expect that these non-useful triples would account for at most an additional few percent of triple mergers where the LK mechanism allows for a substantial decrease in the delay time. Furthermore, in this study we only considered stable triples where all three components are BHs. We found that, for triples (both useful and non-useful) where the inner binary was composed of two BHs, about $2/3$ of the triples had a BH as the outer companion. While a detailed treatment is outside of the scope of this work due to the possibility of mass transfer from the outer companion \citep[e.g.][]{distefano2020}, assuming a comparable merger fraction for the non-BH companions leads to a roughly 50\% increase in the number of triple mergers.

While our approximate technique for modeling hierarchical triples can track the evolution of the triple configuration due to mass loss, supernova, and the evolution of the inner binary, it does not allow for the possibility of LK oscillations during the main sequence.  As a result, it is possible that many of the systems presented here may actually have merged prior to their formation as BH triples.  However, we can estimate the effect this missing physics may have on our results.  In order to explore the sensitivity of our results to LK oscillations during the main sequence and giant phases, we calculated the minimum pericenter distance of each of the inner binaries of the triples attainable due to LK \citep[by numerically solving Eq.~2 of][]{Liu+2019} from their zero-age main sequence initial conditions.  We then compared these separations to the distance required for each star to fill its Roche lobe \citep[Eq.~2 of][]{Eggleton83}, assuming all the stars acquired an average maximum radius of $500\rsun$ \citep[e.g.,][]{Agrawal+2020}, and discarded any systems that would have passed within their Roche lobe separation. We find that $19.3\%$ of the systems survive this cut. The resulting change to the mass distribution is illustrated in Figure \ref{fig:rlof}, where the additional constraint produces an even flatter mass ratio distribution than our original results. This is to be expected, since excluding systems which may have undergone binary interactions or mergers will also preferentially select the ultra-wide triples illustrated in Figure 3, which we show are more likely to have a smaller mass ratio.

\section{Conclusions}
\label{sect:concl}

In this Letter, we started from a sample of triple massive stellar systems and evolved them to their end state as BH triples, in order to obtain a self-consistent comparison between the binary and triple channels. We also compared this population with a population of mergers from previous studies studying BBHs in dense stellar clusters which used the same assumptions for stellar evolution \citep{Kremer2020}.

We report that the mass ratio distribution from the isolated triple systems in our sample produce a BBH mass ratio distribution that is nearly flat from unity to $\sim0.3$, producing significantly more low-mass-ratio mergers than either isolated binary evolution of dynamical formation of BBHs. Furthermore, we show that the triple channel seems to agree with the power law implied by the most recent catalog of GW observations better than other channels. As a result, the triple channel may be able to more efficiently produce events with low mass ratios such as GW190412.

However, our results do not suggest that triple channel is able to reproduce the whole catalog of observed events. We simply assert that if isolated BH triple systems are produced in nature, then we may be able to gauge the contribution of the LK mechanism to the total population of merging BH systems by low mass ratio and high total mass. This is in addition to other means of distinguishing LK mergers, such as through eccentricity in the LIGO band or effective spin distribution \citep[e.g.,][]{Antonini2012,Antonini2017,Liu2017,Liu2018,Rodriguez2018c,fk2020}.

Apart from the mass ratio distributions, it is important to quantify the relative contribution of the triple channel to the total BBH merger rate.  While a complete estimate of the BBH merger rate is beyond the scope of this Letter, we can approximate the rate by multiplying the ratio of triple BBH mergers to binary BBH mergers using our initial conditions ($0.003$) by the volumetric merger rate at $z=0$ using the same physics and (binary) initial conditions from the literature \citep[$\sim 1.6\times10^3 \gpcyr$,][]{Zevin2020}.  This suggests a local triple merger rate of $\sim5 \gpcyr$, consistent with previous estimates of $0.02-25 \gpcyr$ \citep[e.g.][]{Silsbee2017,2017ApJ...841...77A,Rodriguez2018a,flp2019}.  The initial conditions and common envelope physics used in \cite{Zevin2020} clearly produce extremely unrealistic volumetric rates for BBH mergers (up to two orders of magnitude larger than the observed rate of $23.9^{+14.3}_{-8.6} \gpcyr$ \citep{lvc2020catb}), meaning our ratio of triple to binary mergers may similarly be a significant underestimate.\footnote{For comparison, the BBH merger rate predicted for the clusters presented in this work is roughly $17 \gpcyr$ \citep[][]{2021RNAAS...5...19R}}. As stated previously, the majority of the binary systems experienced a common envelope phase whereas only a single triple system did. Thus, while the binary channel is heavily influenced by uncertainties in the common envelope physics, the triple channel is not.

As the number of GW observations continues to grow, it will become much easier to distinguish between different merger formation channels. We have shown the potential for future observations to constrain the importance of hierarchical triples to the cumulative BH merger rate given the efficiency of producing high total mass, low mass ratio events. We leave it to a future study to probe the sensitivity of these conclusions to different assumptions, such as those concerning binary evolution or accounting for mass transfer from the tertiary companion.

\software{\texttt{numpy} \citep{walt_numpy_2011}, \texttt{scipy} \citep{2020SciPy}, \texttt{matplotlib} \citep{hunter_matplotlib:_2007}, \texttt{COSMIC} \citep{2020zndo...3905335B}}

\acknowledgments

We thank Kyle Kremer, Scott Coughlin, Michael Zevin, Max Moe, and Rosanne Di Stefano for useful discussions and suggestions. We thank Kyle Kremer for providing the cluster models used in this work. Computations were supported in part through the resources and staff contributions provided for the Quest high performance computing facility at Northwestern University, which is jointly supported by the Office of the Provost, the Office for Research, and Northwestern University Information Technology. This work also used computing resources at CIERA funded by NSF Grant PHY-1726951 and computing resources provided by Northwestern University and the Center for Interdisciplinary Exploration and Research in Astrophysics (CIERA).

\bibliographystyle{aasjournal}


\section{Formalized Weihrauch analysis}
The following development of formalized Weihrauch reducibility draws from
work of Hirst and Mummert \cite{hm}.  Like them, we work in $i {\sf RCA}_0^\omega$, Kohlenbach's \cite{k2001}
higher order axiomatization for reverse mathematics, restricted to intuitionistic logic.
Informally, we may view $i{\sf RCA}_0^\omega$ as an axiomatization of intuitionistic arithmetic that can
prove the existence of computable functions and computable functionals.  For more
details of the axiomatization, see \cite{hm}.

We formalize a Weihrauch problem with a formula
$\forall x ( p_1 (x) \to \exists y\, p_2 (x,y))$ where $p_1(x)$ indicates that $x$ is an accepted input
and $p_2 (x,y)$ indicates that $y$ is a solution of $x$.  Here $y$ may be a function, set, or number,
depending on the problem.  For total problems, that is, those problems accepting all sets as inputs,
we can use the more simple representation $\forall x \exists y \, p(x,y)$.

Some of the results connecting provability and formalized Weihrauch reducibility are restricted
to a family of formulas called $\Gamma_1$ by Troelstra~\cite{troelstra}.
A formula is {\em $\exists$-free} if it is built from atomic formulas using only universal quantification
and the connectives $\land$ and $\to$.
(Troelstra includes $\bot$ as an atomic formula, so $\neg P$ abbreviates $P \to \bot$.)
The collection $\Gamma_1$ consists
of those formulas defined inductively by the following:
\begin{list}{$\bullet$}{}
\item  All atomic formulas are elements of $\Gamma_1$.
\item  If $A$ and $B$ are in $\Gamma_1$, then so are $A \land B$, $A \lor B$,
$\forall x A$, and $\exists x A$.
\item  If $A$ is $\exists$-free and $B$ is in $\Gamma_1$ then $\exists x A \to B$ is in $\Gamma_1$,
where $\exists x$ denotes a block of zero or more existential quantifiers.
\end{list}

\begin{definition}
Suppose ${\sf P}{\rm :}\forall x (p_1 (x) \to \exists y \, p_2 (x,y))$ and ${\sf Q}{\rm :}\forall u (q_1 (u) \to \exists v \, q_2 (u,v))$ are problems.  The reduction prenex formula for ${\sf Q} \le_{W} {\sf P}$
is the formula:
\[
S^{\sf P}_{\sf Q}:
\forall u \exists x \forall y \exists v ( q_1(u) \to ( p_1 (x) \land (p_2 (x,y ) \to q_2 (u,v) ) ) )
\]
If the problems are total, we can write $\sf P$ as
$\forall x \exists y \, p(x,y)$, $\sf Q$ as $\forall u \exists v \, q(u,v)$ and $S^{\sf P}_{\sf Q}$ as
$\forall u \exists x \forall y \exists v ( p(x,y) \to q(u,v))$.
\end{definition}

The implication $S^{\sf P}_{\sf Q} \to ({\sf P} \to {\sf Q})$ is provable in intuitionistic predicate calculus,
though the proof of the converse requires classical logic.  If the constituent formulas
$p_1$, $p_2$, $q_1$, and $q_2$ are all $\exists$-free, then the matrix of $S^{\sf P}_{\sf Q}$
is also $\exists$-free and $S^{\sf P}_{\sf Q}$ is in $\Gamma _1$.  This also holds for total problems.

If $\sf P$ and $\sf Q$ are Weihrauch problems, we can formalize ${\sf Q} \le_{W} {\sf P}$ by asserting
the existence of Skolem functions for the existential quantifiers of $S^{\sf P}_{\sf Q}$.
Using $\sf P$ and $\sf Q$ as in the definition, the relation ${\sf Q} \le_{W} {\sf P}$ can be
translated into the language of $i{\sf RCA}_0^\omega$ as:
\[
\exists \Phi \exists \Psi \forall u \forall y
(q_1(u) \to (p_1 (\Phi(u))\land(p_2 (\Phi(u),y)\to q_2 (u, \Psi(y)))))
\]
Here the functionals $\Phi$ and $\Psi$ are of type $1\to1$, which is our primary motivation
for working in higher order subsystems.

Using the preceding notation, we can present the following slightly modified version
of Theorem 1 of Hirst and Mummert \cite{hm}.

\begin{theorem}\label{hm1}
Suppose $\sf P$ and $\sf Q$ are problems and
the reduction prenex formula
$S^{\sf P}_{\sf Q}$  is in $\Gamma_1$.
Then $i{\sf RCA}_0^\omega\vdash S^{\sf P}_{\sf Q}$ if and only if
$i{\sf RCA}_0^\omega \vdash {\sf Q} \le_{W} {\sf P}$.
\end{theorem}

\begin{proof}
The result follows from the application of Kohlenbach's \cite{kbook} proof mining technology
to extract terms corresponding to the Skolem functions.
Only one modification to the proof of Theorem 1 of Hirst
and Mummert \cite{hm} is needed.  The hypothesis of their theorem specifies that
the matrix of $S^{\sf P}_{\sf Q}$ is in $\Gamma_1$, which by the definition of
$\Gamma_1$ is equivalent to $S^{\sf P}_{\sf Q} \in \Gamma_1$.
\end{proof}

The following theorem is the intuitionistic analog of a conservation result
of Kohlenbach \cite{k2001}.

\begin{theorem}\label{cons}
The system $i{\sf RCA}_0^\omega$ is conservative over $i{\sf RCA}_0$ for second order formulas.
\end{theorem}

\begin{proof}
Kohlenbach's conservation result for ${\sf RCA}_0^\omega$ over ${\sf RCA}_0$ appears
as Proposition 3.1 in his article on higher order reverse mathematics \cite{k2001}.
Kohlenbach's proof is based on the formalization of the extensional model
of the hereditarily continuous functionals (ECF) as presented in
Section 2.6.5 of Troelstra's book \cite{troelstra}.  The arguments of
Troelstra (e.g.~2.6.12 and 2.6.20 of \cite{troelstra}) are carried out
in intutionistic systems.  Similarly, Kohlenbach's proof holds for $i{\sf RCA}_0^\omega$ and $i{\sf RCA}_0$.
For other related discussion, see Theorem 2.7
and Theorem 2.8 of Hirst and Mummert \cite{hmunif}.
\end{proof}

\subsection{Local graph coloring}\label{section2}

The following encoding of graphs is useful in exploring graph coloring problems.
We can view a countable infinite graph as having $\mathbb N$ as its vertex set.
Fix a primitive recursive bijective pairing function, $p$, mapping $\mathbb N$ onto $\{ (a,b) \mid a< b\}$, the
subset of $\mathbb N \times \mathbb N$ consisting of increasing pairs.  Both $p$ and $p^{-1}$ can be
defined in such a way that $i{\sf RCA}_0^\omega$ proves their existence and salient properties.
Using this pairing function, any function $e : \mathbb N \to \mathbb N$ can be viewed as a characteristic
function for the edge set of a graph $G$.  If $e(n) \neq 0$ then the edge $p(n)$ is in $G$,
and if $e(n) = 0$ then $p(n)$ is not in $G$.  We will conflate $G$ with the set of
codes for the edges of $G$ and write $(a,b)\in G$ as a shorthand for
$e(p^{-1} (a,b) ) \neq 0$.

For any graph $G$ and any $m$,
let $G_m$ denote the finite subgraph
with vertices $\{0, \dots , m\}$ and edge set
$\{(a,b) \mid a< b \le m \land (a,b)\in G \}$.
We say that $G_m$ has a $k$-coloring if there is a finite function
$f:m\to k$ such that for all $a <b\le m$, $(a,b) \in G$ implies $f(a) \neq f(b)$.
Informally, vertices connect by an edge must have distinct colors.
The existence of $k$-colorings for (initial) finite subgraphs can be
formulated as a problem.

\begin{dLGk}
(Local $k$-coloring for graphs):  Fix $k$.
For a graph $G$ (encoded by a characteristic function for its edge set), there
is a value $\lgk{k}(G)$ such that $\lgk{k}(G)=0$ implies that for every $m$ the subgraph
$G_m$ has a $k$-coloring, and $\lgk{k}(G)=m>0$ implies that
$G_m$ has no $k$-coloring and $G_{m-1}$ has a $k$-coloring.
\end{dLGk}

Let $c(G,m)$ denote a primitive recursive function such that
$c(G,m) = 1$ if $G_m$ has a $k$-coloring and $c(G,m)=0$ if $G_m$ has no
$k$-coloring.  Using this function, we can formalize the predicate $\lgk{k}(G)=n$
as the following $\exists$-free formula,
\[
\begin{split}
(n=0 \to \forall m (c(G,m) = 1) )\land & \\
(n>1 \to  (c(G,n)= & 0 \land \forall t (t<n \to c(G,t)=1)))
\end{split}
\]
and note that $\lgk{k}$ is a total problem of the form
$\forall G \exists n ( \lgk{k}(G) = n )$.
We will compare $\lgk{k}$ to a version of the limited principle of omniscience.

\begin{dLPO}
(Limited principle of omniscience):  For every $p: \mathbb N \to \mathbb N$ there is a value
${\sf{LPO}} (p)$ such that ${\sf{LPO}} (p) = 0$ implies that $\forall k ~p(k)>0$, and
${\sf{LPO}} (p) =m>0$ implies that $p(m-1) = 0$ and for all $t<(m-1)$, $p(t) > 0$.
\end{dLPO}

We can formalize the predicate ${\sf{LPO}}(p)=n$ as the following $\exists$-free formula,
\[
(n=0 \to \forall k ( p(k) > 0 ))\land (n>0 \to (p(n-1)=0 \land \forall t(t<(n-1)\to p(t)>0)))
\]
and note that ${\sf{LPO}}$ is a total problem of the form $\forall p \exists n ({\sf{LPO}}(p)=n )$.
This version of ${\sf{LPO}}$ differs from that presented in the survey by
Brattka, Gherardi, and Pauly \cite{bgp}.  It is Weihrauch equivalent to their version,
but not strongly Weihrauch equivalent, as the range of their version includes only $\{0,1\}$
and the range of this version includes all of $\mathbb N$.  However, for our purposes it is desirable
to have the underlying predicate be $\exists$-free.

\begin{lemma}\label{LGL}
$( i{\sf RCA}_0^\omega )$
For each $k \ge 1$, both $S^{\lgk{k}}_{\sf{LPO}}$ and $S^{\sf{LPO}}_{\lgk{k}}$ hold.
\end{lemma}

\begin{proof}
Because both ${\sf{LPO}}$ and $\lgk{k}$ are total, we can use the simple form of the
reduction prenex formula.  Thus $S^{\lgk{k}}_{\sf{LPO}}$ is
\[
\forall p \exists G \forall y \exists v (\lgk{k}(G) = y \to {\sf{LPO}}(p) = v).
\]
To prove this in $i{\sf RCA}_0^\omega$, fix an instance $p$ of ${\sf{LPO}}$.  Define the graph $G$ as follows.
For each $m$, if $p(m) =0$, add the edges
$\{(s,t) \mid m\le s< t \le m+k\}$ to $G$.  These edges form a complete subgraph on
$k+1$ vertices, precluding any $k$-coloring of $G_{m+k}$.  If $p(m) \neq 0$, add no new edges
to $G$.  By this construction, if $\lgk{k}(G) = 0$, then for all $m$, $p(m) >0$, so ${\sf{LPO}} (p) = 0$.
On the other hand, if $\lgk{k}(G) = m >0$, then $m=n+k$ for some $n\ge 0$, and $p(n)=0$,
so ${\sf{LPO}}(p)=n+1=m-k+1$.

To show that $S^{{\sf{LPO}}}_{\lgk{k}}$, fix a graph $G$.  Define an instance $p$ of ${\sf{LPO}}$ as follows.
For each $m$, if the subgraph $G_m$ has a $k$-coloring, let $p(m) = 1$.  If $G_m$ has no $k$-coloring,
let $p(m) = 0$.  The truncated subtraction ${\sf{LPO}} (p)\frac{\cdot}{~~} 1$ yields a correct output for $\lgk{k}(G)$.
\end{proof}

By formalizing the transitivity of Weihrauch reduction we can extract additional results from the preceding lemma.

\begin{lemma}\label{TRANS}
$(i{\sf RCA}_0^\omega )$  If $ {\sf P} \le_{W} {\sf Q}$ and ${\sf Q} \le_{W} {\sf R}$, then ${\sf P} \le_{W} {\sf R}$.
\end{lemma}

\begin{proof}
This is a formalization of the well-known property for Weihrauch reductions.  The
system $i{\sf RCA}_0^\omega$ can prove that compositions of given functionals exist, so the usual
proof holds.
\end{proof}

\begin{theorem}\label{LGT}
$(i{\sf RCA}_0^\omega )$  For any $j \ge k \ge 1$, ${\sf{LPO}} \equiv_{W} \lgk{k} \equiv_{W} \lgk{j}$.
\end{theorem}

\begin{proof}
By our formalization of ${\sf{LPO}}$ and $\lgk{k}$, the corresponding predicates are $\exists$-free.
Consequently, both $S^{\lgk{k}}_{\sf{LPO}}$ and $S^{{\sf{LPO}}}_{\lgk{k}}$ are in $\Gamma_1$.
Applying Theorem~\ref{hm1} to the implications of Lemma~\ref{LGL} yields proofs in
$i{\sf RCA}_0^\omega$ that ${\sf{LPO}} \le_{W} \lgk{k}$, $\lgk{k} \le_{W} {\sf{LPO}}$, and so ${\sf{LPO}} \equiv_{W} \lgk{k}$.
This holds for all $j$ and $k$, so by Lemma \ref{TRANS} we have $\lgk{k} \equiv_{W} \lgk{j}$.
\end{proof}

One noteworthy consequence of the preceding theorem is the provability of the Weihrauch equivalence
of $\lgk{2}$ and $\lgk{3}$ in $i{\sf RCA}_0^\omega$.  The finite combinatorial analogs of these problems are
2-colorability and 3-colorability of finite graphs, which are respectively polynomial time computable
and NP complete.  As was the case in the traditional reverse mathematics and computability
theoretic analysis of Hirst and Lempp \cite{hl}, formal Weihrauch
analysis of the related infinite problems does not distinguish between these problems.
The current setting does allow us to apply techniques of Weihrauch analysis, like the
application of Lemma~\ref{TRANS} in the preceding proof to obtain formal equivalences,
and then to translate these into proofs of implications in weak subsystems, as in the following
corollary.

\begin{corollary}\label{LGC}
$(i{\sf RCA}_0^\omega)$  For every pair of problems $\sf P$ and $\sf Q$ from the list in Theorem \ref{LGT},
$S^{\sf P}_{\sf Q}$ holds.  Furthermore, the implication ${\sf P}\to {\sf Q}$ holds.
\end{corollary}

\begin{proof}
As noted above, the formulas $S^{\sf P}_{\sf Q}$ of Theorem~\ref{LGT}
are in $\Gamma_1$.  Applying the reverse implication Theorem~\ref{hm1} to the equivalences of Theorem~\ref{LGT}
proves  $S^{\sf P}_{\sf Q}$.  To justify the final sentence, note that these are total problems and can be written
as $\Pi^1_1$ formulas.  Over intuitionistic predicate calculus, $S^{\sf P}_{\sf Q}$ implies ${\sf P}\to {\sf Q}$.
\end{proof}

If $\sf P$ is a problem, the parallelization of $\sf P$, denoted by $\widehat{\sf P}$ is the problem
that accepts as input any infinite sequence of inputs for $\sf P$, and outputs the associated infinite
sequence of solutions for the input instances.  The following lemma is a formalization of a portion
of part 3
of Proposition 3.6 of Brattka, Gherardi, and Pauly \cite{bgp}.

\begin{lemma}\label{HAT}
$( i{\sf RCA}_0^\omega )$  ${\sf P} \le_{W} {\sf Q}$ implies $\widehat{\sf{P}}\le_{W} \widehat{\sf{Q}}$.
\end{lemma}

\begin{proof}
Suppose that $\Phi$ and $\Psi$ are the functionals witnessing ${\sf P} \le_{W} {\sf Q}$.
If $\vec u = \langle u_i \rangle_{i \in \mathbb N}$ is an input for $\widehat{\sf Q}$, define
$\hat \Phi$ by $\hat \Phi (\vec u) = \langle \Phi (u_i) \rangle_{i \in \mathbb N}$.  Define
$\hat \Psi$ similarly.  Note that $i{\sf RCA}_0^\omega$ suffices to prove the existence of $\hat\Phi$
and $\hat \Psi$, and also proves that they witness $\widehat{\sf{P}}\le_{W} \widehat{\sf{Q}}$.
\end{proof}

\begin{theorem}\label{GHW}
$( i{\sf RCA}_0^\omega )$  For every $k \ge 1$, $\widehat{\sf{LPO}} \equiv_{W} \widehat{\lgk{k}}$.
\end{theorem}

\begin{proof}
Apply Lemma \ref{HAT} to Theorem \ref{LGT}.
\end{proof}

If $\langle f_i \rangle_{i \in \mathbb N}$ is a sequence of input functions for $\widehat{\sf{LPO}}$, we can
define a type 1 function on (codes of pairs of) natural numbers by $f(i,n) = f_i(n)$ and think of $f$ as a type 1 input for $\widehat {\sf{LPO}}$.  This modification
allows us to think of $\widehat {\sf{LPO}}$ as a $\Pi^1_2$ formula of second order arithmetic.
Similarly, we will conflate $\widehat {\lgk{k}}$ with its second order analog.

\begin{corollary}\label{GHRM}
$(i{\sf RCA}_0 )$ The following are equivalent:
\begin{enumerate}
\item ${\sf ACA}_0$. \label{GHRM1}
\item $\widehat{{\sf{LPO}}}$\label{GHRM2}
\item $\widehat{\lgk{k}}$, where $k\ge 1$.\label{GHRM3}
\end{enumerate}
\end{corollary}

\begin{proof}
The equivalence of parts (\ref{GHRM2}) and (\ref{GHRM3}) follows from
the application of Theorem \ref{hm1} to the Weihrauch reductions included in Theorem \ref{GHW}, and the
fact that $S^{\sf P}_{\sf Q} \to ({\sf P} \to {\sf Q})$.  To show that
(\ref{GHRM1}) implies (\ref{GHRM2}), let $\langle f_i \rangle_{i \in \mathbb N}$ be
an input for $\widehat{{\sf{LPO}}}$.  Arithmetical comprehension asserts the
existence of the set $\{ i \mid \forall n \, f_i(n) \neq 0 \}$ and the
corresponding characteristic function, which is a solution of the instance of $\widehat{{\sf{LPO}}}$.

To show that (\ref{GHRM2}) implies (\ref{GHRM1}), we adapt the familiar
application of Lemma III.1.3 of Simpson \cite{simpson}.  In $i{\sf RCA}_0$ it suffices to
find the range of an arbitrary function that is injective, except for possibly repeatedly
taking the value $0$.  (This broader class of almost injective functions avoids a use of classical
logic in the proof of Lemma II.3.7, used by Simpson \cite{simpson} to prove the reversal.)
Let $f$ be such a function.
Define the sequence of functions $\langle f_i \rangle_{i \in \mathbb N}$ by
$f_i(m) = 1$ if $\forall t< m (f(t) \neq i)$ and $f_i (m) = 0 $ otherwise.
The solution to the $\widehat{{\sf{LPO}}}$ problem $\langle f_i \rangle_{i \in \mathbb N}$
is the characteristic function of the range of $f$.

Finally, the formulas of Corollary~\ref{GHRM} are all second order, so by Theorem~\ref{cons}
the equivalences are provable in the second order system $i{\sf RCA}_0$.
\end{proof}

Summarizing, we used higher order formalized Weihrauch techniques in Lemma \ref{HAT}
and extracted traditional second order reverse mathematics results in Corollary \ref{GHRM}.

\subsection{Colorings as outputs}

We can reformulate the graph coloring problems so that the outputs are infinite graph colorings.
We will continue to use the notation of the previous subsection.  In particular, $G_m$ denotes the finite
subgraph of $G$ consisting of the first $m+1$ vertices and their edges in $G$.

\begin{dGCk}
($k$-coloring of graphs):
If $e:\mathbb N \to \mathbb N$ codes the edge set for a graph $G$ and every finite
subgraph $G_m$ has a $k$-coloring, then there is a function $f: \mathbb N \to k$
that is a $k$-coloring of $G$.
\end{dGCk}

The predicate asserting that $G_m$ is $k$-colorable can be written using bounded quantifiers, with
$G$, $k$, and $m$ as parameters.  The system $i{\sf RCA}_0^\omega$ proves the existence of the primitive recursive
characteristic functional for this predicate, so the assertion that every $G_m$ has a $k$-coloring can
be formalized with a $\exists$-free formula.  Note that $f$ is a $k$-coloring of $G$ if and only if
for each $i \neq j$, if $(i,j)$ is an edge in $G$ then $f(i)\neq f(j)$, which is also $\exists$-free.
Thus we can write an $\exists$-free formula ${\sf{GC}}k(G,f)$ asserting that $f$ is the solution
to the ${\sf{GC}}k$ problem for $G$.

In our study of problems involving infinite trees, we will use the the following encoding.
Fix a suitable bijective coding function ${\sf seq}$ mapping $\mathbb N$ onto $2^{<\mathbb N}$, the set
of finite sequences of zeros and ones.  Any function $t: \mathbb N \to \mathbb N$ can be viewed as
a code for a binary tree $T$ using the following convention.  The finite sequence ${\sf seq} (n)$ is
in $T$ if and only if $t(n)>0$ and for every initial segment $\sigma$ of ${\sf seq} (n)$,
$t({\sf seq}^{-1} (\sigma) )>0$.  Informally, the function $t$ is the characteristic function for a
set that includes the sequences of $T$ and omits the immediate successors of any leaves of $T$.
Using this encoding, we have the following formalization of Weak K\"o{}nigs's Lemma as a total
problem.

\begin{dWKL}
(Weak K\"o{}nig's Lemma):
If $T$ is a binary tree and for every $m$ there is a sequence $\sigma \in T$ of length $m$,
then there is a function $p$ that codes an infinite path through $T$.
\end{dWKL}

In the previous formalization, $p$ can be viewed as
a code for a subtree $P$ of $T$ such that each node in $P$ has precisely one immediate successor.
Using our standard techniques for representing primitive recursive functionals, it is easy to
formalize the assertion that for every $m$ the tree $T$ contains a binary sequence of length
$m$ as an $\exists$-free formula.  Note that the bound on the labels is essential for this.
The claim that $p$ is an infinite path is a universal statement, so we can write an $\exists$-free
formula ${\sf{WKL}}(T,f)$ asserting that $f$ is a solution to the $\sf{WKL}$ problem for $T$.

For values of $n$ greater than $2$, we can use a bijective coding ${\sf seq} _n$ of sequences of numbers
less than $n$, and formulate a corresponding version of ${\sf WKL}$.

\begin{dWKn}
(Weak K\"o{}nig's Lemma for trees in $n^{<\mathbb N}$):
If $T$ is a tree with nodes labeled with numbers less than $n$,
and for every $m$ there is a sequence $\sigma \in T$ of length $m$,
then there is a function $p$ that codes an infinite path through $T$.
\end{dWKn}

Note that ${\sf WKL}$ and $\wkn{2}$ denote the same problem.  As with ${\sf WKL}$, we can formalize
$\wkn{2}$ in the language of $i{\sf RCA}_0^\omega$ with an $\exists$-free formula.

\begin{lemma}\label{GCL0}
$(i{\sf RCA}_0)$ For each $n\ge 2$,  $S^{{\sf WKL}}_{{\sf WKL} n}$ and $S^{{\sf WKL} n}_ {{\sf WKL}}$ hold.
\end{lemma}

\begin{proof}
For $n\ge 2$, every binary tree is an $n$-ary tree, so $S^{{\sf WKL} n}_ {{\sf WKL}}$ holds trivially.
To prove $S^{{\sf WKL}}_{{\sf WKL} n}$, let $T$ be an $n$-ary tree.  Any sequence of $m$ values less
than or equal to $n$ can be mapped to a binary sequence of length $m\cdot n$ in the manner of
the following example.  Consider $\langle 2, 0 , 3 \rangle$ as a sequence of numbers less than or equal to $3$.
Replace each value $k$ with a block of length $3$ consisting of $k$ ones padded on the right with zeros.
In our example $\langle 2, 0 , 3 \rangle$ becomes $\langle 1,1,0, \,\, 0,0,0,\,\, 1, 1, 1\rangle$.  This
process transforms any $n$-ary tree $T$ into a binary tree that is well-founded if and only if $T$ is.
Furthermore, summing successive length $n$ blocks of any infinite path through the binary tree yields a path
through $T$.
\end{proof}

We will use the following formalization
of ${\sf LLPO}$, which is defined for all functions from $\mathbb N$ into $\mathbb N$.
 Na\"i{}vely, if a function $p$ has a positive value, then ${\sf LLPO}$ returns
 the flip of the parity of that first positive value.

 \begin{dLLPO}(Lesser limited principle of omniscience):
For any $p:\mathbb N \to \mathbb N$
there is a value ${\sf LLPO} (p)$ such that
${\sf LLPO} (p)=0$ implies if $p(j) \neq 0$ and $\forall t< j (p(j)=0)$ then $j$ is odd, and
${\sf LLPO} (0) \neq 0$ implies ${\sf LLPO}(p) =1$ and if $p(j) \neq 0$ and $\forall t< j (p(j)=0)$ then $j$ is even.
\end{dLLPO}

Our definition is chosen so that for functions $p$ with ranges that are non-zero
in at most one place, the value of ${\sf LLPO} (p)$ matches the
definition of Brattka, Gherardi, and Pauly \cite{bgp}*{\S7.2}.
By mapping functions from $\mathbb N$ to $\mathbb N$ to the characteristic function for the
least element of their domain taking a positive value, routine verification shows
that our total version of ${\sf LLPO}$ is strongly Weihrauch equivalent to their version.

The predicate ``$j$ is odd'' can be formalized by $\forall m (j \neq 2m)$.  Similarly,
``$j$ is even'' can be formalized by $\forall m (j \neq 2m+1 )$.  Consequently,
${\sf LLPO} (p) =n$ can be formalized by the $\exists$-free formula:
\begin{align*}
&( n=0  \to
\forall j ([p(j)\neq 0 \land \forall t (t<j \to p(t)=0)] \to \forall m (j \neq 2m))) \land \\
&( n\neq 0 \to
(n=1 \land \forall j( [p(j)\neq 0 \land \forall t (t<j \to p(t)=0)] \to \forall m (j \neq 2m+1)))
)
\end{align*}

The problem ${\sf LLPO}$ can be parallelized, resulting in a problem that is
Weihrauch equivalent to ${\sf WKL}$, as noted in part of
Theorem 7.23 of
Brattka, Gherardi, and Pauly \cite{bgp}.
The following results lead to a formalization of a fragment of their theorem,
and its connection to graph colorings.

\begin{lemma}\label{BGP}
$(i{\sf RCA}_0 )$  $S^{\sf \widehat{\sf LLPO}}_{\sf {\sf WKL}}$ holds
\end{lemma}

\begin{proof}
To prove $S^{\widehat{\sf LLPO}}_{{\sf WKL}}$, suppose $T$ is a binary tree.  For every $\sigma \in 2^{<\mathbb N}$, define
the instance $p_\sigma$ of ${\sf LLPO}$ as follows.  If $\sigma \notin T$, then for each $n$,
$p(n) = 0$.  For $\sigma \in T$, let $p_\sigma (0) = p_\sigma (1) = 0$.
For $n> 0$, define $p_\sigma (2n)$ and $p_\sigma (2n+1 )$ as follows.
If $\sigma {^\smallfrown} 0$ has an extension of length $n$ in $T$ and $\sigma {^\smallfrown} 1$ has
no extension of length $n$ in $T$, let $p_\sigma (2n) = 0$ and $p_\sigma (2n+1 ) = 1$.
If $\sigma {^\smallfrown} 1$ has an extension of length $n$ in $T$ and $\sigma {^\smallfrown} 0$ has no
extension of length $n$ in $T$, let $p_\sigma (2n) = 1$ and $p_\sigma (2n + 1) = 0$.  Otherwise,
let $p_\sigma (2n) = p_\sigma (2n+ 1) = 0$.

If $\sigma {^\smallfrown} 0$ extends to an infinite path, but $\sigma {^\smallfrown} 1$ does not, then there is a first
$n>0$ such that $\sigma {^\smallfrown} 1$ has no extensions of length $n$.  In this case,
${\sf LLPO} ( p_\sigma ) = 0$.  Similarly, if $\sigma {^\smallfrown} 1$ extends to an infinite path but $\sigma {^\smallfrown} 0$
does not, ${\sf LLPO} (p_\sigma ) =1$.  Thus, if $T$ is infinite, the sequence constructed by setting
$\sigma (0) = {\sf LLPO} (\langle\, \rangle )$ and $\sigma (n+1) = \sigma (n) {^\smallfrown} {\sf LLPO} (\sigma (n))$ for
$n \ge 0$ is an infinite path through $T$.
\end{proof}

\begin{lemma}\label{GCL1}
$(i{\sf RCA}_0 )$  $S^{\gck{2}}_{\widehat {\sf LLPO}}$.
\end{lemma}

\begin{proof}
Suppose $p_i$ is an instance of ${\sf LLPO}$.  Construct a subgraph $G_i$ with
vertices $u_i$ and $\{ v_{i,0} , v_{i,1}, \dots\}$ as follows.
For all $k$, include the edge $(v_{i,k}, v_{i,k+1})$.  If $j$ is the least natural number
such that $p_i(j) \neq 0$, add the edge $(u_i , v_{i,j})$.  For any 2-coloring of $G_i$,
if $u_i$ and $v_{i,0}$ differ in color, then $1$ is a correct output for ${\sf LLPO}$.  If $u_i$
and $v_{i,0}$ agree in color, then $0$ is a correct output.  For a sequence of instances
of ${\sf LLPO}$, let $G$ consist of the disjoint union of the graphs for each sequence.
Any two coloring of $G$ yields a solution to the instance of $\widehat {\sf LLPO}$.
\end{proof}

\begin{lemma}\label{GCLm}
$(i {\sf RCA}_0 )$  For $n \ge 2$, $S^{\gck{n}}_{\gck{2}}$.
\end{lemma}

\begin{proof}  Suppose $G$ is a locally $2$-colorable graph.  For $n>2$, create a single
copy of the complete graph on $n-2$ vertices, and connect each of its vertices to every
vertex of $G$.  The new graph is locally $n$-colorable, and the restriction of any $n$-coloring
to the vertices of $G$ yields a $2$-coloring of $G$.
\end{proof}

\begin{lemma}\label{GCL2}
$(i{\sf RCA}_0 )$  For $n \ge 2$, $S^{\wkn{n}}_ {\gck{n}}$ holds.
\end{lemma}

\begin{proof}
For any locally $n$-colorable graph $G$, $i{\sf RCA}_0$ can prove that the tree of
sequences corresponding to $n$-colorings of the finite subgraphs $G_m$ is an instance of $\wkn{n}$.
\end{proof}

We can concatenate the lemmas to yield our main theorem on Weihrauch equivalences related to graph colorings.

\begin{theorem}\label{GCT}
$(i{\sf RCA}_0^\omega )$  For $n\ge 2$, we have:
\[\wkn{n} \equiv_{W} {\sf WKL} \equiv_{W} \widehat{\sf LLPO} \equiv_{W} \gck{n} \equiv_{W} \gck{2}\]
\end{theorem}

\begin{proof}
Applying Theorem \ref{hm1} to Lemma \ref{GCL0} and Lemma \ref{BGP}, we have $\wkn{n} \le_{W} {\sf WKL} \le_{W} \widehat{{\sf LLPO}}$.
Applying Theorem \ref{hm1} to Lemma \ref{GCL1}, Lemma \ref{GCLm}, and Lemma~\ref{GCL2} yields
$\widehat{{\sf LLPO}} \le_{W} \gck{2} \le_{W} \gck{n}\le_{W} {\sf WKL}{n}$.  The theorem follows by transitivity as provided by Lemma \ref{TRANS}.
\end{proof}

Given the formal Weihrauch reductions, we can extract the reverse mathematics consequences.

\begin{corollary}\label{GCC}
$(i{\sf RCA}_0 )$  The formula $S^{\sf P}_{\sf Q}$ holds for every problem $\sf P$ and
problem $\sf Q$ appearing in Theorem \ref{GCT}.  Furthermore the implication ${\sf P} \to {\sf Q}$ holds.
\end{corollary}

\begin{proof}
Imitate the proof of Corollary \ref{LGC}.
\end{proof}

\begin{corollary}\label{GCC2}
$(i{\sf RCA}_0 )$  For $k \ge 2$, the following are equivalent:
\begin{enumerate}
\item  ${\sf WKL}$.
\item  $\widehat {\sf LLPO}$.
\item  $\wkn{k}$
\item  $\gck{k}$.
\end{enumerate}
\end{corollary}

\begin{proof}
Immediate from Corollary \ref{GCC}.
\end{proof}

Parallelization of $\gck{k}$ results in a Weihrauch equivalent problem.  This arises from the well-known
idempotence of the parallelization operator, which can be verified in the formal setting.

\begin{lemma}\label{WKLH}
$( i{\sf RCA}_0^\omega )$  The hat operator is idempotent, that is, for any problem $\sf P$, $\widehat{\sf P}\equiv_{W} \widehat{\widehat{\sf P}}$.  Consequently, for $k\ge 2$, $\gck{k} \equiv_{W} \widehat {\gck{k}}$.
\end{lemma}

\begin{proof}
In $i{\sf RCA}_0^\omega$, we can use the bijective pairing function to match each pair $(i,j)$ with an integer code.  Given a
sequence of sequences of problems $\langle\langle p_{i,j} \mid j \in \mathbb N \rangle i\in \mathbb N \rangle$, we match each problem
with an element of the sequence $\langle p_{(i,j)} \mid (i,j) \in \mathbb N\rangle$.  Thus $\widehat{\widehat{\sf P}} \le_{W} \widehat{\sf P}$.
The reverse reduction is trivial.

From Theorem \ref{GCT} we know that $\gck{k} \equiv_{W} \widehat {\sf LLPO}$.  By Lemma \ref{HAT},
$\widehat{ \gck{k}} \equiv_{W} \widehat {\widehat {\sf LLPO}}$.  From the preceding paragraph, $\widehat {\widehat {\sf LLPO}} \equiv_{W} \widehat {\sf LLPO}$,
so the desired equivalence follows by transitivity.
\end{proof}

In combination with Theorem \ref{GCT} we see that $\widehat{\gck{2}} \equiv_{W} \widehat{\gck{3}}$.  These problems correspond
to reverse mathematical statements about infinite sequences  of 2-colorings and 3-colorings reminiscent of those of
Hirst and Lempp \cite{hl}.  The corresponding reverse mathematical results can be extracted in the usual fashion,
yielding the following corollary.

\begin{corollary}\label{GCC4}
$(i{\sf RCA}_0 )$  For $k\ge 2$, ${\sf WKL}$ is equivalent to the assertion that
for any sequence $\seq{G_i}_{i \in \mathbb N}$ of infinite locally $k$-colorable graphs, there
is a function $f: \mathbb N \times \mathbb N \to \mathbb N$ such that for each $i$, the function $f(i,n)$ is
a $k$-coloring of $G_i$.
\end{corollary}

The $k$-coloring problem defined at the beginning of this subsection does not accept
inputs which are not locally $k$-colorable.  The following alternative definition extends
the possible inputs to all graphs.

\begin{dTCk}(Total $k$-coloring of graphs):
Given a graph $G$, there is a function $f: \mathbb N \to \mathbb N$
such that $f(0)=0$ implies $f$ is a $k$-coloring of $G$ and $f(0)>0$ implies $G_{f(0)}$ has no $k$-coloring.
\end{dTCk}

The predicate asserting that $f$ solves $\tgc{k}$ for $G$ can be formalized as a $\exists$-free formula
in the parameters $k$, $f$, and $G$.
Altering the problem affects the Weihrauch analysis.

\begin{theorem}\label{TGC1}
$( i{\sf RCA}_0^\omega )$  For $k\ge 2$, ${\sf{LPO}}\le_{W} \tgc{k} \le_{W} \widehat {\sf{LPO}}$.
\end{theorem}

\begin{proof}
For the first reduction, fix $k$ and suppose $p$ is an instance of ${\sf{LPO}}$.  Let $G$ be the graph
which is completely disconnected except for a completely connected subgraph on the vertices
$\{m, m+1, \dots , m+k\}$ if $p(m)=0$ and $\forall t< m (p(m) \neq 0)$, if such an $m$ exists.
The characteristic function for the edges of $G$ is uniformly computable from $p$.  Suppose
$f$ is a solution of $\tgc{k}$ for $G$.  Then $f(0)=0$ if and only if $\forall k (p(k) \neq 0)$.  Also,
if there is a least $m$ such that $p(m)=0$, then $G_{m+k}$ is the first initial subgraph of $G$
with no $k$-coloring.  In this case, $f(0)=m+k$ and the solution to the ${\sf{LPO}}$ problem $p$ is
obtained by subtracting the fixed value $k$.

For the second reduction, suppose $G$ is a graph.  Let $p_0 (n) = 1$ if for all $t\le n$ the initial
subgraph $G_k$ has a $k$-coloring, and let $p_0 (n) = 0$ otherwise.  For $i>0$, define $p_i$ as follows.
Let $\sigma_1 , \sigma_2 , \dots$ be the finite sequences in $k^{<\mathbb N}$
that start with $0$ and occur in the tree of initial segments of
$k$ colorings of $G$.  If there are only finitely many such sequences, pad the list with copies of the empty
sequence.  Let $p_i (m) = 1$ if $\sigma_i$ extends to a $k$-coloring of $G_m$, and let $p_i (m) = 0$
otherwise.  Given a solution to the $\widehat {\sf{LPO}}$ problem $\langle p_i \rangle_{i \in \mathbb N}$, we can compute a
solution $f$ to $\tgc{k}$ for $G$ as follows.  Let $f(0) ={\sf{LPO}} (p_0 )$.  If $ f(0)>0$, let $f(n) = 0$ for all $n>0$.
Otherwise, use the values of ${\sf{LPO}} (p_n )$ for $n>0$ to enumerate the nodes in a path through the tree of partial colorings
and assign the values of $f$ to match the nodes in the path.
This enumeration is computable because if ${\sf{LPO}} (p_n) = 0$, then the tree of partial
$k$-colorings extending $\sigma_n$ is infinite, and there is a least $m$ such that there is a $j<k$ with
$\sigma_m=\sigma_n ^\frown j$ and ${\sf{LPO}} ( p_m ) = 0$.
\end{proof}

\begin{corollary}\label {TGC2}
$( i{\sf RCA}_0^\omega )$  For $k\ge 2$, $\widehat {\tgc{k}} \equiv_{W} \widehat {\sf{LPO}}$ and $\widehat  {\gck{k}} \equiv_{W} \widehat {\sf LLPO}$.
\end{corollary}

\begin{proof}
Apply parallelization and idempotence to the reductions in Corollary \ref{TGC2} and Corollary \ref{GCC2}.
\end{proof}

Because the associated predicates are $\exists$-free, the Weihrauch results of Corollary \ref{TGC2}
can be converted to a reverse mathematics result
after the fashion of Corollary \ref{GCC4}.

\begin{corollary}\label{TGC3}
$(i{\sf RCA}_0 )$  For $k\ge 2$, ${\sf ACA}_0$ is equivalent to the assertion that
for any sequence $\seq{G_i}_{i \in \mathbb N}$ of graphs, there
is a function $f: \mathbb N \times \mathbb N \to \mathbb N$ such that for each $i$, either $f(i,0)=m>0$ and the $m^\text{th}$ initial subgraph
of $G_i$ is not $k$-colorable or $f(i,0)=0$ and the function $f(i,n)$ is
a $k$-coloring of $G_i$.
\end{corollary}

The previous corollary again demonstrates the use of formal Weihrauch techniques to derive reverse mathematical results.
We close this section by illustrating a limitation of the formal approach.  In traditional Weihrauch analysis, we
can show that ${\sf P} \not \le_{W} {\sf Q}$ by showing that there are no computable functionals witnessing the reduction.
The formal setting does not distinguish between computable witnesses and other functionals, so there
is no analogous argument.  Consequently, results about strict Weihrauch reducibility are not amenable to formalization in $i{\sf RCA}_0^\omega$.

\begin{corollary}\label {TGC4}
For $k\ge 2$, $i{\sf RCA}_0^\omega$ proves $\gck{k} \le_{W} \tgc{k}$.  In the non-formal setting, $\gck{k}<_{W} \tgc{k}$.
\end{corollary}

\begin{proof}
$i{\sf RCA}_0^\omega$ proves that $\gck{k} \le_{W} \tgc{k}$ using the identity functionals as witnesses.  To prove the
strict inequality of the second sentence, we may use classical logic and results from the
Weihrauch reducibility literature.
Suppose by way of contradiction that $\tgc{k} \le_{W} \gck{k}$.  Parallelization preserves the reduction.
By Corollary \ref{TGC2} and transitivity, $\widehat {\sf{LPO}} \le_{W} \widehat {\sf LLPO}$, contradicting
widely known results (e.g.~Theorems 7.23, 7.40, and 7.42 in \cite{bgp}).\end{proof}

\section{Weihrauch analysis related to ${\Pi^1_1 {\text -}{ \sf{CA}}_0}$}

In this section, we apply more traditional techniques of Weihrauch analysis to
problems from \cite{hl}.
The underlying formulas are not $\exists$-free, so the techniques
of the preceding section are not applicable.
The problems are all related to ${\Pi^1_1 {\text -}{ \sf{CA}}_0}$.
The first is based on Lemma VI.1.1 of Simpson \cite{simpson}.

\begin{dWF}(Well founded trees):
Given a tree $T$ in $\mathbb N^{<\mathbb N}$ as input, output $0$ if $T$ contains an infinite path
and $1$ if it does not.
\end{dWF}
The next two problems are based on principles included in Theorem 3.4 of Hirst and Lempp \cite{hl}.

\begin{dS}(Isomorphic subgraph):
Given inputs of graphs $G$ and $H$, output $1$ if $H$ is isomorphic to a subgraph of $G$ and $0$ if it is not.
\end{dS}

Let $L$ denote the linear graph with vertex set $V = \{ v_i \mid i \in \mathbb N\}$ and edges $E= \{(v_i , v_{i+1} )\mid i \in \mathbb N \}$.

\begin{dSL}($L$ as a subgraph):
Given a graph $G$ as input, output $1$ if $L$ is isomorphic to a subgraph of $G$ and $0$ if it is not.
\end{dSL}

\begin{theorem}\label{PW1}
${\sf WF} \equiv_{sW} {\sf S}_L \equiv_{sW} {\sf S}$.
\end{theorem}

\begin{proof}  First we will show that ${\sf WF} \le_{sW} {\sf S}_L$.
Any tree $T$ in $\mathbb N^{<\mathbb N}$ can uniformly be converted to a corresponding graph, with the nodes of the tree as vertices and
edges between neighboring nodes.
Note that the tree $T$ contains an infinite path if and only if the linear graph $L$ is isomorphic
to a subgraph of the graph of $T$.  The output $1-{\sf S}_L (T)$ is equal to ${\sf WF} (T)$, so the post-processing does not
depend on $T$ and the reduction is strong.

The problem  ${\sf S}_L $ is a special case of $\sf S$, so it only remains
to show that ${\sf S} \le_{sW} {\sf WF}$.  Suppose $G$ and $H$ are input graphs with
vertices $\{ g_i \mid i \in \mathbb N \}$ and $\{h_i \mid i \in \mathbb N\}$.
We can uniformly compute the tree $T$ of initial segments of isomorphisms between $H$ and subgraphs of $G$,
where nodes correspond to sequences $g_{i_0} , \dots , g_{i_n}$ such that the pairing of nodes $g_{i_j}$ and $h_j$
for $j\le n$ is an isomorphism of the induced subgraph of $H$ with a subgraph of $G$.  Any infinite path through $T$
is an isomorphism between $H$ and a subgraph of $G$.  Thus $1-{\sf WF} (T)$ is equal to ${\sf S}(G,H)$, yielding the
final strong Weihrauch reduction.
\end{proof}

Theorem 3.4 of \cite{hl} discusses sequences of graphs and trees.  Similar Weihrauch reductions follow by parallelization.

\begin{corollary}\label{PW2}
$\widehat{\sf{WF}} \equiv_{sW} \widehat {\sf S}_L \equiv_{sW} \widehat {\sf S}$.
\end{corollary}

\begin{proof}
As noted in Proposition 3.6 part 3 of \cite {bgp}, parallelization is a strong closure operation with respect
to strong Weihrauch reducibility.  The parallelized equivalences follow immediately from the equivalences in
Theorem \ref{PW1}.
\end{proof}

The proof of Theorem 3.4 of \cite{hl} indicates that an instance of $\widehat{\sf{WF}}$ can be related to isomorphic subgraph
problems for a single target graph $G$.  Let $L_n$ denote the linear graph $L$ with a cycle of size $n+3$ appended
to the first vertex.  For example, $L_0$ is a copy of $L$ with a triangle attached as a tag to the first vertex.

\begin{dSLv}(Tagged linear subgraphs of a fixed graph):
Given a graph $G$ as input, output a function $s: \mathbb N \to 2$ such that $s(n) = 1$ if and only if $L_n$ is a subgraph of $G$.
\end{dSLv}

\begin{theorem}\label{PW3}
$\widehat{\sf{WF}} \equiv_{sW} {\sf S}_{\vec L}$.
\end{theorem}

\begin{proof}  Note that an input $G$ for ${\sf S}_{\vec L}$ corresponds exactly to the input $\seq{G, L_i} _{i \in \mathbb N}$ for $\widehat {\sf S}$.
Thus ${\sf S}_{\vec L} \le_{sW} {\widehat {\sf S}} \equiv_{sW} \widehat{\sf{WF}}$.  To show that $\widehat{\sf{WF}} \le_{sW} {\sf S}_{\vec L}$, we adapt the reversal from Theorem 3.4 of \cite{hl}.
Let $\seq{T_i}_{i \in \mathbb N}$ be an input for $\widehat{\sf{WF}}$.  For each $i$, let $G_i$ be the graph of $T_i$ with a cycle of size $i+3$ attached
to the root node.  The graph $G$ consisting of the disjoint union of the $G_i$ graphs is uniformly computable from
$\seq{T_i}_{i \in \mathbb N}$.  Note that $L_i$ is isomorphic to a subgraph of $G$ if and only if $L_i$ is isomorphic to a subgraph
of $G_i$, which occurs exactly when $T_i$ is not well founded.  If $s:\mathbb N \to 2$ is a solution to ${\sf S}_{\vec L}$ for this graph $G$, then
$w(n)=1-s(n)$ is a solution of $\widehat{\sf{WF}}$ for $\seq{T_i}_{i \in \mathbb N}$, completing the proof that $\widehat{\sf{WF}} \le_{sW} {\sf S}_{\vec L}$.
\end{proof}

Many other graphs could be substituted for the linear graph $L$ in the preceding discussion.  However, not all graphs
yield the same results.  For example, while ${\sf S}_L \equiv_{sW} {\sf WF}$, finite graphs yield a weaker Weihrauch problem.

\begin{theorem}\label{PW4}
Suppose that $F$ is a finite graph with at least two vertices.  Then ${\sf S}_F \equiv_{W} {\sf{LPO}}$.
\end{theorem}

\begin{proof}
We will prove the result for the version of ${\sf{LPO}}$ from section \S\ref{section2}.
For other versions of ${\sf{LPO}}$, the result can be strengthened to strong Weihrauch reduction.
Fix a finite graph $F$.  To show that ${\sf S}_F \le_{W} {\sf{LPO}}$, let $G$ be an input graph and
construct an input for ${\sf{LPO}}$ as follows.  For each $n$, if $F$ is not isomorphic to a subgraph of $G$ restricted
to the first $n$ vertices of $G$, set $p(n)=1$.  If $F$ is isomorphic to such a subgraph, set $p(n)=0$.  Thus
${\sf S}_F (G) = 1$ if and only if ${\sf{LPO}} (p) > 0$.

To prove that ${\sf{LPO}} \le_{W} {\sf S}_F$, we will consider two cases.  First suppose that $F$ is a finite graph with
$j$ vertices and at least one edge.  Let $p$ be an instance of ${\sf{LPO}}$.  Let $G$ be the graph with vertices
$\{v_i \mid i \in \mathbb N \}$, and with edges corresponding to a copy of $F$ on vertices $v_m , \dots , v_{m+j-1}$
if $m$ is the least value such that $p(m)= 0$.  If no such $m$ exists, then $G$ is completely disconnected.
Note that each edge of $G$ depends only on an initial segment of the values of $p$, so $G$ is uniformly
computable from $p$.  If ${\sf S}_F (G) = 0$, output $0$ for ${\sf{LPO}}(p)$.
If ${\sf S}_F (G) = 1$, then the search for the least $m$ such that $p(m)=0$ will
succeed and the appropriate value of ${\sf{LPO}} (p)$ can be output.

The case when $F$ is completely disconnected is similar, using complementary graphs.  All possible edges
are added to $G$ until a zero of $p$ is discovered, at which point no additional edges are added.
\end{proof}

The fact that ${\sf S}_F \equiv_{W} {\sf{LPO}}$ and ${\sf S}_L \equiv_{W} {\sf WF}$ motivates the following question:  Is there a graph
$H$ such that ${\sf{LPO}} <_{W} {\sf S}_H <_{W} {\sf WF}$?
Arno Pauly says yes, if we switch from isomorphism to subgraph embedding ({\sf SE}).
For the graph $H$ consisting of infinitely many copies of K3, $ {\sf SE}_H\equiv_{\sf W} {\sf{LPO}}^\prime$  \cite{pauly}.
Switching to embeddings does not change Theorem \ref{PW1}, for example.  Reed Solomon has
asked what other reductions differ in strength for various notions of embedding.

We can also consider the problem ${\sf S}^G$ for a fixed graph $G$, asking whether or not an input graph is isomorphic
to a subgraph of $G$.  For the complete graph $K$ and the totally disconnected graph $D$ it is easy to show that
${\sf S}^K$ and ${\sf S}^D$ are both Weihrauch equivalent to ${\sf{LPO}}$.  Theorem 3.2 of \cite {hl} shows that there is a
computable graph $G$ such that the set of indices of computable graphs that are isomorphic to a subgraph of $G$ is
$\Sigma^1_1$ complete.  This prompts us to ask:  Is there a graph $G$ such that ${\sf S}^G \equiv_{sW} {\sf WF}$?
Indeed, is there even a graph $G$ such that ${\sf{LPO}} <_{W} {\sf S}^G$?

Theorem 2.6 of \cite{hl} shows a connection between sequential versions of the following problems.
For a graph $G$ with vertex set $V$, we say $c:V\to \mathbb N$ is a coloring of $G$ if whenever $(v_1 , v_2)$ is
an edge of $G$, $c(v_1 ) \neq c(v_2 )$.

\begin{dRC} (Repeated color):
Given a graph $G$ as an input, output $1$ if there is a coloring of $G$ that uses one color infinitely often and
output $0$ if there is no such coloring.
\end{dRC}

\begin{dD}(Disconnected subgraph):
Given a graph $G$ as an input, output $1$ if $G$ has an infinite completely disconnected subgraph and output
$0$ otherwise.
\end{dD}

\begin{theorem}\label{PW5}
${\sf RC} \equiv_{sW} {\sf D} \equiv_{sW} {\sf WF}$.
\end{theorem}

\begin{proof}
Any graph $G$ has a coloring as required by $\sf RC$ if and only if it has a subgraph as in $\sf D$.  Thus
${\sf RC} \equiv_{sW} {\sf D}$.  Overloading notation and using $D$ to denote the totally disconnected graph,
we have ${\sf D} \equiv_{sW} {\sf S}_D$.  The problem ${\sf S}_D$ is a special case of ${\sf S}$, so
${\sf D} \le_{sW} {\sf S} \equiv_{sW} {\sf WF}$.

To show that ${\sf WF} \le_{sW} {\sf S}_D$, given a tree $T$ as input, define a graph $G$ as follows.  The vertices of
$G$ will consist of the nodes of $T$.  A pair $(v_1 , v_2 )$ is an edge in $G$ if and only if the corresponding
nodes of $T$ are incomparable.  (Nodes of $T$ are comparable if one extends the other in the tree.)  $G$ is
uniformly computable from $T$.  The completely disconnected graph $D$ is isomorphic to a subgraph of
$G$ if and only if $T$ contains an infinite collection of pairwise comparable nodes, that is, if and only if
$T$ is not well founded.  For $T$ and $G$ as described above, ${\sf WF} (T) = 1-{\sf S}_D (G)$, so
${\sf WF} \le_{sW} {\sf S}_D$, as desired.
\end{proof}

Appending a triangle to each tree node in the previous construction yields a proof that ${\sf WF}$ is Weihrauch
equivalent to ${\sf S}_G$ for the graph $G$ consisting of infinitely many disconnected triangles.
(This was proven independently by Arno Pauly \cite{pauly}.)  Thus
the graph from Pauly's embedding observation does not answer our question about isomorphic subgraphs.
Parallelizing the previous theorem yields Weihrauch equivalences mirroring the reverse mathematics of Theorem 2.6 of \cite{hl}.

\begin{corollary}
$\widehat{\sf RC} \equiv_{sW} \widehat{\sf D} \equiv_{sW} \widehat{\sf{WF}}$.
\end{corollary}

\begin{proof}
Immediate from Theorem \ref{PW5} by Proposition 3.6 part 3 of \cite{bgp}.
\end{proof}

The application of Weihrauch analysis to the problems of this section yields no new
insights into the corresponding finite complexity theoretic relationships.  However, it does raise
some new Weihrauch analysis questions.  Analyzing infinite versions of other statements from
finite complexity theory might lead to additional interesting Weihrauch reductions.

\begin{bibsection}[Bibliography]
\begin{biblist}

\bib{bgp}{article}{
author={Brattka, Vasco},
author={Gherardi, Guido},
author={Pauly, Arno},
title={Weihrauch Complexity in computable analysis},
date={2018},
pages={1--61},
note={available at arXiv:1808.03202v4},
}

\bib{dorais}{article}{
   author={Dorais, Fran{\c{c}}ois G.},
   title={Classical consequences of continuous choice principles from
   intuitionistic analysis},
   journal={Notre Dame J. Form. Log.},
   volume={55},
   date={2014},
   number={1},
   pages={25--39},
   issn={0029-4527},
   review={\MR{3161410}},
   doi={10.1215/00294527-2377860},
}

\bib{doraisetal}{article}{
  author={Dorais, Fran{\c c}ois G.},
  author={Dzhafarov, Damir D.},
  author={Hirst, Jeffry L.},
  author={ Mileti, Joseph R.},
  author={Shafer, Paul},
  title={On uniform relationships between combinatorial problems},
  journal={Trans.\ AMS},
  year={2014},
  volume={368},
  pages={1321--1359},
  doi={10.1090/tran/6465},
}

\bib{hl}{article}{
   author={Hirst, Jeffry L.},
   author={Lempp, Steffen},
   title={Infinite versions of some problems from finite complexity theory},
   journal={Notre Dame J. Form. Log.},
   volume={37},
   date={1996},
   number={4},
   pages={545--553},
   issn={0029-4527},
   review={\MR{1446228}},
   doi={10.1305/ndjfl/1040046141},
}

\bib{hmunif}{article}{
   author={Hirst, Jeffry L.},
   author={Mummert, Carl},
   title={Reverse mathematics and uniformity in proofs without excluded
   middle},
   journal={Notre Dame J. Form. Log.},
   volume={52},
   date={2011},
   number={2},
   pages={149--162},
   issn={0029-4527},
   review={\MR{2794648}},
   doi={10.1215/00294527-1306163},
}

\bib{hm}{article}{
author={Hirst, Jeffry L.},
author={Mummert, Carl},
title={Using Ramsey's theorem once},
journal={Arch. Math. Logic},
date={2019},
pages={1--10},
issn={0933-5846},
doi={10.1007/s00153-019-00664-z},
}

\bib{leaf}{article}{
   author={Hirst, Jeffry L.},
   title={Leaf management},
   journal={Computability},
   volume={9},
   date={2020},
   number={3-4},
   pages={309--314},
   issn={2211-3568},
   review={\MR{4133717}},
   doi={10.3233/com-180243},
}

\bib{kmp}{article}{
   author={Kihara, Takayuki},
   author={Marcone, Alberto},
   author={Pauly, Arno},
   title={Searching for an analogue of ${\sf ATR}_0$ in the Weihrauch lattice},
   journal={J. Symb. Log.},
   volume={85},
   date={2020},
   number={3},
   pages={1006--1043},
   issn={0022-4812},
   review={\MR{4231614}},
   doi={10.1017/jsl.2020.12},
}

\bib{k2001}{article}{
   author={Kohlenbach, Ulrich},
   title={Higher order reverse mathematics},
   conference={
      title={Reverse mathematics 2001},
   },
   book={
      series={Lect. Notes Log.},
      volume={21},
      publisher={Assoc. Symb. Log., La Jolla, CA},
   },
   date={2005},
   pages={281--295},
   review={\MR{2185441}},
}

\bib{kbook}{book}{
   author={Kohlenbach, Ulrich},
   title={Applied proof theory: proof interpretations and their use in
   mathematics},
   series={Springer Monographs in Mathematics},
   publisher={Springer-Verlag, Berlin},
   date={2008},
   pages={xx+532},
   isbn={978-3-540-77532-4},
   review={\MR{2445721}},
}

\bib{pauly}{miscellaneous}{
author={Pauly, Arno},
title={Personal communication},
date={2021},
}

\bib{simpson}{book}{
   author={Simpson, Stephen G.},
   title={Subsystems of second order arithmetic},
   series={Perspectives in Logic},
   edition={2},
   publisher={Cambridge University Press, Cambridge; Assoc.
   Symb. Log., Poughkeepsie, NY},
   date={2009},
   pages={xvi+444},
   isbn={978-0-521-88439-6},
   review={\MR{2517689 (2010e:03073)}},
   doi={10.1017/CBO9780511581007},
}

\bib{troelstra}{book}{
author={Troelstra, A.~S.},
title={Metamathematical investigation of intuitionistic arithmetic and analysis},
series={Lect. Notes in Math.},
volume ={344},
publisher={Springer, Berlin},
date={1973},
pages={xvii+485},
isbn={0-387-06491-5},
}

\end{biblist}
\end{bibsection}
\end{document}

@article {bgp,
AUTHOR={Brattka, Vasco and
Gherardi, Guido and
Pauly, Arno},
TITLE={Weihrauch Complexity in computable analysis},
YEAR={2018},
PAGES={1--61},
NOTE={available at arXiv:1808.03202v4},
}

@article {dorais,
    AUTHOR = {Dorais, Fran\c{c}ois G.},
     TITLE = {Classical consequences of continuous choice principles from
              intuitionistic analysis},
   JOURNAL = {Notre Dame J. Form. Log.},
  FJOURNAL = {Notre Dame Journal of Formal Logic},
    VOLUME = {55},
      YEAR = {2014},
    NUMBER = {1},
     PAGES = {25--39},
      ISSN = {0029-4527},
   MRCLASS = {03B20 (03B30 03F35 03F55)},
  MRNUMBER = {3161410},
MRREVIEWER = {Carl Mummert},
       DOI = {10.1215/00294527-2377860},
       URL = {https://doi.org/10.1215/00294527-2377860},
}

@article {doraisetal,
    AUTHOR = {Dorais, Fran\c{c}ois G. and Dzhafarov, Damir D. and Hirst, Jeffry
              L. and Mileti, Joseph R. and Shafer, Paul},
     TITLE = {On uniform relationships between combinatorial problems},
   JOURNAL = {Trans. Amer. Math. Soc.},
  FJOURNAL = {Transactions of the American Mathematical Society},
    VOLUME = {368},
      YEAR = {2016},
    NUMBER = {2},
     PAGES = {1321--1359},
      ISSN = {0002-9947},
   MRCLASS = {03B30 (03D30 03D32 03D80 03F35 05D10 05D15 05D40)},
  MRNUMBER = {3430365},
MRREVIEWER = {Denis R. Hirschfeldt},
       DOI = {10.1090/tran/6465},
       URL = {https://doi.org/10.1090/tran/6465},
}

AUTHOR
@article {hl,
    AUTHOR = {Hirst, Jeffry L. and Lempp, Steffen},
     TITLE = {Infinite versions of some problems from finite complexity
              theory},
   JOURNAL = {Notre Dame J. Formal Logic},
  FJOURNAL = {Notre Dame Journal of Formal Logic},
    VOLUME = {37},
      YEAR = {1996},
    NUMBER = {4},
     PAGES = {545--553},
      ISSN = {0029-4527},
   MRCLASS = {03D15 (03D35 68Q15)},
  MRNUMBER = {1446228},
MRREVIEWER = {Uwe Sch\"{o}ning},
       DOI = {10.1305/ndjfl/1040046141},
       URL = {https://doi.org/10.1305/ndjfl/1040046141},
}

@article {hmunif,
    AUTHOR = {Hirst, Jeffry L. and Mummert, Carl},
     TITLE = {Reverse mathematics and uniformity in proofs without excluded
              middle},
   JOURNAL = {Notre Dame J. Form. Log.},
  FJOURNAL = {Notre Dame Journal of Formal Logic},
    VOLUME = {52},
      YEAR = {2011},
    NUMBER = {2},
     PAGES = {149--162},
      ISSN = {0029-4527},
   MRCLASS = {03F50 (03B30 03F35 03F60)},
  MRNUMBER = {2794648},
MRREVIEWER = {Paulo Oliva},
       DOI = {10.1215/00294527-1306163},
       URL = {https://doi.org/10.1215/00294527-1306163},
}

@article{hm,
AUTHOR={Hirst, Jeffry L. and Mummert, Carl},
TITLE={Using Ramsey's theorem once},
 JOURNAL = {Arch. Math. Logic},
  FJOURNAL = {Archive for Mathematical Logic},
YEAR={2019},
PAGES={1--10},
ISSN={0933-5846},
DOI={10.1007/s00153-019-00664-z},
URL={https://doi.org/10.1007/s00153-019-00664-z},
}

@article {leaf,
    AUTHOR = {Hirst, Jeffry L.},
     TITLE = {Leaf management},
   JOURNAL = {Computability},
  FJOURNAL = {Computability. The Journal of the Association CiE},
    VOLUME = {9},
      YEAR = {2020},
    NUMBER = {3-4},
     PAGES = {309--314},
      ISSN = {2211-3568},
   MRCLASS = {03F35 (03D30)},
  MRNUMBER = {4133717},
       DOI = {10.3233/com-180243},
       URL = {https://doi.org/10.3233/com-180243},
}

@article {kmp,
    AUTHOR = {Kihara, Takayuki and Marcone, Alberto and Pauly, Arno},
     TITLE = {S{earching} {for} {an} {analogue} {of} ${\sf ATR}_0$ {in} {the}
              {Weihrauch} {lattice}},
   JOURNAL = {J. Symb. Log.},
  FJOURNAL = {The Journal of Symbolic Logic},
    VOLUME = {85},
      YEAR = {2020},
    NUMBER = {3},
     PAGES = {1006--1043},
      ISSN = {0022-4812},
   MRCLASS = {03D78 (03B30 03D30)},
  MRNUMBER = {4231614},
       DOI = {10.1017/jsl.2020.12},
       URL = {https://doi.org/10.1017/jsl.2020.12},
}

@incollection {k2001,
    AUTHOR = {Kohlenbach, Ulrich},
     TITLE = {Higher order reverse mathematics},
 BOOKTITLE = {Reverse mathematics 2001},
    SERIES = {Lect. Notes Log.},
    EDITOR = {S. Simpson},
    VOLUME = {21},
     PAGES = {281--295},
 PUBLISHER = {Assoc. Symbol. Logic, La Jolla, CA},
      YEAR = {2005},
   MRCLASS = {03F60 (03D65 03F35)},
  MRNUMBER = {2185441},
  URL={https://doi.org/10.1017/9781316755846.018},
  DOI={10.1017/9781316755846.018},
}

@book {kbook,
    AUTHOR = {Kohlenbach, U.},
     TITLE = {Applied proof theory: proof interpretations and their use in
              mathematics},
    SERIES = {Springer Monographs in Mathematics},
 PUBLISHER = {Springer-Verlag, Berlin},
      YEAR = {2008},
     PAGES = {xx+532},
      ISBN = {978-3-540-77532-4},
   MRCLASS = {03-02 (03Fxx 41A50 46Bxx 47Hxx 54E35)},
  MRNUMBER = {2445721},
MRREVIEWER = {H. Schwichtenberg},
}

@misc {pauly,
author={Pauly, Arno},
title={Personal communication},
year={2021},
}

@book {simpson,
    AUTHOR = {Simpson, Stephen G.},
     TITLE = {Subsystems of second order arithmetic},
    SERIES = {Perspectives in Logic},
   EDITION = {Second},
 PUBLISHER = {Cambridge University Press, Cambridge; Association for
              Symbolic Logic, Poughkeepsie, NY},
      YEAR = {2009},
     PAGES = {xvi+444},
      ISBN = {978-0-521-88439-6},
   MRCLASS = {03F35 (03-02 03B30)},
  MRNUMBER = {2517689},
       DOI = {10.1017/CBO9780511581007},
       URL = {https://doi.org/10.1017/CBO9780511581007},
}

@book {troelstra,
AUTHOR={Troelstra, A.~S.},
TITLE={Metamathematical investigation of intuitionistic arithmetic and analysis},
SERIES={Lect. Notes in Math.},
VOLUME ={344},
PUBLISHER={Springer, Berlin},
YEAR={1973},
PAGES={xvii+485},
ISBN={0-387-06491-5},
DOI={https://doi.org/10.1007/BFb0066739},
URL={10.1007/BFb0066739},
}