text:
\section{Introduction}
This work explores the uniform computational strength of some infinite-dimensional generalizations of Ramsey's theorem. The classical finite-dimensional Ramsey theorem can be stated as follows: for every $A\subset \mathbb{N}$ let $[A]^n:=\{ B\subset A: |B|=n\}$ be the set of subsets of $A$ with cardinality $n$. A map $c\colon[\mathbb{N}]^n\to k$ is called a \textdef{$k$-coloring} of $[\mathbb{N}]^n$. A set $H$ s.t.\ $c([H]^n)=\{i\}$ for some $i<k$ is called \textdef{homogeneous} for $c$.
\begin{theorem}[Ramsey's theorem]
	For every $n,k\ge 1$ and every coloring $c\colon[\mathbb{N}]^n\to k$ there is an infinite subset $H\subset \mathbb{N}$ that is homogeneous for $c$.
\end{theorem}
There is a vast literature exploring the computational aspects of Ramsey's theorem. Our focus will be on the infinite generalization of the above result, i.e.\ we will consider $n=\infty$. In particular we will focus on Nash-Williams' theorem, also called the open Ramsey theorem:
\begin{theorem}[Nash-Williams \cite{NashWilliams65}]
	The open subsets of ${[\mathbb{N}]}^\mathbb{N} $ admit infinite homogeneous sets.
\end{theorem}
We will also consider the restriction of Nash-Williams' theorem to clopen subsets of ${[\mathbb{N}]}^\mathbb{N} $.

The notion of Weihrauch reducibility provides a useful tool to explore the uniform computational content of theorems: indeed many statements in mathematics can be written in the form $(\forall x\in X)(\varphi(x)\rightarrow(\exists y\in Y)(\psi(x,y)))$, which can be thought of as a computational problem where $x$ is an instance of a problem and the goal is to find a solution $y$ (which is, in general, not unique). This can be naturally written in the language of partial multivalued functions by considering $f\pmfunction{X}{Y}$ s.t.\ $f(x)=\{y\in Y : \psi(x,y)\}$, for every $x\in X$ s.t.\ $\varphi(x)$.

Starting with the work of Gherardi and Marcone \cite{GM09}, it has been shown that Weihrauch reducibility provides a bridge between computable analysis and reverse mathematics. In particular reverse mathematics focuses on proving the equivalence of statements over a weak base theory. Historically, a large number of theorems turned to be equivalent to one of the so-called \textdef{big five}: $\mathrm{RCA}_0$, $\mathrm{WKL}_0$, $\mathrm{ACA}_0$, $\mathrm{ATR}_0$, $\boldsymbol{\Pi}^1_1\mathrm{-CA}_0$. Oftentimes, the close connection between reverse mathematics and Weihrauch reducibility has been exploited to translate results from one setting into the other.

Following this connection, there are a number of established ``analogues'' of the big-five in the Weihrauch lattice: $\mathrm{RCA}_0$ corresponds to computable problems, $\mathrm{WKL}_0$ corresponds to $\mathsf{C}_\Cantor$ (i.e.\ choosing an element from a non-empty closed subset of ${2^\mathbb{N}}$) and $\mathrm{ACA}_0$ corresponds to iterations of $\mathsf{lim}$.

Recently Marcone \cite{Dagstuhl2016} raised the question ``What do the Weihrauch hierarchies look like once we go to very high levels of reverse mathematics strength?". There have been several works in this direction: Kihara, Marcone and Pauly \cite{KMP20} have studied several principles, like the (strong) comparability of well-orders, the perfect tree theorem and the open determinacy theorem; Goh \cite{gohatr,GohThesis} analyzed the weak comparability of well-orders and the K\"onig duality theorem; Angl\`es D'Auriac and Kihara \cite{KiharaADauriacChoice} dealt with the $\Sigma^1_1$ choice on $\mathbb{N}$ and variants thereof.

Our work explores the formalization of the open and clopen Ramsey theorems as multivalued functions and analyzes their position in the Weihrauch lattice (both the open and the clopen Ramsey theorems are known to be equivalent to $\mathrm{ATR}_0$ over $\mathrm{RCA}_0$, see \cite[Sec.\ V.9]{Simpson09}). Notice that, as already occurred to other principles equivalent to $\mathrm{ATR}_0$ (\cite{KMP20,GohThesis}), there is not a single multivalued function corresponding to the open Ramsey theorem. Actually, in our case, the situation is even more complex than for the open determinacy or the perfect tree theorem, as the two alternatives (homogeneous solution on the open side or homogeneous solution on the closed side) given by the open Ramsey theorem are not mutually exclusive. Therefore given an open set we can ask for a homogeneous solution on the open side, a homogeneous solution on the closed side or a homogeneous solution on either side. Altogether we will define five different multivalued functions corresponding to the open Ramsey theorem and three different functions corresponding to the clopen Ramsey theorem.

While it is hard to point out a single analogue of $\mathrm{ATR}_0$ in the Weihrauch lattice, there are a number of degrees that play a central role in calibrating the strength of principles that, from the point of view of reverse mathematics, lie at the level of $\mathrm{ATR}_0$. Prominent among these are $\mathsf{UC}_\Baire$, $\mathsf{C}_\Baire$ and $\mathsf{TC}_\Baire$ (see Section \ref{subsec:wei} for their precise definitions).
It is known that $\mathsf{UC}_\Baire<_\mathrm{W}\mathsf{C}_\Baire<_\mathrm{W}\mathsf{TC}_\Baire$ (see \cite{KMP20}).

When dealing with multivalued functions that are very high in the Weihrauch lattice it is often appropriate to use arithmetic Weihrauch reducibility rather than (computable) Weihrauch reducibility.

In Figure \ref{fig:summary} we summarize the results we obtain both with respect to Weihrauch reducibility and arithmetic Weihrauch reducibility. Notice that the multivalued function $\mathsf{FindHS}_{\boldfaceSigma^0_1} $ is stronger than any multivalued function related to $\mathrm{ATR}_0$ considered so far. In fact all these functions are strictly Weihrauch reducible to $\mathsf{TC}_\Baire^*$, which, by \thref{thm:tcbaire^*<findHopen}, is strictly below $\mathsf{FindHS}_{\boldfaceSigma^0_1} $. Notice also that, since $\mathsf{FindHS}_{\boldfaceSigma^0_1} $ is closed under parallel product (\thref{prop:findHopen_closed_product}), it computes $\mathsf{sTC}_{\Baire}^* \equiv_{\mathrm{W}} \mathsf{TC}_\Baire^*\times \chi_{\Pi^1_1}^*$, which was suggested as an $\mathrm{ATR}_0$ analogue in \cite[Sec.\ 9]{KMP20}.
\begin{figure}
\begin{center}
	\tikzstyle{every picture}=[tikzfig]
	\input{summary.tikz}
	\caption{Multivalued functions related to the open and clopen Ramsey theorems in the Weihrauch lattice. Dashed arrows represent Weihrauch reducibility in the direction of the arrow, solid arrows represent strict Weihrauch reducibility. The large rectangles indicate arithmetic Weihrauch equivalence classes. In particular, every function strictly arithmetically reduces to all the functions in rectangles above its own.}
	\label{fig:summary}
\end{center}
\end{figure}

\subsection{Structure of the paper}
In Section \ref{sec:background} we briefly introduce the notation and recall the
preliminary notions on represented spaces (Section \ref{subsec:rep_spaces}) and Weihrauch reducibility (Section \ref{subsec:wei}). In Section \ref{sec:ramsey} we will recall the precise statement for the open and clopen Ramsey theorems and prove some lemmas that will be useful in proving the results on the Weihrauch degrees. The reader may skip these lemmas on the first read, and return to it as needed. In Section \ref{sec:rt_wei} we define the multivalued functions corresponding to the open and clopen Ramsey theorems and study their degrees. In particular we divide the analysis into: functions that are reducible to $\mathsf{UC}_\Baire$ (Section \ref{subsec:ucbaire}), functions that are reducible to $\mathsf{C}_\Baire$ (but not to $\mathsf{UC}_\Baire$, Section \ref{subsec:cbaire}) and functions that are not reducible to $\mathsf{C}_\Baire$ (Section \ref{subsec:not_cbaire}). Moreover, in Section \ref{subsec:strong_wei} we characterize the strength of these functions from the point of view of strong Weihrauch reducibility. Finally, in Section \ref{sec:artihemtic_reducibility} we focus on the behavior of these functions under arithmetic Weihrauch reducibility and in Section \ref{sec:conclusions} we draw some conclusions and list some open problems.

\section{Background}
\thlabel{sec:background}
	We refer the reader to \cite{Simpson09} for a detailed introduction to reverse mathematics.

	Here we introduce the notation we will use in the rest of the paper.

	Let ${\mathbb{N}^\mathbb{N}}$ be the Baire space endowed with the usual product topology and let ${\mathbb{N}^{<\mathbb{N}}}$ be the set of finite sequences of natural numbers. Let also ${[\mathbb{N}]}^\mathbb{N} $ be the space of total functions $f\colon \mathbb{N}\to\mathbb{N}$ that are strictly increasing (i.e.\ $n<m\Rightarrow f(n)<f(m)$). This is sometimes called \textdef{Ramsey space} (see e.g.\ \cite[Sec.\ V.9]{Simpson09}). We will use the symbol $\sqsubseteq$ for the prefix relation. For $\sigma,\tau\in{\mathbb{N}^{<\mathbb{N}}}$ we write: $\abslength{\sigma}$ for the length of $\sigma$, $\sigma\raisebox{.9ex}{\ensuremath\smallfrown}  \tau$ for the concatenation of $\sigma$ and $\tau$, and $\sigma\trianglelefteq \tau$ for the domination relation, i.e.\ $\abslength{\sigma}=\abslength{\tau}$ and $(\forall i<\abslength{\sigma})(\sigma(i)\le \tau(i))$. The domination relation applies also to infinite strings. Also if $x\in{\mathbb{N}^{<\mathbb{N}}}\cup {\mathbb{N}^\mathbb{N}}$ we write $x[m]$ for the prefix of $x$ of length $m$. If $f,g\in{\mathbb{N}^\mathbb{N}}$ we denote the composition $f\circ g$ by $fg$. Moreover, we write $f\preceq g$ if $f$ is a subsequence of $g$, i.e.\ if there exists $h\in{[\mathbb{N}]}^\mathbb{N} $ s.t.\ $f=gh$. In particular for every $h\in{[\mathbb{N}]}^\mathbb{N} $ we have $gh\preceq g$. Similarly, we write $\sigma\preceq^* f$ if $\sigma$ is a finite subsequence of $f$.

\subsection{Represented spaces}
\label{subsec:rep_spaces}
	We briefly introduce the main concepts on the theory of represented spaces. For a more thorough presentation we refer to \cite{Pauly16,Weihrauch00}.

	A \textdef{represented space} is a pair $(X,\repmap{X})$ where $X$ is a set and $\repmap{X}:\subseteq {\mathbb{N}^\mathbb{N}} \to X$ is a partial surjection. For every $x\in X$ a \textdef{name} or \textdef{code} for $x$ is any element of $\repmap{X}^{-1}(x)$. When it is clear from the context, we omit to explicitly mention the representation map $\repmap{X}$.

	Given two representation maps $\delta$ and $\delta'$ of the same set $X$, we say that $\delta$ is \textdef{reducible} to $\delta'$ (and we write $\delta\le_c \delta'$) if there is a computable map $F:\subseteq{\mathbb{N}^\mathbb{N}}\to{\mathbb{N}^\mathbb{N}}$ s.t.\ $\delta(p)=\delta'(F(p))$ for every $p\in \operatorname{dom}(\delta)$. The maps $\delta$ and $\delta'$ are called \textdef{equivalent} if $\delta\le_c\delta'$ and $\delta'\le_c\delta$.

	Let $(X,\repmap{X})$ and $(Y,\repmap{Y})$ be represented spaces and $f\pmfunction{X}{Y}$ be a partial multivalued function. We say that a partial function $F:\subseteq {\mathbb{N}^\mathbb{N}}\to{\mathbb{N}^\mathbb{N}}$ is a \textdef{realizer}\footnote{The very existence of realizers for every $f$ depends on some form of the axiom of choice.} for $f$ (and we write $F\vdash f$) if, for every $p\in\operatorname{dom}(f\circ \repmap{X})$ we have that $\repmap{Y}(F(p))\in f(\repmap{X}(p))$. The notion of realizer allows us to transfer properties of functions on the Baire space (such as computability or continuity) to multivalued functions on represented spaces. In particular we say that a multivalued function between represented spaces is computable if it has a computable realizer.

	Let $(X,d)$ be a separable metric space and $\alpha\colon\mathbb{N}\to X$ be a dense sequence in $X$. The tuple $(X,d,\alpha)$ is called a \textdef{computable metric space} if $d\circ(\alpha\times\alpha)\colon\mathbb{N}^2\to\mathbb{R}$ is a computable double sequence in $\mathbb{R}$.

	Fix a computable enumeration $\sequence{q_n}{n\in\mathbb{N}}$ of $\mathbb{Q}$. If $(X,d,\alpha)$ is a separable metric space, for every $k\ge 1$ we can define the represented spaces $(\boldsymbol{\Sigma}^0_k(X),\repmap{\boldsymbol{\Sigma}^0_k(X)})$, $(\boldsymbol{\Pi}^0_k(X),\repmap{\boldsymbol{\Pi}^0_k(X)})$, $(\boldsymbol{\Delta}^0_k(X),\repmap{\boldsymbol{\Delta}^0_k(X)})$ inductively by:
	\begin{itemize}
		\item $\repmap{\boldsymbol{\Sigma}^0_1(X)}(p):=\bigcup_{\coding{i,j}\in\operatorname{ran}(p)}\ball{\alpha(i)}{q_j}$;
		\item $\repmap{\boldsymbol{\Pi}^0_k(X)}(p):=\setcomplement[X]{\repmap{\boldsymbol{\Sigma}^0_k(X)}(p)}$;
		\item $\repmap{\boldsymbol{\Sigma}^0_{k+1}(X)}(\coding{p_0,p_1,\hdots}):=\bigcup_{i\in\mathbb{N}} \repmap{\boldsymbol{\Pi}^0_k(X)}(p_i)$;
		\item $\repmap{\boldsymbol{\Delta}^0_k(X)}(\coding{p,q}):=\repmap{\boldsymbol{\Sigma}^0_k(X)}(p)$, iff $p\in\operatorname{dom}(\repmap{\boldsymbol{\Sigma}^0_k(X)})$, $q\in\operatorname{dom}(\repmap{\boldsymbol{\Pi}^0_k(X)})$ and $\repmap{\boldsymbol{\Sigma}^0_k(X)}(p)=\setcomplement[X]{\repmap{\boldsymbol{\Pi}^0_k(X)}(q)}$.
	\end{itemize}
	The represented spaces $(\boldsymbol{\Sigma}^0_k(X),\repmap{\boldsymbol{\Sigma}^0_k(X)})$, $(\boldsymbol{\Pi}^0_k(X),\repmap{\boldsymbol{\Pi}^0_k(X)})$ can be defined for any represented space $(X,\repmap{X})$, using the fact that the category of represented spaces is cartesian-closed and letting a name for an open set be the name of its characteristic function, where the codomain $\{0,1\}$ is equipped with the Sierpi\'nski topology.	For separable metric spaces, the two representations are equivalent (see \cite{Pauly16,Brattka05}).

	\begin{lemma}
		\thlabel{lem:computable_operations_open}
		The following maps are computable:
		\begin{enumerate}
			\item \label{itm:includsion_clopen_open} $\boldsymbol{\Delta}^0_1({[\mathbb{N}]}^\mathbb{N} )\hookrightarrow \boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} ):=D\mapsto D$;
			\item \label{itm:compl_clopen_set} $\boldsymbol{\Delta}^0_1({[\mathbb{N}]}^\mathbb{N} )\to \boldsymbol{\Delta}^0_1({[\mathbb{N}]}^\mathbb{N} ):=D\mapsto \setcomplement[{[\mathbb{N}]}^\mathbb{N} ]{D}$;
			\item \label{itm:open_union} $\cup\colon\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )\times\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )\to\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} ):=(P,Q)\mapsto P \cup Q$.
		\end{enumerate}
	\end{lemma}
	\begin{proof}
		${}$
		\begin{description}
			\item[\ref{itm:includsion_clopen_open}, \ref{itm:compl_clopen_set}] follow from the fact that a name for a clopen set is the join $\coding{p,q}$ of two names for open sets (one for the set and one for its complement);
			%
			\item[\ref{itm:open_union}] see \cite[Prop. 3.2(5)]{Brattka05}.\qedhere
		\end{description}
	\end{proof}

	The set $\boldsymbol{\Sigma}^1_1(X)$ of analytic subsets of $X$ can be seen as a represented space by defining a name for $S$ to be a name for a closed set $A\subset X\times {\mathbb{N}^\mathbb{N}}$ s.t.\ $S=\pi_X (A)$ (where $\pi$ denotes projection). Moreover, we can define a name for a coanalytic set $R\in\boldsymbol{\Pi}^1_1(X)$ to be a name for its complement.

	We denote with $\mathbf{Tr}$ the space of trees on $\mathbb{N}$ represented via their characteristic function. Similarly we denote with $\mathbf{Ti}$ the space of trees with strictly increasing strings, represented analogously.
	The function $[\cdot]\colon \mathbf{Tr}\to\boldsymbol{\Pi}^0_1({\mathbb{N}^\mathbb{N}})$ that maps a tree to the set of its paths is computable with multivalued computable inverse. This implies that a closed set $A$ of ${\mathbb{N}^\mathbb{N}}$ or ${[\mathbb{N}]}^\mathbb{N} $ can be equivalently represented via the characteristic function of a tree $T$ s.t.\ $[T]=A$.

	Similarly, an open set $P$ of ${\mathbb{N}^\mathbb{N}}$ can be equivalently represented via an enumeration $p$ of a prefix-free subset of ${\mathbb{N}^{<\mathbb{N}}}$ s.t.\ $P=\{ f\in{\mathbb{N}^\mathbb{N}} : (\exists i)(p(i) \sqsubset f) \}$. With a small abuse of notation we write $\tau\in p$ in place of $\tau \in \operatorname{ran}(p)$. The same considerations can be made for the space ${[\mathbb{N}]}^\mathbb{N} $.

	We denote by $\mathrm{LO}=(\mathrm{LO},\repmap{\mathrm{LO}})$ the represented space of countable linear orders, where an order $L$ is represented by the characteristic function of the relation $\{\coding{a,b}: a\le_L b\}$. We also denote by $\mathrm{WO}=(\mathrm{WO},\repmap{\mathrm{WO}})$ the represented space of countable well-orders, where the representation map $\repmap{\mathrm{WO}}$ is the restriction of $\repmap{\mathrm{LO}}$ to codes of well-orders.

	For every tree $T\subset{\mathbb{N}^{<\mathbb{N}}}$ we denote by $\mathrm{KB}(T)$ the Kleene-Brouwer order on $T$, defined as $\sigma \le_{\mathrm{KB}(T)} \tau$ iff $\sigma,\tau \in T$ and $\tau \sqsubseteq\sigma$ or $\sigma\le_{lex} \tau$. The map $T\mapsto \mathrm{KB}(T)$ from $\mathbf{Tr}$ to $\mathrm{LO}$ is computable. It is known that $\mathrm{KB}(T)$ is a well-order iff $[T]=\emptyset$ (see e.g.\ \cite[Lem.\ V.1.3]{Simpson09}).

\subsection{Weihrauch reducibility}
\label{subsec:wei}
	Let $f\pmfunction{X}{Y}$ and $g\pmfunction{Z}{W}$ be multivalued functions between represented spaces. We say that $f$ is \textdef{Weihrauch reducible} to $g$ and we write $f\le_{\mathrm{W}} g$ iff there are two computable maps $\Phi,\Psi:\subseteq {\mathbb{N}^\mathbb{N}}\to{\mathbb{N}^\mathbb{N}}$ s.t., for every realizer $G\vdash g$ we have $p\mapsto \Psi(\coding{ p,G\Phi(p) })$ is a realizer for $f$. We say that $f$ is \textdef{strongly Weihrauch reducible} to $g$, and we write $f\le_{\mathrm{sW}} g$, if there are two computable maps $\Phi,\Psi:\subseteq {\mathbb{N}^\mathbb{N}}\to{\mathbb{N}^\mathbb{N}}$ s.t., for every realizer $G\vdash g$ we have $\Psi G\Phi \vdash f$. We often say that $\Phi$ is the \textdef{forward} functional of the (strong) Weihrauch reduction, while $\Psi$ is the \textdef{backward} functional.

	The relations $\le_{\mathrm{W}}$ and $\le_{\mathrm{sW}}$ are reflexive and transitive, and therefore induce two degree structures on the family of multivalued functions on represented spaces. For more details on the algebraic properties of the Weihrauch and strong Weihrauch degrees we refer the reader to \cite{HiguchiPauly13,BP16,BGP17}.

	In the following we briefly introduce the operations on multivalued functions that we will need in this work:
	\begin{description}
		\item [parallel product] $f\times g\pmfunction{X\times Z}{Y\times W}:=(x,z)\mapsto f(x)\times g(z)$ with $\operatorname{dom}(f\times g):=\operatorname{dom}(f)\times \operatorname{dom}(g)$;
		\item [finite parallelization] $f^*\pmfunction{\finStrings{X}}{\finStrings{Y}}$ with domain $\operatorname{dom}(f^*):=\{\sequence{x_i}{i<n}: (\forall i<n)(x_i \in \operatorname{dom}(f)) \}$ defined as $f^*(\sequence{x_i}{i<n}):=\{ \sequence{y_i}{i<n}: (\forall i<n)(y_i\in f(x_i)) \}$;
		\item [parallelization] $\parallelization{f}\pmfunction{\infStrings{X}}{\infStrings{Y}}$ with domain $\operatorname{dom}(\parallelization{f}):=\operatorname{dom}(f)^\mathbb{N}$ defined as $\parallelization{f}(\sequence{x_n}{n\in\mathbb{N}}):= \sequence{f(x_n)}{n\in\mathbb{N}}$;
		\item [jump] we define the \textdef{jump} of the represented space $(X,\repmap{X})$ as the represented space $X'=(X,\repmap{X'})$, where a $\repmap{X'}$-name for $x$ is a string $\coding{p_0,p_1,\hdots}$ s.t.\ $\repmap{X}(\lim_{n\to\infty} p_n)=x$. The jump of $f$ is defined as $\wjump{f}\pmfunction{X'}{Y}:=x\mapsto f(x)$. We write $f^{(n)}$ to denote the result of applying the jump operation $n$ times.
 	\end{description}
	We also define the \textdef{compositional product} as
	\[ f*g:=\max_{\le_{\mathrm{W}}}\{f_0\circ g_0: f_0\le_{\mathrm{W}} f \text{ and } g_0\le_{\mathrm{W}} g \}. \]
	Intuitively the compositional product captures the idea of applying first $g$, then using some computable operation on the output of $g$ and then feeding the result as an input for $f$. The fact that the compositional product is well-defined has been shown in \cite[Cor.\ 3.7]{BP16}. Notice that, by definition, $f*g$ is a Weihrauch degree and not a specific multivalued function. Nonetheless, with a small abuse of notation, we will write formulas such as $h\le_{\mathrm{W}} f* g$ with the obvious meaning. We also write $f^{[n]}$ to denote the $n$-fold compositional product of $f$ with itself, where $f^{[0]}:=\id{}$ and $f^{[1]}:=f$.

	We say that $f$ is a \textdef{cylinder} if $f\equiv_{\mathrm{sW}} \id{}\times f$, where $\id{}$ denotes the identity on the Baire space. The notion of cylinder is very useful because of the following
	\begin{unprovedproposition}[{\cite[Cor.\ 3.6]{BG09}}]
		For every multivalued functions $f$ and $g$, if $g$ is a cylinder then $f\le_{\mathrm{W}} g \iff f \le_{\mathrm{sW}} g$.
	\end{unprovedproposition}
	Cylinders are also useful to deal with the compositional product, thanks to the so-called \textdef{cylindrical decomposition}:
	\begin{unprovedproposition}[{\cite[Lem.\ 3.10]{BP16}}]
		For all $f,g$ and all cylinders $F, G$ with $F \equiv_{\mathrm{W}} f$ and $G \equiv_{\mathrm{W}} g$ there exists a computable $K$ such that $f*g\equiv_{\mathrm{W}} F\circ K \circ G$.
	\end{unprovedproposition}
	In particular, knowing that for every function $f$ we have that $f\equiv_{\mathrm{W}} \id{}\times f$ and that the latter is a cylinder, we can always take a representative of $f*g$ of the form $(\id{}\times f)\circ \Phi_e \circ (\id{}\times g)$ for some computable function $\Phi_e$.

	Finally we define the \textdef{total continuation} or \textdef{totalization} of $f$, written $\mathsf{T}f$, as the total multivalued function $\mathsf{T}f(x):=f(x)$ if $x\in\operatorname{dom}(f)$ and $\mathsf{T}f(x)=Y$ otherwise. Clearly $\mathsf{T}f = f$ iff $f$ is total. Notice that the definition of $\mathsf{T}f$ is sensitive to the particular definition of $f$ as a multivalued function between represented spaces. For a more detailed exposition we refer to \cite{BGCompOfChoice19}.

	Let us now define some well-known multivalued functions that will be useful in the development of the work:
	\begin{itemize}
		\item $ \mathsf{LPO} \colon{\mathbb{N}^\mathbb{N}} \to \{0,1\}$ is defined as $ \mathsf{LPO} (p):=1$ iff $(\exists n)(p(n)=0)$. It is often convenient to think of $ \mathsf{LPO} $ as the problem of finding a yes/no answer to a $\Sigma^{0,p}_1$ or $\Pi^{0,p}_1$ question.
		\item $\mathsf{lim}:\subseteq \infStrings{({\mathbb{N}^\mathbb{N}})}\to{\mathbb{N}^\mathbb{N}}:=\sequence{p_n}{n\in\mathbb{N}}\mapsto \lim_{n\to\infty} p_n$, where the domain of $\mathsf{lim}$ is the set of Cauchy sequences.
		\item $ \mathsf{NHA} \mfunction{{\mathbb{N}^\mathbb{N}}}{{\mathbb{N}^\mathbb{N}}}$ is defined as $ \mathsf{NHA} (p)=\{q: q\text{ is not hyperarithmetic in }p\}$.
		\item $\chi_{\Pi^1_1}\colon{\mathbb{N}^\mathbb{N}}\to\{ 0,1\}$ is the characteristic function of a $\Pi^1_1$-complete set. It is often convenient to think of $\chi_{\Pi^1_1}$ as the function that takes in input a tree on $\mathbb{N}$ and checks whether it is well-founded.
	\end{itemize}

	A central role is played by the choice problems: given a represented space $X$ we define $\codedChoice{\boldsymbol{\Gamma}}{}{X}\pmfunction{\boldsymbol{\Gamma}(X)}{X}$ as the multivalued function that chooses an element from a non-empty set $A\in \boldsymbol{\Gamma}(X)$. If $\boldsymbol{\Gamma}=\boldsymbol{\Pi}^0_1$ we simply write $\codedChoice{}{}{X}$. We also write $\codedUChoice{\boldsymbol{\Gamma}}{}{X}$ if the choice is restricted to singletons.

	Three choice problems that turned out to be very relevant to calibrate the strength of multivalued functions that corresponds to theorems around $\mathrm{ATR}_0$ (from the point of view of reverse mathematics) are $\mathsf{UC}_\Baire$, $\mathsf{C}_\Baire$ and $\mathsf{TC}_\Baire$. They have been explored in great detail in \cite{KMP20}. It is known that $\mathsf{lim}^{(n)}<_\mathrm{W}\mathsf{UC}_\Baire$ for every $n$ (see \cite[Sec.\ 6]{BdBPLow12}) and indeed $\mathsf{lim}^\dagger \equiv_{\mathrm{W}} \mathsf{UC}_\Baire$, where $\mathsf{lim}^\dagger$ corresponds to the iteration of $\mathsf{lim}$ over a countable ordinal (\cite{Pauly15ordinals}). Moreover $\mathsf{UC}_\Baire$ and $\mathsf{C}_\Baire$ are closed under compositional product (\cite[Thm.\ 7.3]{BdBPLow12}). In \cite{KMP20} it is proved that $\codedUChoice{\boldsymbol{\Sigma}^1_1}{}{{\mathbb{N}^\mathbb{N}}}\equiv_{\mathrm{W}}\mathsf{UC}_\Baire$ and $\codedChoice{\boldsymbol{\Sigma}^1_1}{}{{\mathbb{N}^\mathbb{N}}}\equiv_{\mathrm{W}} \mathsf{C}_\Baire$. The fact that $\mathsf{UC}_\Baire<_\mathrm{W}\mathsf{C}_\Baire$ follows from the fact that the element of a $\Sigma^1_1$ singleton is hyperarithmetic, but the hyperarithmetic functions are not a basis for the $\Pi^0_1$ predicates (see \cite[Thm.\ I.1.6 and thm.\ III.1.1]{SacksHRT}). In particular we have
	\begin{unprovedtheorem}[{\cite[Cor.\ 3.4]{KMP20}}]
		\thlabel{thm:ucbaire_hyperarithmetic_solution}
		Let $f\pmfunction{{\mathbb{N}^\mathbb{N}}}{X}$ be a (partial) multivalued function, for some represented space $X$. If $f\le_{\mathrm{W}} \mathsf{UC}_\Baire$ then, for every $x\in\operatorname{dom}(f)$, $f(x)$ contains some $y$ hyperarithmetic relative to $x$.
	\end{unprovedtheorem}

	The Weihrauch degree of $\mathsf{TC}_\Baire$ has been explored in \cite[Sec.\ 8]{KMP20}. It is known that $\mathsf{C}_\Baire <_\mathrm{W} \mathsf{TC}_\Baire$ (\cite[Prop.\ 8.2(1)]{KMP20}) and $\mathsf{TC}_\Baire^*$ is one of the strongest problem studied so far that is still considered among the ``$\mathrm{ATR}_0$ analogues''.

	We conclude this section with the following proposition.
	\begin{proposition}
		\thlabel{prop:product_with_NHA_general}
		Let $f\pmfunction{X}{Y}$ and $g\pmfunction{Z}{W}$ be multivalued functions between represented spaces and let $A\subset \operatorname{dom}(g)$ be s.t.\
		\[ \{ z\in\operatorname{dom}(g): (\forall w\in g(z))( w\text{ is not hyperarithmetic in } z ) \} \subset A. \]
		If $f\times  \mathsf{NHA} \le_{\mathrm{W}} g$ then $f\le_{\mathrm{W}} g\restrict{A}$.
	\end{proposition}
	\begin{proof}
		Assume $f\times \mathsf{NHA} \le_{\mathrm{W}} g$ and let the reduction be witnessed by the computable functions $\Phi,\Psi$. For every $p_x$ which is the name of some $x\in\operatorname{dom}(f)$, the pair $(p_x,p_x)$ is mapped via $\Phi$ to a name $p_z$ for some element $z\in\operatorname{dom}(g)$.

		It suffices to show that for every name $p_x$ of an element in the domain of $f$, the pair $(p_x,p_x)$ is mapped via $\Phi$ to a name $p_z$ of an element $z\in A$.

		If this were not the case then, for some $x\in\operatorname{dom}(f)$, $p_z$ is the name of some $z\notin A$. By hypothesis, there is a $w\in g(z)$ s.t.\ $w$ has a name $p_w$ which is hyperarithmetic in $p_z$. Let $G$ be a realizer of $g$ s.t.\ $p_w=G\Phi(p_x,p_x)$. Since $p_w$ is hyperarithmetic in $p_z$, and hence in $p_x$, we have reached a contradiction with the fact that $\Psi(p_w,p_x,p_x)$ computes a solution for $ \mathsf{NHA} (p_x)$.
	\end{proof}

	This result will often be used in combination with \thref{thm:ucbaire_hyperarithmetic_solution}. In fact if there is a computable $x\in \operatorname{dom}(f)$ s.t.\ $f(x)$ does not contain any hyperarithmetic element, then $f\not\equiv_{\mathrm{W}}\mathsf{UC}_\Baire$.

\section{Ramsey theorems}
\label{sec:ramsey}

The space ${[\mathbb{N}]}^\mathbb{N} $, endowed with the induced topology from the Baire space ${\mathbb{N}^\mathbb{N}}$ is computably isometric to ${\mathbb{N}^\mathbb{N}}$. There is actually a canonical choice for a computable bijection ${\mathbb{N}^\mathbb{N}}\to{[\mathbb{N}]}^\mathbb{N} $.

Let $P\subset{[\mathbb{N}]}^\mathbb{N} $. We say that $f$ is a \textdef{homogeneous solution for $P$} iff
\[ (\forall g\in{[\mathbb{N}]}^\mathbb{N} )(fg\in P) \lor (\forall g\in{[\mathbb{N}]}^\mathbb{N} )(fg\notin P). \]
If $f$ is homogeneous for $P$ we say that $f$ \textdef{lands in $P$} if the first disjunct holds, i.e.\ if $(\forall g\in{[\mathbb{N}]}^\mathbb{N} )(fg\in P)$. Vice versa, if $(\forall g\in{[\mathbb{N}]}^\mathbb{N} )(fg\notin P)$ then we say that $f$ \textdef{avoids $P$}. A set $P\subset{[\mathbb{N}]}^\mathbb{N} $ is called \textdef{Ramsey} (or we say that it has the \textdef{Ramsey property}) iff it has a homogeneous solution. We will denote the set of homogeneous solutions for $P$ (which may either land in it or avoid it) with $\mathrm{HS}(P)$. Notice that, in general, a set can have both solutions that land in the set and solutions that avoid the set.

In the literature, the symbol ${[\mathbb{N}]}^\mathbb{N} $ is sometimes used to denote the family of all infinite subsets of $\mathbb{N}$. Also, if $X$ is an infinite subset of $\mathbb{N}$, $[X]^\mathbb{N}$ denotes the family of all infinite subsets of $X$. It is easy to identify the Ramsey space ${[\mathbb{N}]}^\mathbb{N} $ with the space of infinite subsets of $\mathbb{N}$ (by identifying a function $f$ with its range). With this in mind, we may write $[f]^\mathbb{N}:=[\operatorname{ran}(f)]^\mathbb{N}$ to denote the set of all infinite subsequences of $f$. The definition of homogeneous solution can now be written as
\[ [f]^\mathbb{N}\subset P \lor [f]^\mathbb{N}\cap P = \emptyset. \]

It is natural to ask which classes of subsets of ${[\mathbb{N}]}^\mathbb{N} $ have the Ramsey property. The problem is well studied and has an extensive literature. The Galvin-Prikry theorem (\cite{GalvinPrikry73}) states that all Borel subsets of ${[\mathbb{N}]}^\mathbb{N} $ have the Ramsey property. This result can actually be extended to analytic sets (\cite{Silver70}). To go beyond the analytic sets we need axioms above ZFC (see e.g.\ \cite[Rem.\ VI.7.6, p.\ 240]{Simpson09}, \cite[pp.\ 1036--1037]{Kastanas83}). We will focus on Nash-Williams' theorem (\cite{NashWilliams65}), which states that open sets have the Ramsey property. This is also known as the open Ramsey theorem. It, in turn, implies the clopen Ramsey theorem (which is the restriction of Nash-Williams' theorem to clopen sets). As already mentioned, the open and clopen Ramsey theorems are known to be equivalent to $\mathrm{ATR}_0$ over $\mathrm{RCA}_0$ (see \cite[Thm.\ V.9.7]{Simpson09}).

\subsection{Some useful tools}
\label{subsec:tools}
Before formalizing the open and clopen Ramsey theorems in the context of
Weihrauch reducibility as multivalued functions, let us explicitly state
some properties of the set of homogeneous solutions that will turn out to be
useful in the rest of the paper. As a notational convenience we will use the
letters $P,Q,\hdots$ to denote open sets and $D,E,\hdots$ to denote clopen
sets.

\begin{proposition}
	\thlabel{prop:galvin_prikry_subset}
	Let $\boldsymbol{\Gamma}$ be a definable (boldface) pointclass that is downward closed with respect to Wadge reducibility (i.e.\ it is a downward closed family of Wadge degrees), such as the families of open and of clopen sets. Assume that every $P\in\boldsymbol{\Gamma}({[\mathbb{N}]}^\mathbb{N} )$ is Ramsey and that for every $f\in{[\mathbb{N}]}^\mathbb{N} $,
	\[ \boldsymbol{\Gamma}([f]^\mathbb{N}) = \{ P\cap [f]^\mathbb{N} : P \in \boldsymbol{\Gamma}({[\mathbb{N}]}^\mathbb{N} ) \}. \]
	Then for every $f\in{[\mathbb{N}]}^\mathbb{N} $, every $Q\in\boldsymbol{\Gamma}([f]^\mathbb{N})$ is Ramsey. Moreover if $P\in\boldsymbol{\Gamma}({[\mathbb{N}]}^\mathbb{N} )$ and $f\in{[\mathbb{N}]}^\mathbb{N} $ there exists $h\in\mathrm{HS}(P)$ s.t.\ $h\preceq f$.
\end{proposition}
\begin{proof}
	It is easy to see that every $f\in{[\mathbb{N}]}^\mathbb{N} $ induces a $f$-computable homeomorphism $\varphi_f\colon{[\mathbb{N}]}^\mathbb{N} \to[f]^\mathbb{N}$ defined as
	\[ \varphi_f(p):= n \mapsto f(p(n)). \]
	Notice also that
	\begin{equation*}\tag{$\star$}
		\varphi_f(h)g = fhg = \varphi_f(hg).
	\end{equation*}
	In particular this homeomorphism preserves subsequences, i.e.\ for every $q\preceq p$ we have $\varphi_f(q)\preceq \varphi_f(p)$.
	Fix $f\in{[\mathbb{N}]}^\mathbb{N} $ and let $Q\in\boldsymbol{\Gamma}([f]^\mathbb{N})$. Since $\boldsymbol{\Gamma}$ is closed under Wadge reducibility we have that
	\[ P:=\varphi_f^{-1}(Q)\in \boldsymbol{\Gamma}({[\mathbb{N}]}^\mathbb{N} ). \]
	Moreover, since every pointset in $\boldsymbol{\Gamma}({[\mathbb{N}]}^\mathbb{N} )$ has the Ramsey property, there is $h\in \mathrm{HS}(P)$. Using $(\star)$, it is straightforward to conclude that $\varphi_f(h)\in \mathrm{HS}(Q)$.

	For the second part it suffices to apply the first part to $Q:=[f]^\mathbb{N}\cap P$, which is in $\boldsymbol{\Gamma}([f]^\mathbb{N})$.
\end{proof}

\begin{proposition}
	\thlabel{prop:sets_with_disjoint_solutions}
	Let $A,B\subset \mathbb{N}$ be disjoint. Let $P,Q\in\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )$ be s.t.\
	\begin{enumerate}
		\item \label{itm:dsA} $(\forall f \in P)( f(0)\in A \text{ and } f(1) \in A);$
		\item \label{itm:dsB} $(\forall g \in Q)( g(0)\in B \text{ and } g(1) \in B).$
	\end{enumerate}
	If $R:=P \cup Q$ then
	\[ \mathrm{HS}(R)\cap R= (\mathrm{HS}(P)\cap P)\cup(\mathrm{HS}(Q)\cap Q). \]
\end{proposition}
\begin{proof}
	The inclusion $(\mathrm{HS}(P)\cap P)\cup(\mathrm{HS}(Q)\cap Q) \subset \mathrm{HS}(R)\cap R$ is trivial and always holds, so we only need to prove the converse direction. Let $h\in \mathrm{HS}(R)\cap R$ and assume that $h\in P$. By induction we can easily show that $\operatorname{ran}(h)\subset A$. Indeed, by point \ref{itm:dsA}, $h(0)\in A$ and $h(1)\in A$. Moreover, if $h(i)\in A$ then $h(i+1)\in A$ because $h$ lands in $R$: indeed if not then the substring $\coding{h(i), h(i+1), \hdots}$ of $h$ can neither be in $P$ nor in $Q$ (by the disjointness of $A$ and $B$), hence it cannot be in $R$, contradicting the fact that $h$ lands in $R$. This shows that $h\in P$ implies $h\in \mathrm{HS}(P)\cap P$. Notice also that, by the disjointness of $A$ and $B$, $\operatorname{ran}(h)\subset A$ implies $\operatorname{ran}(h)\cap B=\emptyset$ and therefore no subsequence of $h$ is in $Q$. Similarly we can show that $h\in \mathrm{HS}(R)\cap Q$ implies $h\in (\mathrm{HS}(Q)\cap Q)\backslash (\mathrm{HS}(P)\cap P)$ and therefore the claim follows.
\end{proof}

The following construction was used by Avigad \cite{Avigad98} in his proof of the open Ramsey theorem in $\mathrm{ATR}_0$.
\begin{definition}
	Let $P\in\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )$ and let $\coding{P}$ be a name for $P$. We can define the tree
	\[ \closedsidesoltree{\coding{P}}:= \{ \sigma \in {[\mathbb{N}]}^{<\mathbb{N}} : (\forall \tau\preceq^* \sigma)(\tau \not \in \coding{P} ) \}. \]
\end{definition}
\begin{lemma}
\thlabel{lem:solution_closed_side_iff_path_through_tree}
Let $P\in\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )$. For every name $\coding{P}$ of $P$ and every $f\in{[\mathbb{N}]}^\mathbb{N} $ we have
\[ f\in \mathrm{HS}(P)\backslash P \iff f\in [\closedsidesoltree{\coding{P}} ]. \]
\end{lemma}
\begin{proof}
	If $f\notin [\closedsidesoltree{\coding{P}}]$ then $(\exists n )(f[n]\notin \closedsidesoltree{\coding{P}})$, i.e.\ $(\exists n)(\exists \tau\preceq^* f[n])(\tau \in \coding{P})$.
	This implies that there exists a $g\preceq f$ s.t.\ $\tau \sqsubset g$. This shows that $g\in P$ and hence $f\notin\mathrm{HS}(P)\backslash{P}$.

	Let $f\in [\closedsidesoltree{\coding{P}}]$ and let $g\preceq f$. If $g\in P$ then $(\exists n)(g[n]\in \coding{P})$, contradicting the fact that $f\in [\closedsidesoltree{\coding{P}}]$ (by definition of $\closedsidesoltree{\coding{P}}$). Therefore we have that $f\in \mathrm{HS}(P)\backslash{P}$.
\end{proof}
Notice that the above lemma shows that $\mathrm{HS}(P)\backslash P$ is closed whenever $P$ is open. In particular, if $D$ is clopen then $\mathrm{HS}(D)$ is closed: indeed, letting
 $E:=\setcomplement[{[\mathbb{N}]}^\mathbb{N} ]{D}$, we have $\mathrm{HS}(D)=\mathrm{HS}(E)$ and
\[\mathrm{HS}(D)=(\mathrm{HS}(D)\cap D)\cup (\mathrm{HS}(D)\backslash D) = (\mathrm{HS}(E)\backslash E) \cup (\mathrm{HS}(D)\backslash D) \]
is the union of two closed sets.

On the other hand, the set of solutions for an open set $P$ that lands in $P$ can be $\Pi^1_1$-complete: let $\sequence{q_i}{i\in\mathbb{N}}$ be an enumeration of the rationals. We can define
\[ T:=\{\sigma\in{[\mathbb{N}]}^{<\mathbb{N}}  : (\forall i<\abslength{\sigma}-1)(q_{\sigma(i+1)}<_\mathbb{Q} q_{\sigma(i)} ) \}. \]
A path through $T$ is an infinite descending sequence in $\mathbb{Q}$. If we define $P:=\setcomplement[{[\mathbb{N}]}^\mathbb{N} ]{[T]}$ we have that $\mathrm{HS}(P)\cap P$ is the set of well-suborders of $\mathbb{Q}$ (every suborder of $\mathbb{Q}$ that is not a well-order contains an infinite descending sequence with increasing indexes, and therefore, a subsequence that lands in $[T]$) and hence is $\Pi^1_1$-complete.

This underlines a critical difference between the problem of finding a homogeneous solution that lands in $P$ and finding one that avoids $P$.

The following construction will be used in the following to move open sets around while ``preserving'' homogeneous solutions.
\begin{definition}
For every $n>1$ let $\operatorname{pow}_n:=i\mapsto n^{i+1}$. We
can define the map $\elementpower{n}\colon ({[\mathbb{N}]}^{<\mathbb{N}}  \cup {[\mathbb{N}]}^\mathbb{N}  ) \to
({[\mathbb{N}]}^{<\mathbb{N}}  \cup {[\mathbb{N}]}^\mathbb{N}  )$ as
\[ \elementpower{n}(f):= \operatorname{pow}_n \circ f = i \mapsto n^{f(i)+1}. \]
It is clear that $\elementpower{n}$ is a computable injection with computable inverse.

Let $P\in\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )$ and let $\coding{P}$ be a name for $P$. We can define (with a small abuse of notation)
	\[ \elementpower{n}{(\coding{P})}:=\bigcup_{\sigma\in\coding{P}} \{ f\in {[\mathbb{N}]}^\mathbb{N}  : \elementpower{n}(\sigma)\sqsubset f \}.  \]
We can naturally extend the definition to a multivalued map $\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )   \rightrightarrows \boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )$ defining
	\[ \elementpower{n}(P):= \left\{ \elementpower{n}(\coding{P}) : \coding{P} \text{ is a name of }P \right\}.  \]
\end{definition}

\begin{lemma}
	\thlabel{lem:elementpower_preserves_solutions}
	Let $P\in \boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )$. Fix $n>1$ and let $Q:=\elementpower{n}(\coding{P})$ for some name $\coding{P}$ of $P$. Then
	\[ f\in \mathrm{HS}(P)\cap P \Leftrightarrow \elementpower{n}(f) \in \mathrm{HS}(Q)\cap Q. \]
\end{lemma}
\begin{proof}
	It is straightforward to see that, for every $f\in {[\mathbb{N}]}^\mathbb{N} $, $f\in P$ iff  $\elementpower{n}(f)\in Q$. Moreover, if $g\in{[\mathbb{N}]}^\mathbb{N} $, then
		\[ \elementpower{n}(f)g = i \mapsto n^{fg(i)+1} = \elementpower{n}(fg). \]

	If $f$ is a homogeneous solution that lands in $P$ then $\elementpower{n}(f)g \in Q$ for every $g\in {[\mathbb{N}]}^\mathbb{N} $, i.e.\ $\elementpower{n}(f)\in \mathrm{HS}(Q)\cap Q$. Vice versa, if $\elementpower{n}(f)\in \mathrm{HS}(Q)\cap Q$ then for every $g\in{[\mathbb{N}]}^\mathbb{N} $ we have $\elementpower{n}(f)g=\elementpower{n}(fg)\in Q$, which implies $fg\in P$.
\end{proof}

\begin{definition}
	Let $\sigma,\tau\in{[\mathbb{N}]}^{<\mathbb{N}} $. We define $\sigma\boxtimes \tau$ to be the set of all strings of the form $\coding{(\rho(i),\theta(i)): i<N }$ where $\rho,\theta\in{[\mathbb{N}]}^{<\mathbb{N}} $ and s.t.\
	\[ \sigma \sqsubseteq\rho \land \tau \sqsubseteq\theta \land N=\max\{\abslength{\sigma},\abslength{\tau}\}. \]
	Clearly the map $\boxtimes$ can be extended to infinite strings by defining
	\[ f\boxtimes g := \coding{ (f(0), g(0)), (f(1),g(1)), \hdots }. \]

	For the sake of readability, it is convenient to introduce the following notation: for $i=1,2$,  we define
	\[ \pi_i: (\mathbb{N}\times\mathbb{N})^{<\mathbb{N}}\cup (\mathbb{N}\times\mathbb{N})^{\mathbb{N}}\to {\mathbb{N}^{<\mathbb{N}}} \cup {\mathbb{N}^\mathbb{N}} \]
	as the map that, given in input a finite (resp.\ infinite) string of pairs, returns the finite (resp.\ infinite) string of the $i$-th elements of the pairs.

	Let $\coding{P},\coding{Q}$ be two names for two open subsets of ${[\mathbb{N}]}^\mathbb{N} $. We can define
	\[ \coding{P}\boxtimes \coding{Q} := \bigcup_{\sigma\in\coding{P}}\bigcup_{\tau\in\coding{Q}} \sigma \boxtimes \tau, \]
	which is a name for a new open set.

	This leads to a map $\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )\times\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} ) \rightrightarrows \boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )$ defined by
	\[ P\boxtimes Q := \{ R\in\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} ): \coding{P}\boxtimes\coding{Q} \text{ is a name for } R \}.  \]
\end{definition}

Notice that, in general, it is not true that if $f$ lies in the open set with name $\coding{P}\boxtimes\coding{Q}$ then $\pi_i f\in {[\mathbb{N}]}^\mathbb{N} $.

\begin{lemma}
	\thlabel{lem:opencodepairing_properties}
	Let $P_1,P_2\in\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )$ and let $\coding{P_1},\coding{P_2}$ be names for $P_1,P_2$ respectively s.t.\ every string in $\coding{P_1}$ has length at least $2$. Let $P\in\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )$ be the open set with name $\coding{P_1}\boxtimes\coding{P_2}$. Then
	\[ \mathrm{HS}(P)\cap P = \{ f\boxtimes g: f\in \mathrm{HS}(P_1)\cap P_1 \text{ and } g\in \mathrm{HS}(P_2)\cap P_2\}. \]
\end{lemma}
\begin{proof}
	Notice first of all that $f\in \mathrm{HS}(P)\cap P$ implies that, for $i=1,2$,
	\[  \pi_i f \in {[\mathbb{N}]}^\mathbb{N} .\]
	Indeed, fix $n\in\mathbb{N}$ and consider the substring $g:=\coding{f(n), f(n+1),\hdots}$ of $f$. Since $f$ is homogeneous we have $g\in P$. In particular, there is $\tau=\coding{(\tau_1(i),\tau_2(i)): i<N } \in \coding{P_1}\boxtimes\coding{P_2}$ s.t.\ $\tau\sqsubset g$. Fix $\sigma_1\in \coding{P_1}$ and $\sigma_2\in\coding{P_2}$ s.t.\ $\tau \in \sigma_1\boxtimes\sigma_2$. Since $\abslength{\sigma_1}\ge 2$ we have $\abslength{\tau}\ge 2$. Moreover
		\[ (\pi_i f)(n) = \tau_i(0) < \tau_i(1) =(\pi_i f)(n+1). \]
	Let now $f\in \mathrm{HS}(P)\cap P$. For every $g\preceq f$ we have that $g\in \mathrm{HS}(P)\cap P$ and $\pi_1 g\in P_1$, $\pi_2 g \in P_2$ (indeed if $\pi_1 g \notin P_1$ or $\pi_2 g \notin P_2$ then $g\notin P$). Hence  $\pi_i f\in \mathrm{HS}(P_i)\cap P_i$ for $i=1,2$. The reverse inclusion is straightforward as if $f_i\in \mathrm{HS}(P_i)\cap P_i$ then $f:= f_1 \boxtimes f_2$ is a homogeneous solution for $P$.
\end{proof}

The following generalizes the tree used by Solovay \cite{Solovay78}.

\begin{definition}
	\thlabel{def:solovay_open}
Let $\phi\colon\mathbb{N}\to\mathbb{N}$ be injective. For every tree $T\in \mathbf{Ti}$ we define the \textdef{Solovay open set $\solovay{\phi}(T) $} as
\begin{align*}
	\solovay{\phi}(T) := \{ f\in {[\mathbb{N}]}^\mathbb{N}  : {}&{} (\exists k)(\forall \tau \trianglelefteq f[k])(\tau \notin T ) \text{ and }\\
	& (\exists n,m\in\mathbb{N})(f(0)= \phi(n) \text{ and } f(1)=\phi(m))\}.
\end{align*}
If $\phi$ is the identity function we drop the subscript.
\end{definition}

It is easy to see that $\solovay{\phi}(T)$ is an open set.

\begin{lemma}
\thlabel{lem:solutions_solovay_open_set}
Let $T\in \mathbf{Ti}$ and let $W:=\solovay{\phi}(T)$. Then
\begin{enumerate}
	\item \label{itm:solovay_wf_tree} If $[T]=\emptyset$ then $\mathrm{HS}(W)\cap W\neq \emptyset$. Moreover, if $\phi$ is surjective then $W={[\mathbb{N}]}^\mathbb{N} $ and therefore $\mathrm{HS}(W) = \mathrm{HS}(W)\cap W = {[\mathbb{N}]}^\mathbb{N} $.
	\item \label{itm:solovay_if_tree} If $[T]\neq\emptyset$ then $\mathrm{HS}(W) = \mathrm{HS}(W)\backslash{W}$. Moreover every $f\in \mathrm{HS}(W)$ dominates a path through $T$.
\end{enumerate}
\end{lemma}
\begin{proof}
For each $f\in{[\mathbb{N}]}^\mathbb{N} $ define the tree
\[ T_f := \{ \sigma \in T : (\forall i<\abslength{\sigma})(\sigma(i)\le f(i)) \}.\]
\begin{description}
	\item[\ref{itm:solovay_wf_tree}] Notice that, for every $f\in{[\mathbb{N}]}^\mathbb{N} $, the set $T_f$ is a finitely-branching well-founded subtree of $T$. By K\"onig's lemma, $T_f$ must be finite and therefore there is a $k$ s.t.\ every string in $T_f$ has length $<k$. This implies that every $\tau \trianglelefteq f[k]$ is not in $T$. If $\operatorname{ran}(f)\subset\operatorname{ran}(\phi)$ (as is always the case if $\phi$ is surjective) then $f\in\mathrm{HS}(W) \cap W$ .
	\item[\ref{itm:solovay_if_tree}] Notice that $\mathrm{HS}(W)\cap W=\emptyset$ because for every path $x\in [T]$ and every $f\in{[\mathbb{N}]}^\mathbb{N} $, there exists $g\in{[\mathbb{N}]}^\mathbb{N} $ that grows sufficiently quickly s.t.\ $x \trianglelefteq fg$ (as proved in \cite[p.\ 108]{Solovay78}).

	Moreover, if $f\in \mathrm{HS}(W)\backslash{W}$ then $(\forall k)(\exists \tau \trianglelefteq f[k])(\tau \in T)$. This implies that $T_f$ is infinite and therefore, by K\"onig's lemma, $[T_f]\neq\emptyset$. This concludes the proof as $[T_f]\subset [T]$.\qedhere
\end{description}
\end{proof}

\begin{definition}
Let $\phi\colon\mathbb{N}\to\mathbb{N}$. For every tree $T\in \mathbf{Ti}$ we
define the clopen set $\describepath{\phi}(T)$ as
\begin{align*}
	\describepath{\phi}(T) := \{ f\in [\mathbb{N}]^{\mathbb{N}} : (\exists \sigma_0,\sigma_1\in T) (\, & f(0)=\phi(\coding{\sigma_0}) \text{ and } \\
		& f(1)=\phi(\coding{\sigma_1}) \text{ and } \sigma_0\sqsubset \sigma_1) \}.
\end{align*}
If $\phi$ is the identity function we just drop the subscript.
\end{definition}

\begin{lemma}
	\thlabel{lem:clopen_describes_paths} Let $T\in\mathbf{Ti}$ and let
$D:=\describepath{\phi}(T)$ for some computable strictly increasing function
$\phi\colon\mathbb{N}\to\mathbb{N}$. If $[T]\neq\emptyset$ then $\mathrm{HS}(D)\cap D\neq \emptyset$ and there is a uniform computable surjection $\mathrm{HS}(D)\cap D \to [T]$. On the other hand, if $[T]=\emptyset$
then $\mathrm{HS}(D)\cap D=\emptyset$.
\end{lemma}
\begin{proof}
	Let $y\in [T]$ and define $h\in D$ s.t.\ $h(i)=\phi(\coding{y[i]})$. It is easy to see that $h$ is an homogeneous solution for $D$ landing in $D$, therefore $\mathrm{HS}(D)\cap D \neq \emptyset$. Moreover, given any $f$ that lands in $D$ we can compute a path $x$ through $T$ as
	\[ x := \bigcup_{k\in\mathbb{N}} \phi^{-1}f(k). \]
	Indeed, since $f$ lands in $D$ we have that $\phi^{-1}f(k)\in T$ for every $k\in\mathbb{N}$. Moreover, for every $k$, $\coding{f(k),f(k+1),\hdots}\in D$ so that $\phi^{-1}f(k+1)$ is a finite string that properly extends $\phi^{-1}f(k)$. Therefore $x$ is a well-defined function $\mathbb{N}\to\mathbb{N}$. Finally it is easy to see that $x\in [T]$: for every $i$, let $j>i$ s.t.\ there is a $k$ s.t.\ $x[j]=\phi^{-1}f(k)$. By definition of $D$ we have that $\phi^{-1}f(k)\in T$. Since $T$ is a tree, we can conclude that $x[i]\in T$. Notice that $\phi^{-1}$ is computable, therefore $x$ is computable from $f$. Notice also that, if $y$ and $h$ are as in the beginning of this proof, then $y = \bigcup_{k\in\mathbb{N}}\phi^{-1}h(k)$, which proves that the mapping is a surjection.

	On the other hand, if $[T]=\emptyset$ then, for every $f\in D$, there is an $i$ s.t.\ $\phi^{-1}(f(i))\notin T$ or $\phi^{-1}(f(i))\not\sqsubset \phi^{-1}(f(i+1))$, otherwise we could compute a path through $T$. In any case if $f\in D$ then it is not a homogeneous solution for $D$.
\end{proof}

\begin{lemma}
\thlabel{lem:computable_operations}
The following maps are computable:
\begin{enumerate}
	\item \label{itm:comp_tree} $\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )\to\boldsymbol{\Pi}^0_1({[\mathbb{N}]}^\mathbb{N} ):=P\mapsto\mathrm{HS}(P)\backslash{P} $;
	\item \label{itm:elem_power} $ \elementpower{n}\mfunction{\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )}{\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )}:=P\mapsto\elementpower{n}(P)$, for every $n\in\mathbb{N}$;
	\item \label{itm:opencode_pairing} $\boxtimes\mfunction{\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )\times\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )}{\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )}:=(P,Q)\mapsto P\boxtimes Q$;
	\item \label{itm:solovay_closed} $\solovay{\phi}\colon\mathbf{Ti}\to\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} ):=T\mapsto \solovay{\phi}(T)$, for every injective map $\phi\colon\mathbb{N}\to\mathbb{N}$ with computable range;
	\item \label{itm:path_description} $\describepath{\phi}\colon\mathbf{Ti}\to\boldsymbol{\Delta}^0_1({[\mathbb{N}]}^\mathbb{N} ):=T\mapsto \describepath{\phi}(T)$, for every invertible map $\phi\colon\mathbb{N}\to\mathbb{N}$ with computable inverse.
\end{enumerate}
\end{lemma}
\begin{proof}
${}$
\begin{description}
	\item[\ref{itm:comp_tree}] Let $P\subset {[\mathbb{N}]}^\mathbb{N} $ be open and let $\coding{P}$ be a name for $P$. The definition of $\closedsidesoltree{\coding{P}}$ is computable in $\coding{P}$. Moreover, $x\in [\closedsidesoltree{\coding{P}}]$ iff $x\in \mathrm{HS}(P)\backslash{P}$ (see \thref{lem:solution_closed_side_iff_path_through_tree}). Since a name for $A\in\boldsymbol{\Pi}^0_1({[\mathbb{N}]}^\mathbb{N} )$ can be a tree $T$ s.t.\ $A=[T]$, the claim follows.
	\item[\ref{itm:elem_power}, \ref{itm:opencode_pairing}] Straightforward from the definition.
	\item[\ref{itm:solovay_closed}] Let $T\in \mathbf{Ti}$ be represented by its characteristic function $\charfun{T}$. We can define
	\begin{align*}
		\coding{\solovay{\phi}(T)} := \{ \sigma\in {[\mathbb{N}]}^{<\mathbb{N}}  : {}&{} (\forall \tau \trianglelefteq \sigma)(\tau \notin T) \text{ and }\\
		& (\exists n,m\in\mathbb{N})(\sigma(0)= \phi(n) \text{ and } \sigma(1)=\phi(m))\}.
	\end{align*}
	Notice that the universal quantifier is bounded, while the formula in the scope of the existential quantifier is equivalent to requiring that $\sigma(0)$ and $\sigma(1)$ are in $\operatorname{ran}(\phi)$, which is computable by hypothesis. Therefore $\coding{\solovay{\phi}(T)}$ is computable in $T$.
	\item[\ref{itm:path_description}] Let $T\in \mathbf{Ti}$. By definition of $\describepath{\phi}(T)$, the basic clopen cone $\{f\in{[\mathbb{N}]}^\mathbb{N} : \tau\sqsubset f \}$ is a subset of $\describepath{\phi}(T)$ iff
	\[ \phi^{-1}\tau(0)\in T \text{ and }\phi^{-1}\tau(1)\in T \text{ and }\phi^{-1}\tau(0)\sqsubset \phi^{-1}\tau(1).\]
	In particular, this shows that we can $T$-computably obtain open names for $\describepath{\phi}(T)$ and its complement. \qedhere
\end{description}
\end{proof}

\section{Ramsey theorems in the Weihrauch lattice}
\label{sec:rt_wei}
\subsection{Definitions}
There are several ways to formalize the open Ramsey theorem as a multivalued function.
\begin{definition}[Open Ramsey Theorem]
\label{def:openRT}
 We define the \textdef{full version} of the open Ramsey theorem as the (total) multivalued function
\[ \boldfaceSigma^0_1\mathsf{-RT}\mfunction{\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )}{{[\mathbb{N}]}^\mathbb{N} } := P \mapsto \mathrm{HS}(P).\]
We may modify the full version by adding the requirement on ``which side" we want the solution to be in. In this case, however, we need to restrict the domain to the family of open sets that admit a solution. We can define the \textdef{strong versions} of the open Ramsey theorem as the multivalued functions $\mathsf{FindHS}_{\boldfaceSigma^0_1} , \mathsf{FindHS}_{\boldfacePi^0_1} \pmfunction{\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )}{{[\mathbb{N}]}^\mathbb{N} }$ with domain respectively
\[ \operatorname{dom}(\mathsf{FindHS}_{\boldfaceSigma^0_1} ):=\{P\in \boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} ) : \mathrm{HS}(P)\cap P \neq \emptyset\}, \]
\[ \operatorname{dom}(\mathsf{FindHS}_{\boldfacePi^0_1}):=\{P\in \boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} ) : \mathrm{HS}(P)\backslash P \neq \emptyset \} \]
and defined as $\mathsf{FindHS}_{\boldfaceSigma^0_1} (P):= \mathrm{HS}(P)\cap P$ and $\mathsf{FindHS}_{\boldfacePi^0_1}(P):= \mathrm{HS}(P)\backslash P$.
We may strengthen further the requirements, defining the \textdef{weak versions} of the open Ramsey theorem: namely we define $\mathsf{wFindHS}_{\boldfaceSigma^0_1} $ as the restriction of $\mathsf{FindHS}_{\boldfaceSigma^0_1} $ to
\[ \operatorname{dom}(\mathsf{wFindHS}_{\boldfaceSigma^0_1} ):=\{ P \in \boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} ) : \mathrm{HS}(P)\subset P \}. \]
Similarly we can define the weak version of $\mathsf{FindHS}_{\boldfacePi^0_1}$ as the multivalued function $\mathsf{wFindHS}_{\boldfacePi^0_1}$ obtained by restricting $\mathsf{FindHS}_{\boldfacePi^0_1}$ to
\[ \operatorname{dom}(\mathsf{wFindHS}_{\boldfacePi^0_1}):=\{ P \in \boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} ) : \mathrm{HS}(P)\cap P =\emptyset \}. \]
\end{definition}

Recall that, in general, an open set can have both solutions that land in the set and solutions that avoid the set. The domain of $\mathsf{wFindHS}_{\boldfaceSigma^0_1} $ (resp.\ $\mathsf{wFindHS}_{\boldfacePi^0_1}$) is therefore strictly smaller than the domain of $\mathsf{FindHS}_{\boldfaceSigma^0_1} $ (resp.\ $\mathsf{FindHS}_{\boldfacePi^0_1}$). As we will see the two versions exhibit very different behaviors. Notice also that the weak versions are restrictions of $\boldfaceSigma^0_1\mathsf{-RT}$, while the strong versions are not (the set of solutions can be strictly smaller).

As in the case of the open Ramsey theorem, we can consider different multivalued functions corresponding to the clopen Ramsey theorem.
\begin{definition}[Clopen Ramsey Theorem]
We define the full version of the clopen Ramsey theorem as the multivalued function $\boldfaceDelta^0_1\mathsf{-RT}\mfunction{\boldsymbol{\Delta}^0_1({[\mathbb{N}]}^\mathbb{N} )}{{[\mathbb{N}]}^\mathbb{N} }:= D\mapsto \mathrm{HS}(D)$.

The strong version of the clopen Ramsey theorem is the multivalued function
	\[ \mathsf{FindHS}_{\boldfaceDelta^0_1}\pmfunction{\boldsymbol{\Delta}^0_1({[\mathbb{N}]}^\mathbb{N} )}{{[\mathbb{N}]}^\mathbb{N} }:=D\mapsto \mathrm{HS}(D)\cap D\]
with domain
	\[ \operatorname{dom}(\mathsf{FindHS}_{\boldfaceDelta^0_1}):=\{ D\in\boldsymbol{\Delta}^0_1({[\mathbb{N}]}^\mathbb{N} )  : \mathrm{HS}(D)\cap D \neq \emptyset \}. \]

The weak version of the clopen Ramsey theorem is the multivalued function $\mathsf{wFindHS}_{\boldfaceDelta^0_1}\pmfunction{\boldsymbol{\Delta}^0_1({[\mathbb{N}]}^\mathbb{N} )}{{[\mathbb{N}]}^\mathbb{N} }$ defined as the restriction of $\mathsf{FindHS}_{\boldfaceDelta^0_1}$ to
	\[ \operatorname{dom}(\mathsf{wFindHS}_{\boldfaceDelta^0_1}):=\{ D \in \boldsymbol{\Delta}^0_1({[\mathbb{N}]}^\mathbb{N} ): \mathrm{HS}(D) \subset D\}. \]
\end{definition}

Notice that we defined only one strong and one weak version of the clopen Ramsey theorem. This is because, using \thref{lem:computable_operations_open}.\ref{itm:compl_clopen_set}, it is straightforward to see that the other two are (strongly) Weihrauch equivalent to the ones we defined.

\subsection{Problems reducible to  \texorpdfstring{$\mathsf{UC}_\Baire$}{\mathsf{UC}}}
\label{subsec:ucbaire}

We show that $\mathsf{wFindHS}_{\boldfaceSigma^0_1} $, $\mathsf{wFindHS}_{\boldfaceDelta^0_1}$ and $\boldfaceDelta^0_1\mathsf{-RT}$ are all Weihrauch equivalent to $\mathsf{UC}_\Baire$. None of these principles are strongly Weihrauch equivalent to $\mathsf{UC}_\Baire$, as we will show in \thref{thm:strong_wei_characterization}.

\begin{lemma}
\thlabel{thm:open<ucbaire}
$ \mathsf{wFindHS}_{\boldfaceSigma^0_1}  \le_{\mathrm{W}} \mathsf{UC}_\Baire $.
\end{lemma}
\begin{proof}
	Since ${ \mathsf{ATR} } \equiv_{\mathrm{W}} \mathsf{UC}_\Baire$ \cite{KMP20} it suffices to prove that  $\mathsf{wFindHS}_{\boldfaceSigma^0_1} \le_{\mathrm{W}}{ \mathsf{ATR} }$. Here we use the formulation of ${ \mathsf{ATR} }$ given in \cite{gohatr}, namely ${ \mathsf{ATR} }$ is defined as the function ${ \mathsf{ATR} } : \mathrm{WO}\times {2^\mathbb{N}} \times \mathbb{N} \to {2^\mathbb{N}}$ mapping a countable well-order $L$, a set $A\subset \mathbb{N}$ and (a code for) an arithmetic formula $\theta(n,W,V)$ to the unique set $Y\subset \mathbb{N}$ satisfying $\mathrm{H}_\theta(L,Y,A)$, where $\mathrm{H}_\theta(X,S,T)$ is the arithmetic formula defined in \cite[Def.\ V.2.2]{Simpson09}, asserting that $X$ is a linear order and $S$ is the result of iterating $\theta$ along $X$ with parameter $T$.
	The proof is the direct translation in the context of Weihrauch reducibility of the proof presented in \cite[Lem.\ V.9.4]{Simpson09}. More details on the construction can be found in the paper where the proof was first presented, i.e.\ \cite[Sec.\ 3]{Avigad98}. Let $P\in\operatorname{dom}(\mathsf{wFindHS}_{\boldfaceSigma^0_1} )$. The proof consists of four steps:
	\begin{enumerate}
		\item \label{item:or1} build the tree $T:=\closedsidesoltree{\coding{P}}$ of homogeneous solutions that avoid $P$;
		\item \label{item:or2} build $\mathrm{KB}(T)$;
		\item \label{item:or3} via arithmetic transfinite recursion along $\mathrm{KB}(T)$, obtain a sequence of infinite sets $\sequence{U_\sigma}{\sigma\in T}$ s.t.\ $U_\sigma \backslash U_\tau$ is finite whenever $\tau \le_{\mathrm{KB}(T)} \sigma$, and classify each $\sigma \in {[\mathbb{N}]}^{<\mathbb{N}} $ as ``good'' or ``bad'';
		\item \label{item:or4} use this classification to build a solution $f$.
	\end{enumerate}
	Notice that steps \ref{item:or1} and \ref{item:or2} are computable (using \thref{lem:computable_operations}.\ref{itm:comp_tree}). For $\sigma\notin T$, we classify $\sigma$ as good if the shortest prefix of $\sigma$ which is not in $T$ belongs to $\coding{P}$, and bad otherwise. For $\sigma\in T$, to define $U_\sigma$ and classify $\sigma$ as good or bad, we first define an infinite set $V_\sigma$ as follows:
	\begin{itemize}
		\item if $\sigma$ is the minimum of $\mathrm{KB}(T)$ then $V_\sigma := \mathbb{N}$;
		\item if $\sigma$ is the successor of $\tau$ in $\mathrm{KB}(T)$ then $V_\sigma := U_\tau$;
		\item if $\sigma$ is a limit in $\mathrm{KB}(T)$ then we define $V_\sigma$ by diagonal intersection: we computably and uniformly find a sequence $\tau_j$ cofinal in $\sigma$. Define
			  \[ \begin{gathered} 	u_0 := \min U_{\tau_0}; \\
								  u_{i+1} :=\min \left\{ \bigcap_{j\le i} U_{\tau_j}\backslash\{u_j\}\right\};\\
								  V_\sigma := \{ u_i: i\in\mathbb{N}\}. \end{gathered} \]
	\end{itemize}
	It is easy to verify that $V_\sigma$ is defined by an arithmetic formula. Let
	\[V_\sigma^1:= \{ m\in V_\sigma : \sigma\raisebox{.9ex}{\ensuremath\smallfrown}  m \text{ is good}\},\]
	and similarly $V_\sigma^0:= \{ m\in V_\sigma : \sigma\raisebox{.9ex}{\ensuremath\smallfrown}  m \text{ is bad}\} = V_\sigma \backslash V_\sigma^1$. Set
	\[ n \in U_\sigma :\Leftrightarrow ( |V_\sigma^1|=\infty \text{ and } n \in V_\sigma^1) \text{ or } (|V_\sigma^1|<\infty \text{ and } n \in V_\sigma^0 ). \]
	We now classify $\sigma$ as good if $V^1_\sigma$ is infinite, and bad otherwise.

	We can obtain the information about $\sequence{U_\sigma}{\sigma\in T}$ and the goodness (or badness) for each $\sigma\in T$ as a name for $Y\in { \mathsf{ATR} }(\mathrm{KB}(T),P,\theta)$, for an appropriate arithmetic formula $\theta$.

	As in \cite{Simpson09,Avigad98}, one can show that $\coding{}$ is good and compute a solution $f\in \mathsf{wFindHS}_{\boldfaceSigma^0_1} (P)$ from $Y$.
\end{proof}

\begin{lemma}
\thlabel{thm:ucbaire<clopen}
$ \mathsf{UC}_\Baire \le_{\mathrm{W}} \mathsf{wFindHS}_{\boldfaceDelta^0_1}$.
\end{lemma}
\begin{proof}
We follow the proof of the fact that the clopen Ramsey theorem implies $\text{ATR}_0$ over $\text{RCA}_0$ presented in \cite[Lem.\ V.9.6]{Simpson09}. We actually prove the reduction $\mathbf{\boldfaceSigma^1_1\mathsf{-Sep}} \le_{\mathrm{W}} \mathsf{wFindHS}_{\boldfaceDelta^0_1}$, as the equivalence $\mathbf{\boldfaceSigma^1_1\mathsf{-Sep}}\equiv_{\mathrm{W}} \mathsf{UC}_\Baire$ has been proved in \cite{KMP20}.

Let $\sequence{(T^0_k,T^1_k)}{k\in\mathbb{N}}$ be a sequence of pairs of trees s.t.\ for all $k$ at most one of $T^0_k$ and $T^1_k$ has a path (i.e.\ the sequence is a valid input for $\mathbf{\boldfaceSigma^1_1\mathsf{-Sep}}$). Our goal is to find a set $Z$ s.t.\ if $T^0_k$ has a path then $k\in Z$ and if $T^1_k$ has a path then $k\notin Z$.

Following \cite{Simpson09}, we can uniformly compute from $\sequence{(T^0_k,T^1_k)}{k\in\mathbb{N}}$ a name for a clopen $D\in\operatorname{dom}(\mathsf{wFindHS}_{\boldfaceDelta^0_1})$ s.t.\ for every $f\in \mathsf{wFindHS}_{\boldfaceDelta^0_1}(D)$, $f$ and $\sequence{(T^0_k,T^1_k)}{k\in\mathbb{N}}$ uniformly compute some $Z\in \mathbf{\boldfaceSigma^1_1\mathsf{-Sep}}(\sequence{(T^0_k,T^1_k)}{k\in\mathbb{N}})$.
\end{proof}

\begin{theorem}
\thlabel{cor:wfindclopen=ucbaire}
$\mathsf{UC}_\Baire \equiv_{\mathrm{W}} \mathsf{wFindHS}_{\boldfaceSigma^0_1}  \equiv_{\mathrm{W}} \mathsf{wFindHS}_{\boldfaceDelta^0_1}$.
\end{theorem}
\begin{proof}
This follows from \thref{thm:open<ucbaire}, \thref{thm:ucbaire<clopen} and the fact that $\mathsf{wFindHS}_{\boldfaceDelta^0_1}$ is the restriction of $\mathsf{wFindHS}_{\boldfaceSigma^0_1} $ to clopen sets.
\end{proof}

\begin{theorem}
\thlabel{thm:ucbaire=clopenramsey}
$\mathsf{UC}_\Baire \equiv_{\mathrm{W}} \boldfaceDelta^0_1\mathsf{-RT}$.
\end{theorem}
\begin{proof}
By \thref{cor:wfindclopen=ucbaire} it suffices to prove that $\mathsf{wFindHS}_{\boldfaceDelta^0_1}\equiv_{\mathrm{W}} \boldfaceDelta^0_1\mathsf{-RT}$. The
reduction $\mathsf{wFindHS}_{\boldfaceDelta^0_1} \le_{\mathrm{W}} \boldfaceDelta^0_1\mathsf{-RT}$ is trivial (the former
is a restriction of the latter).

Let us prove the reverse reduction. By \thref{prop:galvin_prikry_subset}, for every open
$P\subset{[\mathbb{N}]}^\mathbb{N} $, if $f\notin \mathrm{HS}(P)$ then there is a $g\preceq f$
s.t.\ $g\in \mathrm{HS}(P)$. This implies that the set $\setcomplement[{[\mathbb{N}]}^\mathbb{N} ]{\mathrm{HS}(P)}$ has no homogeneous
solution that lies in itself.

Let $D\in \boldsymbol{\Delta}^0_1({[\mathbb{N}]}^\mathbb{N} )$ and fix a name $\coding{p,q}$ for $D$. Consider the set
\[ E:= \{ f\in{[\mathbb{N}]}^\mathbb{N}  : (\exists \sigma,\tau\in p)(\sigma\raisebox{.9ex}{\ensuremath\smallfrown} \tau \sqsubset f) \lor (\exists \sigma,\tau\in q)(\sigma\raisebox{.9ex}{\ensuremath\smallfrown} \tau \sqsubset f)\}. \]
It is clear that $E$ is a clopen set and a name for $E$ is computable from $\coding{p,q}$.

Notice also that $\mathrm{HS}(D) \subset E$. Indeed, let $f$ be a homogeneous
solution for $D$ and assume first that $f\in D$. Since $D$ is open there
must be a $\sigma\in p$ s.t.\ $\sigma\sqsubset f$. Moreover,
since $f$ is a homogeneous solution,
$g:=\coding{f(\abslength{\sigma}), f(\abslength{\sigma}+1),\hdots}$ must
again be in $D$, hence there must be a $\tau\in p$ s.t.\ $\tau \sqsubset g$. This implies that $\sigma\raisebox{.9ex}{\ensuremath\smallfrown} \tau \sqsubset f$, i.e.\
$f\in E$. The case $f\in \setcomplement[{[\mathbb{N}]}^\mathbb{N} ]{D}$ is analogous by
replacing $D$ with $\setcomplement[{[\mathbb{N}]}^\mathbb{N} ]{D}$.

Moreover we can notice that there are no homogeneous solutions that land in
$\setcomplement[{[\mathbb{N}]}^\mathbb{N} ]{E}$, i.e.\ $E\in\operatorname{dom}(\mathsf{wFindHS}_{\boldfaceDelta^0_1})$. Indeed assume that $f$ avoids $E$ and let $\sigma,\tau\in{[\mathbb{N}]}^{<\mathbb{N}} $ be s.t.\ $\sigma\raisebox{.9ex}{\ensuremath\smallfrown} \tau \sqsubset f$ and $\sigma\in p$ and $\tau\in q$ (the case in which $\tau\in p$ and $\sigma\in q$ is analogous). Let also $g:=\coding{f(\abslength{\sigma}), f(\abslength{\sigma}+1), \hdots}$. Since $g\preceq f$ and $f$ is homogeneous there must be $\rho\in p$ s.t.\ $\tau\raisebox{.9ex}{\ensuremath\smallfrown} \rho \sqsubset g$. We can now notice that the subsequence $h$ of $f$ defined as
\[ h:= \coding{f(0),\hdots,f(\abslength{\sigma}-1), f(\abslength{\sigma}+\abslength{\tau}),f(\abslength{\sigma}+\abslength{\tau}+1),\hdots } \]
is s.t.\ $\sigma\raisebox{.9ex}{\ensuremath\smallfrown} \rho\sqsubset h$, and therefore $h\in E$, contradicting the fact that $f$ avoids $E$.

We now claim that $\mathrm{HS}(D) = \mathrm{HS}(E)$. Once the claim is proved we can
use $\mathsf{wFindHS}_{\boldfaceDelta^0_1} (E) = \boldfaceDelta^0_1\mathsf{-RT}(D)$ to finish the reduction.

It is straightforward to notice that $\mathrm{HS}(D)\subset E$ implies $\mathrm{HS}(D)\subset\mathrm{HS}(E)$, hence we only need to prove the inclusion $\mathrm{HS}(E)\subset\mathrm{HS}(D)$. Let $f\in \mathrm{HS}(E)$. Since $E\in\operatorname{dom}(\mathsf{wFindHS}_{\boldfaceDelta^0_1})$ we must have $f\in E$. Assume w.l.o.g.\ that $f\in D$ and let $\sigma\sqsubset f$ be s.t.\ $\sigma\in p$. Fix $g\preceq f$ and let $\rho\sqsubset g$ be s.t.\ $\rho \in p \cup q$. Let $k\in \mathbb{N}$ be s.t.\ $\max \rho < f(k)$ and $\max \sigma < f(k)$, and consider $\tau \in p \cup q$ be s.t.\ $\tau \sqsubset \coding{f(k), f(k+1), \hdots}$. By the homogeneity of $f$ we have that $\tau \in p$ (otherwise every substring of $f$ that begins with $\sigma\raisebox{.9ex}{\ensuremath\smallfrown}  \tau$ would not be in $E$). Let $h\preceq f$ be s.t.\ $\rho\raisebox{.9ex}{\ensuremath\smallfrown}  \tau\sqsubset h$. Again, by the homogeneity of $f$ we have that $\rho \in p$, hence $g\in D$. Since $g$ was  arbitrary, we have that $f\in \mathrm{HS}(D)$.
\end{proof}

\subsection{Problems reducible to \texorpdfstring{$\mathsf{C}_\Baire$}{\mathsf{C}}}
\label{subsec:cbaire}
Here we consider $\mathsf{wFindHS}_{\boldfacePi^0_1}$, $\mathsf{FindHS}_{\boldfacePi^0_1}$ and $\mathsf{FindHS}_{\boldfaceDelta^0_1}$.

\begin{theorem}
	\thlabel{thm:findclopen=findclosed=cbaire}
	$\mathsf{C}_\Baire \equiv_{\mathrm{sW}} \mathsf{FindHS}_{\boldfaceDelta^0_1} \equiv_{\mathrm{sW}} \mathsf{FindHS}_{\boldfacePi^0_1}$.
\end{theorem}
\begin{proof}
	We first show that $\mathsf{FindHS}_{\boldfacePi^0_1}\le_{\mathrm{sW}} \mathsf{C}_\Baire$. Given a name $\coding{P}$ for some open set $P\in\operatorname{dom}(\mathsf{FindHS}_{\boldfacePi^0_1})$, by \thref{lem:computable_operations}.\ref{itm:comp_tree} we can compute a name for the closed set $\mathrm{HS}(P)\backslash P$, which by hypothesis is nonempty. Therefore we can use $\mathsf{C}_\Baire$ to pick a solution.

	Since $\mathsf{FindHS}_{\boldfaceDelta^0_1}\le_{\mathrm{sW}} \mathsf{FindHS}_{\boldfacePi^0_1}$ is trivial, it remains to show that $\mathsf{C}_\Baire \le_{\mathrm{sW}} \mathsf{FindHS}_{\boldfaceDelta^0_1}$.
	Let $T\subset{[\mathbb{N}]}^{<\mathbb{N}} $ be s.t.\ $[T]\neq \emptyset$ and let
	$D:=\describepath{}(T)$, i.e.
	\[ D = \{ f\in [{\mathbb{N}^{<\mathbb{N}}}]^\mathbb{N}: f(0)\in T \text{ and } f(1)\in T \text{ and } f(0)\sqsubseteq f(1) \}. \]
	Recall that $D$ is computable from $T$ (see	\thref{lem:computable_operations}.\ref{itm:path_description}). Moreover, by \thref{lem:clopen_describes_paths}, we have that $D\in\operatorname{dom}(\mathsf{FindHS}_{\boldfaceDelta^0_1})$ and that every $f\in\mathsf{FindHS}_{\boldfaceDelta^0_1}(D)$ uniformly computes a path through $T$.
\end{proof}

\begin{proposition}
	\thlabel{prop:ucbaire<wfindHclosed}
	$\mathsf{UC}_\Baire <_\mathrm{W} \mathsf{wFindHS}_{\boldfacePi^0_1}$.
\end{proposition}
\begin{proof}
	The reduction $\mathsf{UC}_\Baire \le_{\mathrm{W}} \mathsf{wFindHS}_{\boldfacePi^0_1}$ is straightforward
	knowing that $\mathsf{UC}_\Baire\equiv_{\mathrm{W}} \mathsf{wFindHS}_{\boldfaceDelta^0_1}$
	(\thref{cor:wfindclopen=ucbaire}). The fact that the reduction is strict
	follows from \cite[Sec.\ 3]{Solovay78}. In particular, Solovay showed that
	there is an open set $W$ with computable code s.t.\ every
	homogeneous solution avoids $W$ (hence $W$ is a valid input for
	$\mathsf{wFindHS}_{\boldfacePi^0_1}$) and is neither $\Sigma^1_1$ nor $\Pi^1_1$ (in particular it
	is not hyperarithmetic), while every computable instance of $\mathsf{UC}_\Baire$ has an
	hyperarithmetic solution (\thref{thm:ucbaire_hyperarithmetic_solution}).
\end{proof}

\begin{proposition}
\thlabel{prop:wfindHclosed<=cbaire}
	$\mathsf{wFindHS}_{\boldfacePi^0_1} \le_{\mathrm{W}} \mathsf{C}_\Baire \equiv_{\mathrm{W}} \mathsf{C}_\Cantor * \mathsf{wFindHS}_{\boldfacePi^0_1}$.
\end{proposition}
\begin{proof}
The first reduction follows from \thref{thm:findclopen=findclosed=cbaire} as $\mathsf{wFindHS}_{\boldfacePi^0_1}$ is the restriction of $\mathsf{FindHS}_{\boldfacePi^0_1}$ to a smaller domain.
The reduction $\mathsf{C}_\Cantor * \mathsf{wFindHS}_{\boldfacePi^0_1}\le_{\mathrm{W}}\mathsf{C}_\Baire$ is straightforward from $\mathsf{C}_\Cantor\le_{\mathrm{W}}\mathsf{C}_\Baire$, $ \mathsf{wFindHS}_{\boldfacePi^0_1}\le_{\mathrm{W}} \mathsf{C}_\Baire$ and $\mathsf{C}_\Baire$ is closed under compositional product.

Finally the reduction $\mathsf{C}_\Baire \le_{\mathrm{W}} \mathsf{C}_\Cantor * \mathsf{wFindHS}_{\boldfacePi^0_1}$ is suggested by the proof of the corollary in \cite[Sec.\ 3]{Solovay78}. In particular, given an ill-founded tree $T\subset{[\mathbb{N}]}^\mathbb{N} $ we can computably define the open set $W:=\solovay{}(T)$ (\thref{def:solovay_open}). By \thref{lem:solutions_solovay_open_set}, $W\in\operatorname{dom}(\mathsf{wFindHS}_{\boldfacePi^0_1})$ and every solution $f\in \mathsf{wFindHS}_{\boldfacePi^0_1}(W)$ dominates a path through $T$. Let $X$ be the subtree of ${\mathbb{N}^{<\mathbb{N}}}$ of the strings that are dominated by $f$ and let $T_f:= T \cap X$. Since $\emptyset\neq [T_f]\subset [T]$, we can use $\codedChoice{}{}{[X]}([T_f])$ to compute a path through $T$. To conclude the proof it is enough to notice that $\mathsf{C}_\Cantor \equiv_{\mathrm{W}} \codedChoice{}{}{[X]}$ (\cite[Thm.\ 7.23]{BGP17}).
\end{proof}

Notice that, by the choice-elimination principle (\cite[Thm.\ 7.25]{BGP17}), if $Y$ is a computable metric space, $f:\subseteq X \to Y$ is a single-valued function and $f\le_{\mathrm{W}}\mathsf{C}_\Baire$ then $f\le_{\mathrm{W}} \mathsf{wFindHS}_{\boldfacePi^0_1}$.

Since we are not able to show the equivalence of $\mathsf{wFindHS}_{\boldfacePi^0_1}$ with any known principle, it is worth to study its properties.

\begin{proposition}
	\thlabel{prop:wfindclosed_closed_product}
	$\mathsf{wFindHS}_{\boldfacePi^0_1} \equiv_{\mathrm{sW}}  \mathsf{wFindHS}_{\boldfacePi^0_1} \times \mathsf{wFindHS}_{\boldfacePi^0_1}$.
\end{proposition}
\begin{proof}
	Notice that if $P,Q\in \operatorname{dom}(\mathsf{wFindHS}_{\boldfacePi^0_1})$ then $P\cup Q \in \operatorname{dom}(\mathsf{wFindHS}_{\boldfacePi^0_1})$. Indeed, for every $f\in {[\mathbb{N}]}^\mathbb{N} $, by the open Ramsey theorem applied to $[f]^\mathbb{N}\cap P$ (see \thref{prop:galvin_prikry_subset}), there is a $g\preceq f$ s.t.\ $[g]^\mathbb{N}\subset [f]^\mathbb{N}\cap P$ or $[g]^\mathbb{N}\cap [f]^\mathbb{N}\cap P = \emptyset$. In the first case we would have a contradiction as $[g]^\mathbb{N}\subset [f]^\mathbb{N}\cap P$ implies $[g]^\mathbb{N}\subset P$, i.e.\ $\mathrm{HS}(P)\cap P \neq \emptyset$, against $P\in\operatorname{dom}(\mathsf{wFindHS}_{\boldfacePi^0_1})$. Therefore we have $[g]^\mathbb{N}\cap [f]^\mathbb{N}\cap P = [g]^\mathbb{N}\cap P = \emptyset$, i.e.\ $g\in\mathrm{HS}(P)\backslash{P}$. With a similar argument, we can now apply the open Ramsey theorem to $[g]^\mathbb{N}\cap Q$ and conclude that there is a $h\preceq g$ s.t.\ $h\in \mathrm{HS}(Q)\backslash{Q}$. In particular $h\notin Q$ and $h\notin P$ (as $h\preceq g$ and $g$ avoids $P$). Therefore $h$ is a subsequence of $f$ that is not in $P\cup Q$. Since $f$ was arbitrary, we have that $\mathrm{HS}(P\cup Q)\cap (P\cup Q)=\emptyset$. This shows that every homogeneous solution $f\in \mathrm{HS}(P\cup Q)$ avoids $P\cup Q$, and, in particular, avoids both $P$ and $Q$. Since the union is computable (see \thref{lem:computable_operations_open}.\ref{itm:open_union}) we can compute a solution for $(\mathsf{wFindHS}_{\boldfacePi^0_1}\times\mathsf{wFindHS}_{\boldfacePi^0_1})(P,Q)$ by computing $f\in\mathsf{wFindHS}_{\boldfacePi^0_1}(P\cup Q)$ and returning two copies of $f$.
\end{proof}

Let $\codedChoice{\boldfaceSigma^1_1}{cof}{\mathbb{N}}\pmfunction{\boldsymbol{\Sigma}^1_1(\mathbb{N})}{\mathbb{N}}$ be the multivalued function that chooses an element from a non-empty $\boldsymbol{\Sigma}^1_1$ cofinite subset of $\mathbb{N}$. It is equivalent to assume that the input is a $\boldsymbol{\Sigma}^1_1$ final segment of $\mathbb{N}$. Indeed, given a cofinite $\boldsymbol{\Sigma}^1_1$ set $A$ we can computably define the $\boldsymbol{\Sigma}^1_1$ set
\[ B:=\{ n\in\mathbb{N} : (\forall m\ge n)(m\in A)\}, \]
which is a (non-empty) final segment of $\mathbb{N}$. Since $B\subset A$, choosing an element in $B$ yields a solution for $\codedChoice{\boldfaceSigma^1_1}{cof}{\mathbb{N}}(A)$. With this in mind, we can assume that an input for $\codedChoice{\boldfaceSigma^1_1}{cof}{\mathbb{N}}$ is a sequence $\sequence{T_m}{m\in\mathbb{N}}$ of trees s.t.\ there exists $k$ s.t.\ $[T_i]=\emptyset$ iff $i<k$.

The problem $\parallelization{\codedChoice{\boldfaceSigma^1_1}{cof}{\mathbb{N}}}$ has been studied in \cite{KiharaADauriacChoice} under the name $\boldsymbol{\Sigma}^1_1\text{-}\mathsf{AC}^{\vphantom{g}\mathsf{cof}}_{{\mathbb{N}^\mathbb{N}}}$. Moreover, \cite{KMP20} (implicitly) uses $\parallelization{\codedChoice{\boldfaceSigma^1_1}{cof}{\mathbb{N}}}$ in the proof of Lemma 4.7 to separate $\boldsymbol{\Sigma}^1_1\text{-}\mathsf{WKL}$ from $\parallelization{\codedChoice{\boldsymbol{\Sigma}^1_1}{}{\mathbb{N}}}$. It is known that $\parallelization{\codedChoice{\boldfaceSigma^1_1}{cof}{\mathbb{N}}} <_\mathrm{W} \mathsf{C}_\Baire$ \cite[Thm.\ 3.34]{KiharaADauriacChoice}. Moreover, $\mathsf{UC}_\Baire <_\mathrm{W} \parallelization{\codedChoice{\boldfaceSigma^1_1}{cof}{\mathbb{N}}}$ (\cite{GPVDescSeq}).

\begin{theorem}
	$\parallelization{\codedChoice{\boldfaceSigma^1_1}{cof}{\mathbb{N}}}\le_{\mathrm{sW}} \mathsf{wFindHS}_{\boldfacePi^0_1}$.
\end{theorem}
\begin{proof}
	We will use strings $\sigma$ which are prefixes of an infinite string $f$ obtained by joining countably many strings $g_i$; we write $\sigma = \operatorname{dvt}(\tau_0,\hdots,\tau_n)$ if $\tau_i$ is the prefix of $g_i$ contained in $\sigma$. Formally $\sigma = \operatorname{dvt}(\tau_0,\hdots,\tau_n)$ iff
	\begin{itemize}
		\item $n = \max\{i: \coding{i,0} < \abslength{\sigma}\}$,
		\item for each $i$, $\abslength{\tau_i} = \max\{j: \coding{i,j} < \abslength{\sigma}\}+1$,
		\item for each $\coding{i,j} < \abslength{\sigma}$, $\tau_i(j) = \sigma(\coding{i,j})$.
	\end{itemize}

	Let $\sequence{T_{n,m}}{n,m\in\mathbb{N}}$ be a double sequence of trees s.t.\ for every $n$ there is $k_n$ s.t.\ $[T_{n,m}]=\emptyset$ iff $m<k_n$. For every $n$ we can define
	\[ T_n := \coding{}\cup \bigcup_{m\in\mathbb{N}} \coding{m}\raisebox{.9ex}{\ensuremath\smallfrown}  T_{n,m}. \]
	Notice that, by hypothesis, for every $n$ we have $[T_n]\neq\emptyset$. Moreover, if $f\in [T_n]$ then $f(0)\in \codedChoice{\boldfaceSigma^1_1}{cof}{\mathbb{N}}( \sequence{T_{n,m}}{m\in\mathbb{N}} )$.
	Define also
	\[ T:= \{\sigma \in \finStrings{\mathbb{N}}: \sigma = \operatorname{dvt}(\tau_0,\hdots,\tau_k) \land (\forall i\le k)(\tau_i\in T_i) \}. \]
	Notice that if $f_n\in [T_n]$ then $\coding{f_n}_{n\in\mathbb{N}}\in [T]$, hence $[T]\neq\emptyset$. Moreover, if $f\in [T]$ and $i\le j$ then, letting $f[i]=\operatorname{dvt}(\tau_0,\hdots,\tau_k)$ and $f[j]=\operatorname{dvt}(\rho_0,\hdots,\rho_h)$, for every $n\le k$ we have $\tau_n\sqsubseteq \rho_n$. Therefore
	\[ f\in [T] \iff f= \coding{f_n}_{n\in\mathbb{N}} \text{ and } (\forall n\in \mathbb{N})(f_n \in [T_n]). \]
	Let $W:=\solovay{}(T)$ be the Solovay open set for $T$. By \thref{lem:solutions_solovay_open_set}, $W\in \operatorname{dom}(\mathsf{wFindHS}_{\boldfacePi^0_1})$ and every $h\in \mathsf{wFindHS}_{\boldfacePi^0_1}(W)$ dominates a path through $T$.

	To conclude the proof we notice that, if $f=\coding{f_n}_{n\in\mathbb{N}}\in [T]$ and  $h$ dominates $f$ then, for every $n$,
	\[ h(\coding{n,0})\ge f_n(0) \in \codedChoice{\boldfaceSigma^1_1}{cof}{\mathbb{N}}( \sequence{T_{n,m}}{m\in\mathbb{N}} ).\] In particular $h(\coding{n,0})\in\codedChoice{\boldfaceSigma^1_1}{cof}{\mathbb{N}}(\sequence{T_{n,m}}{m\in\mathbb{N}} )$.
\end{proof}

Let ${ \mathsf{ATR} }_2\mfunction{\mathrm{LO}\times {2^\mathbb{N}}\times \mathbb{N}}{\{0,1\}\times{\mathbb{N}^\mathbb{N}}}$ be the two sided version of ${ \mathsf{ATR} }$, defined in \cite[Def.\ 8.2 and prop.\ 8.9]{gohatr} as the multivalued function whose inputs are triples $(L,A,\theta)$ and the output is a pair $(i,Y)$ s.t.\ either $i=0$ and $Y$ is a $<_L$-infinite descending chain or $i=1$ and $Y$ is a (pseudo)hierarchy $\coding{Y_a}_{a\in L}$ s.t.\ for all $b\in L$, $Y_b=\{n: \theta(n,\bigoplus_{a<_L b} Y_a, A )\}$. It is known that $\mathsf{UC}_\Baire<_\mathrm{W} { \mathsf{ATR} }_2 <_\mathrm{W} \mathsf{C}_\Baire$ (\cite[Cor.\ 8.5 and 8.7]{gohatr}). Jun Le Goh (personal communication) observed the following corollary:

\begin{corollary}
	\thlabel{thm:wfindclosed_not_reducible_atr2}
	$\mathsf{wFindHS}_{\boldfacePi^0_1}\not\le_{\mathrm{W}} { \mathsf{ATR} }_2$.
\end{corollary}
\begin{proof}
	The claim follows from the fact that $\mathsf{C}_\Baire\le_{\mathrm{W}}\mathsf{C}_\Cantor*\mathsf{wFindHS}_{\boldfacePi^0_1}$ (\thref{prop:wfindHclosed<=cbaire}) while $\mathsf{C}_\Baire
	\not\le_{\mathrm{W}}\mathsf{C}_\Cantor*{ \mathsf{ATR} }_2$ (\cite[Cor.\ 8.5]{gohatr}).
\end{proof}

Let us denote with $\mathsf{TwFindHS}_{\boldfaceSigma^0_1} $ the total continuation of $\mathsf{wFindHS}_{\boldfaceSigma^0_1} $, i.e.\ the (total) multivalued function with domain $\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )$ defined as
\[ \mathsf{TwFindHS}_{\boldfaceSigma^0_1} (P):= \begin{cases}
	\mathrm{HS}(P)	& \text{if } P\in \operatorname{dom}(\mathsf{wFindHS}_{\boldfaceSigma^0_1} ); \\
	{[\mathbb{N}]}^\mathbb{N} 		& \text{otherwise}.
\end{cases} \]
The following proposition underlines the gap between $\mathsf{wFindHS}_{\boldfaceSigma^0_1} $ and $\mathsf{wFindHS}_{\boldfacePi^0_1}$ ($\mathsf{wFindHS}_{\boldfaceSigma^0_1} <_\mathrm{W} \mathsf{wFindHS}_{\boldfacePi^0_1}$ by \thref{thm:open<ucbaire} and \thref{prop:ucbaire<wfindHclosed}).
\begin{proposition}
	\thlabel{thm:twfindopen<=atr2}
	$\mathsf{TwFindHS}_{\boldfaceSigma^0_1}  \le_{\mathrm{W}} { \mathsf{ATR} }_2$, and hence $\mathsf{wFindHS}_{\boldfacePi^0_1}\not\le_{\mathrm{W}}\mathsf{TwFindHS}_{\boldfaceSigma^0_1} $.
\end{proposition}
\begin{proof}
	Let $P\in\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )$ be an input for $\mathsf{TwFindHS}_{\boldfaceSigma^0_1} $ and consider the tree $\closedsidesoltree{\coding{P}}$. We can computably build the linear order $\mathrm{KB}(\closedsidesoltree{\coding{P}})$. Let $\theta$ be the arithmetic formula defined in the proof of \thref{thm:open<ucbaire}. Notice that $\mathrm{KB}(\closedsidesoltree{\coding{P}})$ is not necessarily a well-order, as we are not assuming $P\in\operatorname{dom}(\mathsf{wFindHS}_{\boldfaceSigma^0_1} )$ (i.e.\ there may be solutions that avoid $P$). We therefore need to modify $\theta$ by requiring that for every $\sigma \in \closedsidesoltree{\coding{P}}$, if either $V_\sigma$ is finite or $V_\sigma \backslash U_\tau$ is infinite for some $\tau <_{\mathrm{KB}(\closedsidesoltree{\coding{P}})} \sigma$ (this cannot happen if $\mathrm{KB}(\closedsidesoltree{\coding{P}})$ is a well-order), then we set $U_\sigma = \mathbb{N}$ and we label $\sigma$ as bad. Let $\theta'$ be the modified formula.

	Let $(i,Y)\in { \mathsf{ATR} }_2(\mathrm{KB}(\closedsidesoltree{\coding{P}}), P, \theta')$. If $i=0$ then $Y$ is a $<_{\mathrm{KB}(\closedsidesoltree{\coding{P}})}$-infinite descending sequence and $P\notin\operatorname{dom}(\mathsf{wFindHS}_{\boldfaceSigma^0_1} )$; therefore any $f\in{[\mathbb{N}]}^\mathbb{N} $ is a valid output for $\mathsf{TwFindHS}_{\boldfaceSigma^0_1} (P)$. Suppose now that $i=1$, so that $Y$ is a (pseudo)hierarchy. By construction, $Y$ yields a labeling of each $\sigma\in{[\mathbb{N}]}^{<\mathbb{N}} $ as ``good'' or ``bad'', and, for each $\sigma \in \closedsidesoltree{\coding{P}}$, an infinite set $U_\sigma$ (see the proof of \cite[Lem.\ V.9.4]{Simpson09}). The classical proof shows that if $P\in\operatorname{dom}(\mathsf{wFindHS}_{\boldfaceSigma^0_1} )$ then $\coding{}$ is good. In particular if $\coding{}$ is bad then we can immediately conclude that $P\notin\operatorname{dom}(\mathsf{wFindHS}_{\boldfaceSigma^0_1} )$ (and, again, any $f\in{[\mathbb{N}]}^\mathbb{N} $ is a valid solution for the original problem). On the other hand,
	if $\coding{}$ is good then the modifications made to obtain $\theta'$ ensure that the intersection of finitely many $U_\sigma$ is infinite, and therefore we can compute $f\in {[\mathbb{N}]}^\mathbb{N} $ following the construction of the classical proof. Notice that if $P\in\operatorname{dom}(\mathsf{wFindHS}_{\boldfaceSigma^0_1} )$ then $f\in \mathrm{HS}(P)=\mathsf{TwFindHS}_{\boldfaceSigma^0_1} (P)$. On the other hand, if $P\notin\operatorname{dom}(\mathsf{wFindHS}_{\boldfaceSigma^0_1} )$ then $f\in\mathsf{TwFindHS}_{\boldfaceSigma^0_1} (P)$ (trivially).

	The second part follows from \thref{thm:wfindclosed_not_reducible_atr2}.
\end{proof}

\subsection{Problems not reducible to \texorpdfstring{$\mathsf{C}_\Baire$}{\mathsf{C}}}
\label{subsec:not_cbaire}

Let us turn our attention to the last two remaining problems, namely $\boldfaceSigma^0_1\mathsf{-RT}$ and $\mathsf{FindHS}_{\boldfaceSigma^0_1} $.

\begin{proposition}
	\thlabel{prop:tcbaire<=ccantor_comp_openRamsey}
	$\mathsf{TC}_\Baire\le_{\mathrm{W}} \mathsf{C}_\Cantor* \boldfaceSigma^0_1\mathsf{-RT}$ and $\chi_{\Pi^1_1}<_\mathrm{W} \mathsf{LPO} * \boldfaceSigma^0_1\mathsf{-RT}$.
\end{proposition}
\begin{proof}
	We first show $\mathsf{TC}_\Baire\le_{\mathrm{W}}\mathsf{C}_\Cantor*\boldfaceSigma^0_1\mathsf{-RT}$. Let $T\subset{[\mathbb{N}]}^\mathbb{N} $ be a tree and let $W:=\solovay{}(T)$ be the Solovay open set of $T$. Let also $f\in \boldfaceSigma^0_1\mathsf{-RT}(W)$. By \thref{lem:solutions_solovay_open_set}, if $[T]\neq \emptyset$ then $\mathrm{HS}(W)\cap W=\emptyset$ and $f$ is a bound for some $x\in [T]$. On the other hand, if $[T]=\emptyset$ then $W={[\mathbb{N}]}^\mathbb{N} $ and $f$ is just an arbitrary infinite string.

	Let $X$ be the subtree of ${\mathbb{N}^{<\mathbb{N}}}$ of the strings that are dominated by $f$. Notice that $\TChoice{[X]}\equiv_{\mathrm{W}}\Choice{[X]}$. Indeed, to show that $\TChoice{[X]}\le_{\mathrm{W}} \Choice{[X]}$ we can notice that, given a tree $S\subset X$, we can computably define an ill-founded tree $R$ as follows: for each level $n$ we check whether $S$ has no nodes at level $n$.
	If this happens for some $n$, we can (computably) extend $S$ to an ill-founded tree $R$. If this never happens then $R=S$. It is straightforward to see that $\Choice{[X]}([R])\subset \TChoice{[X]}([S])$.

	Let $T_f:= T \cap X$. By \cite[Thm.\ 7.23]{BGP17}, $\mathsf{C}_\Cantor\equiv_{\mathrm{W}}\Choice{[X]}\equiv_{\mathrm{W}}\TChoice{[X]}$, therefore we can use $\mathsf{C}_\Cantor$ to compute a solution $h\in\TChoice{[X]}([T_f])$. Notice that $h\in \mathsf{TC}_\Baire([T])$. Indeed, if $[T]\neq \emptyset$ then $[T_f]\neq \emptyset$ and $h$ is a path through $T$.

	A simple modification of the above argument shows that $\chi_{\Pi^1_1}\le_{\mathrm{W}} \mathsf{LPO} *\boldfaceSigma^0_1\mathsf{-RT}$. In fact, we can see the tree $T$ as an input for $\chi_{\Pi^1_1}$. If $f\in\boldfaceSigma^0_1\mathsf{-RT}(\solovay{}(T))$ then $T_f$ is a finitely branching tree. Thus whether $T_f$ is finite is a $\Sigma^0_1$ question in $T_f$. We can therefore use $ \mathsf{LPO} $ to check if $T_f$ is infinite and hence establish whether it is well-founded or not (by K\"onig's lemma, a finitely-branching tree is infinite iff it has a path).

	The reduction is trivially strict as $\chi_{\Pi^1_1}$ always has a computable output.
\end{proof}

It follows from \thref{thm:openRT_not_<=_sTCbaire_x_lim^n} that the reduction $\mathsf{TC}_\Baire\le_{\mathrm{W}}\mathsf{C}_\Cantor*\boldfaceSigma^0_1\mathsf{-RT}$ is actually strict.

\begin{corollary}
\thlabel{cor:openRamsey_not<_cbaire}
$\boldfaceSigma^0_1\mathsf{-RT} \not\le_{\mathrm{W}} \mathsf{C}_\Baire$.
\end{corollary}
\begin{proof}
If $\boldfaceSigma^0_1\mathsf{-RT} \le_{\mathrm{W}} \mathsf{C}_\Baire $ then
\[ \chi_{\Pi^1_1} \le_{\mathrm{W}}  \mathsf{LPO} * \boldfaceSigma^0_1\mathsf{-RT} \le_{\mathrm{W}} \mathsf{C}_\Baire * \mathsf{C}_\Baire \equiv_{\mathrm{W}} \mathsf{C}_\Baire, \]
contradicting the fact that $\chi_{\Pi^1_1} \not\le_{\mathrm{W}} \mathsf{C}_\Baire$ (see \cite[Sec.\ 7]{KMP20}).
\end{proof}

\begin{corollary}
\thlabel{cor:wfindHclosed<openRT}
$\mathsf{wFindHS}_{\boldfacePi^0_1}<_\mathrm{W} \boldfaceSigma^0_1\mathsf{-RT}$.
\end{corollary}
\begin{proof}
The fact that $\mathsf{wFindHS}_{\boldfacePi^0_1}\le_{\mathrm{W}}\boldfaceSigma^0_1\mathsf{-RT}$ is trivial since $\mathsf{wFindHS}_{\boldfacePi^0_1}$ is a restriction of $\boldfaceSigma^0_1\mathsf{-RT}$ to a smaller
domain. The reduction is strict because
$\boldfaceSigma^0_1\mathsf{-RT}\not\le_{\mathrm{W}}\mathsf{C}_\Baire$ (\thref{cor:openRamsey_not<_cbaire})
but $\mathsf{wFindHS}_{\boldfacePi^0_1}\le_{\mathrm{W}}\mathsf{C}_\Baire$ (\thref{prop:wfindHclosed<=cbaire}).
\end{proof}

\begin{definition}
	For every represented space $X$, we define the \textdef{strong total continuation of} $\mathsf{C}_X$ to be the multivalued function $\mathsf{sTC}_X\mfunction{\boldsymbol{\Pi}^0_1(X)}{2\times X}$ defined as
	\[ \mathsf{sTC}_X(A):=\{ (b,x) \in 2\times X : (b=0 \rightarrow A=\emptyset) \land (b=1 \rightarrow x\in A) \}. \]
	In particular, for $X={\mathbb{N}^\mathbb{N}}$ (and analogously for $X={2^\mathbb{N}}$) we can think of $\mathsf{sTC}_{\Baire}$ as the total multivalued function that, given in input a tree, returns a string $\coding{b}\raisebox{.9ex}{\ensuremath\smallfrown}  x$ s.t.\ $b$ codes whether the tree is well-founded or not and, if it is ill-founded, then $x$ is a path through $T$.
\end{definition}

\label{thm:tcbaire<stcbaire} It is clear that $\mathsf{TC}_\Baire <_\mathrm{W} \mathsf{sTC}_{\Baire}$ (the fact that the reduction is strict follows from $\chi_{\Pi^1_1}\not\le_{\mathrm{W}}\mathsf{TC}_\Baire$ \cite[Cor.\ 8.6]{KMP20}, while obviously $\chi_{\Pi^1_1}\le_{\mathrm{W}}\mathsf{sTC}_{\Baire}$). We can also notice the following:

\begin{corollary}
	\thlabel{thm:sTCBaire<=sTCCantor*openRT}
	$\mathsf{sTC}_{\Baire} \le_{\mathrm{W}} \mathsf{sTC}_{\Cantor} * \boldfaceSigma^0_1\mathsf{-RT}$.
\end{corollary}
\begin{proof}
	It suffices to repeat the proof of the first statement of \thref{prop:tcbaire<=ccantor_comp_openRamsey}, using $\mathsf{sTC}_{\Cantor}$ in place of $\mathsf{C}_\Cantor$.
\end{proof}
We will prove in \thref{thm:tcbaire_arit_<_openRT} that the above reduction is actually strict.

\begin{proposition}
	$\parallelization{ \mathsf{TC}_\Baire } ~|_{\mathrm{W}~} \mathsf{sTC}_{\Baire}$.
\end{proposition}
\begin{proof}
	The fact that $\mathsf{sTC}_{\Baire}\not\le_{\mathrm{W}} \parallelization{ \mathsf{TC}_\Baire }$ follows from the obvious observation that $\chi_{\Pi^1_1}\le_{\mathrm{W}}\mathsf{sTC}_{\Baire}$, while $\chi_{\Pi^1_1}\not\le_{\mathrm{W}}\parallelization{ \mathsf{TC}_\Baire }$ (see \cite[Cor.\ 8.6]{KMP20}).

	On the other hand, if $\parallelization{ \mathsf{TC}_\Baire } \le_{\mathrm{W}} \mathsf{sTC}_{\Baire}$ then, in particular, $\mathsf{TC}_\Baire\times \mathsf{C}_\Baire\le_{\mathrm{W}} \mathsf{sTC}_{\Baire}$. Since $ \mathsf{NHA} \le_{\mathrm{W}}\mathsf{C}_\Baire$ (see e.g.\ \cite[Cor.\ 3.6]{KMP20}), by \thref{prop:product_with_NHA_general}, this implies that $\mathsf{TC}_\Baire\le_{\mathrm{W}}\mathsf{sTC}_{\Baire}\restrict{A}$, where $A$ is the set of non-empty closed sets of ${\mathbb{N}^\mathbb{N}}$ with no hyperarithmetic member (notice that $\mathsf{sTC}_{\Baire}(\emptyset)$ has computable solutions). In particular, this implies that $\mathsf{TC}_\Baire\le_{\mathrm{W}}\mathsf{C}_\Baire$, contradicting \cite[Prop. 8.2.1]{KMP20}.
\end{proof}

We will now show that $\boldfaceSigma^0_1\mathsf{-RT}\not\le_{\mathrm{W}}\mathsf{TC}_\Baire$. We actually prove a stronger result that will be useful in Section~\ref{sec:artihemtic_reducibility}.

\begin{theorem}
	\thlabel{thm:openRT_not_<=_sTCbaire_x_lim^n}
	For every $n\in\mathbb{N}$, $\boldfaceSigma^0_1\mathsf{-RT}\not\le_{\mathrm{W}} \mathsf{sTC}_{\Baire} \times \mathsf{lim}^{(n)}$.
\end{theorem}
\begin{proof}
	Let $(X,\repmap{X})$ be the represented space of computably open subsets of ${[\mathbb{N}]}^\mathbb{N} $ with no arithmetic homogeneous solution, where $\repmap{X}$ is the restriction of $\repmap{\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )}$ to computable names. Let us define $\boldfaceSigma^0_1\mathsf{-RT}_X\mfunction{X}{{[\mathbb{N}]}^\mathbb{N} }$ as $\boldfaceSigma^0_1\mathsf{-RT}_X(P):=\mathrm{HS}(P)$.

	The reduction $\boldfaceSigma^0_1\mathsf{-RT}_X\le_{\mathrm{W}}\boldfaceSigma^0_1\mathsf{-RT}$ holds trivially, hence it is enough to prove that
	\[ \boldfaceSigma^0_1\mathsf{-RT}_X \not\le_{\mathrm{W}} \mathsf{sTC}_{\Baire} \times \mathsf{lim}^{(n)}.\]
	Assume by contradiction that there is a reduction. Since $\mathsf{lim}^{(n)}$ is a cylinder, we can assume that the reduction is a strong Weihrauch reduction. Let $\Phi_1, \Phi_2,\Psi$ be the maps witnessing the strong reduction, with $\Phi_1$ producing an input for $\mathsf{sTC}_{\Baire}$ and $\Phi_2$ producing an input for $\mathsf{lim}^{(n)}$. Assume that there is an $P\in X$ s.t.\ $\Phi_1(\coding{P})$ is a name for the empty set, for some name $\coding{P}$ of $P$. By definition, $0^\omega$ is a valid output of $\mathsf{sTC}_{\Baire}(\emptyset)$. Let $q:= \mathsf{lim}^{(n)}(\Phi_2(\coding{P}))$. Notice that $q$ is arithmetic, as $\coding{P}$ is computable by definition of $X$. We have now reached a contradiction as $\Psi(0^\omega, q)$ is arithmetic, against the fact that $P$ has no arithmetic solution.

	This implies that, for every $P\in X$ and every name $\coding{P}$ of $P$, $\Phi_1(\coding{P})$ is a name for a non-empty closed set, hence we have a reduction $\boldfaceSigma^0_1\mathsf{-RT}_{X}\le_{\mathrm{W}}\mathsf{C}_\Baire \times \mathsf{lim}^{(n)}\equiv_{\mathrm{W}} \mathsf{C}_\Baire$.

	We now claim that $\boldfaceSigma^0_1\mathsf{-RT}_X\not\le_{\mathrm{W}}\mathsf{C}_\Baire$, concluding the proof. We will in fact show that $c\chi_{\Pi^1_1}\le_{\mathrm{W}} \mathsf{LPO} *\boldfaceSigma^0_1\mathsf{-RT}_X$, where $c\chi_{\Pi^1_1}$ is the restriction of $\chi_{\Pi^1_1}$ to computable trees. The claim then follows from the fact that $c\chi_{\Pi^1_1}\not\le_{\mathrm{W}}\mathsf{C}_\Baire$ (as $c\chi_{\Pi^1_1}$ is not effectively Borel measurable, see \cite[Thm.\ 7.7]{BdBPLow12}) and the fact that $\mathsf{C}_\Baire$ is closed under compositional product.

	Let $\Phi_D$ be the forward functional witnessing $\codedUChoice{\boldsymbol{\Sigma}^1_1}{}{{\mathbb{N}^\mathbb{N}}}\le_{\mathrm{W}}\mathsf{wFindHS}_{\boldfaceDelta^0_1}$ (recall that $\codedUChoice{\boldsymbol{\Sigma}^1_1}{}{{\mathbb{N}^\mathbb{N}}}\equiv_{\mathrm{W}}\mathsf{UC}_\Baire$ \cite[Thm.\ 3.11]{KMP20}, while $\mathsf{UC}_\Baire\le_{\mathrm{W}}\mathsf{wFindHS}_{\boldfaceDelta^0_1}$ has been proved in \thref{thm:ucbaire<clopen}). Let also $T_{NAR}$ be a computable input for $\codedUChoice{\boldsymbol{\Sigma}^1_1}{}{{\mathbb{N}^\mathbb{N}}}$ with a single non-arithmetic solution (recall that, by \cite[Thm.\ II.4.2]{SacksHRT} every $H$-set is a $\Pi^0_2$ singleton).

	Let $T$ be an input for $c\chi_{\Pi^1_1}$. We can assume w.l.o.g.\ that $T$ has no hyperarithmetic path: indeed if $S$ is a computable ill-founded tree with no hyperarithmetic path then
	\[ T\times S:=\{ \coding{ \coding{\sigma(0),\tau(0)},\hdots, \coding{\sigma(n-1),\tau(n-1)}} : \sigma \in T \text{ and } \tau\in S \}\]
	is ill-founded iff $T$ is, and $T\times S$ has no hyperarithmetic path.

	Let $W:=\solovay{}(T)$ be the Solovay open set for $T$ and let $Q$ be the clopen set with name $\Phi_D(T_{NAR})$. Notice that, since $Q\in\operatorname{dom}(\mathsf{wFindHS}_{\boldfaceDelta^0_1})$, for every $f$ we can computably find a subsequence $g\preceq f$ s.t.\ $g\in Q$.

	We can computably define $P:=W\cap Q$ (see \cite[Prop.\ 3.2.4]{Brattka05}). Since $W$ and $Q$ are computable then so is $P$. Let us show that $P$ does not have any arithmetic solution, which implies $P\in X$. We distinguish two cases:
	\begin{enumerate}
		\item $[T]=\emptyset$:  by \thref{lem:solutions_solovay_open_set} we have that $W={[\mathbb{N}]}^\mathbb{N} $, hence $P=Q$ and $\mathrm{HS}(P)=\mathrm{HS}(Q)$. Since every solution for $Q$ computes the non-arithmetic solution for $T_{NAR}$, $P$ does not have arithmetic solutions.
		\item $[T]\neq\emptyset$: notice first of all that $P\in\operatorname{dom}(\mathsf{wFindHS}_{\boldfacePi^0_1})$ as $P\subset W$ and $W\in\operatorname{dom}(\mathsf{wFindHS}_{\boldfacePi^0_1})$ (see \thref{lem:solutions_solovay_open_set}).

		Given $f\in\mathrm{HS}(P)$ then, by the above observation, we can computably find a subsolution $g\in\mathrm{HS}(P)$ s.t.\ $g\in Q$, thus $g\notin W$. By K\"onig's lemma such a $g$ is a bound for a path through $T$ (see the proof of \thref{lem:solutions_solovay_open_set}). This also implies that every $f\in\mathrm{HS}(P)$ is not (hyper)arithmetic (as, by hypothesis, $T$ does not have hyperarithmetic paths).
	\end{enumerate}
	Given $f\in \boldfaceSigma^0_1\mathsf{-RT}_{X}(P)$ we can computably find $g\preceq f$ s.t.\ $g\in Q$. Let $T_g$ be the subtree of $T$ bounded by $g$. Notice that $g$ is a bound for a path through $T$ iff $T_g$ is ill-founded iff $T$ is ill-founded (as shown in case $2$ above). Since $T_g$ is a finitely-branching tree, by K\"onig's lemma $T_g$ is ill-founded iff it is infinite. Moreover, the problem of checking whether $T_g$ is finite is a $\Sigma^{0,g}_1$ question, hence we can use $ \mathsf{LPO} $ to solve the problem (as in the proof of \thref{prop:tcbaire<=ccantor_comp_openRamsey}).
\end{proof}

\begin{proposition}
	\thlabel{prop:product_with_NHA}
	For every (partial) multivalued function $f$, if $f\times \mathsf{NHA}  \le_{\mathrm{W}}\boldfaceSigma^0_1\mathsf{-RT}$ then $f\le_{\mathrm{W}} \mathsf{C}_\Baire$.
\end{proposition}
\begin{proof}
	Assume $f\times \mathsf{NHA} \le_{\mathrm{W}} \boldfaceSigma^0_1\mathsf{-RT}$ and let
	$B:=\operatorname{dom}(\mathsf{wFindHS}_{\boldfaceSigma^0_1} )$. Obviously $\boldfaceSigma^0_1\mathsf{-RT}\restrict{B} = \mathsf{wFindHS}_{\boldfaceSigma^0_1} $,
	hence, since $\mathsf{wFindHS}_{\boldfaceSigma^0_1} \equiv_{\mathrm{W}}\mathsf{UC}_\Baire$
	(\thref{cor:wfindclopen=ucbaire}), the restriction of $\boldfaceSigma^0_1\mathsf{-RT}$ to $B$
	always has a solution that is hyperarithmetic relative to the input
	(\thref{thm:ucbaire_hyperarithmetic_solution}). Since $f\times
	 \mathsf{NHA} \le_{\mathrm{W}}\boldfaceSigma^0_1\mathsf{-RT}$, by \thref{prop:product_with_NHA_general}, we
	have that $f$ is reducible to the restriction of $\boldfaceSigma^0_1\mathsf{-RT}$ to
	\[ A:= \setcomplement[\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )]{B} = \operatorname{dom}(\mathsf{FindHS}_{\boldfacePi^0_1}).  \]
	This implies that $f\le_{\mathrm{W}} \mathsf{FindHS}_{\boldfacePi^0_1}$, as for each $P\in A$ we have $\mathsf{FindHS}_{\boldfacePi^0_1}(P)\subset \boldfaceSigma^0_1\mathsf{-RT}(P)$ (and therefore every realizer for $\mathsf{FindHS}_{\boldfacePi^0_1}$ is also a realizer for $\boldfaceSigma^0_1\mathsf{-RT}\restrict{A}$). The claim follows from the fact that $\mathsf{FindHS}_{\boldfacePi^0_1}\equiv_{\mathrm{W}}\mathsf{C}_\Baire$ (\thref{thm:findclopen=findclosed=cbaire}).
\end{proof}

\begin{corollary}
	\thlabel{cor:openRamsey_<_cbaire_x_openRamsey}
	$\boldfaceSigma^0_1\mathsf{-RT}<_\mathrm{W}  \mathsf{NHA}  \times \boldfaceSigma^0_1\mathsf{-RT} \le_{\mathrm{W}} \mathsf{C}_\Baire \times \boldfaceSigma^0_1\mathsf{-RT}.$
\end{corollary}
\begin{proof}
	The first reduction is straightforward and the second one follows from the fact that $ \mathsf{NHA} \le_{\mathrm{W}}\mathsf{C}_\Baire$ (see \cite[Cor.\ 3.6]{KMP20}). The fact that the first reduction is strict follows from \thref{prop:product_with_NHA} and the fact that $\boldfaceSigma^0_1\mathsf{-RT}\not\le_{\mathrm{W}}\mathsf{C}_\Baire$ (\thref{cor:openRamsey_not<_cbaire}).
\end{proof}

To have a better understanding of the uniform strength of $\boldfaceSigma^0_1\mathsf{-RT}$, we now show that, even with a parallel access to some hyperarithmetic computational power, $\boldfaceSigma^0_1\mathsf{-RT}$ does not reach the level of $\mathsf{TC}_\Baire\times \mathsf{C}_\Baire$. Thus $\boldfaceSigma^0_1\mathsf{-RT}$ is not at the level of $\mathsf{TC}_\Baire^*$, which is one of the strongest principles considered in \cite{KMP20} to be still at the level of $\mathrm{ATR}_0$.

\begin{proposition}
	\thlabel{thm:tcbaire_x_cbaire_not<_f_times_openRT}
	If $f\pmfunction{X}{Y}$ always has an hyperarithmetic solution relative to the input and $f\le_{\mathrm{W}} \mathsf{C}_\Baire$ then
	$\mathsf{TC}_\Baire\times \mathsf{C}_\Baire \not \le_{\mathrm{W}} f \times \boldfaceSigma^0_1\mathsf{-RT}$.
\end{proposition}
\begin{proof}
	Notice that, if we define $B:=\operatorname{dom}(\mathsf{wFindHS}_{\boldfaceSigma^0_1} )$, then
	\[ (f \times\boldfaceSigma^0_1\mathsf{-RT})\restrict{X \times B} = f \times\mathsf{wFindHS}_{\boldfaceSigma^0_1} . \]
	Since $\mathsf{wFindHS}_{\boldfaceSigma^0_1} \equiv_{\mathrm{W}}\mathsf{UC}_\Baire$ (\thref{cor:wfindclopen=ucbaire}) we have that $(f \times\boldfaceSigma^0_1\mathsf{-RT})\restrict{X \times B}$ always has a solution that is hyperarithmetic relative to the input (\thref{thm:ucbaire_hyperarithmetic_solution}). Assume by contradiction that the reduction $\mathsf{TC}_\Baire\times \mathsf{C}_\Baire \le_{\mathrm{W}}  f \times \boldfaceSigma^0_1\mathsf{-RT}$ holds. By \thref{prop:product_with_NHA_general} we have that $\mathsf{TC}_\Baire$ is reducible to the restriction of $f \times \boldfaceSigma^0_1\mathsf{-RT}$ to
	\[ A:= X \times (\setcomplement[\boldsymbol{\Sigma}^0_1({[\mathbb{N}]}^\mathbb{N} )]{B}) = X \times\operatorname{dom}(\mathsf{FindHS}_{\boldfacePi^0_1}). \]
	In particular this implies that $\mathsf{TC}_\Baire\le_{\mathrm{W}} f\times \mathsf{FindHS}_{\boldfacePi^0_1}$ (see also the proof of \thref{prop:product_with_NHA}). We have therefore reached a contradiction as we would have
	\begin{equation*}
		\mathsf{TC}_\Baire\le_{\mathrm{W}} f \times\mathsf{FindHS}_{\boldfacePi^0_1} \le_{\mathrm{W}} \mathsf{C}_\Baire\times \mathsf{C}_\Baire \equiv_{\mathrm{W}}  \mathsf{C}_\Baire.	\qedhere
	\end{equation*}
\end{proof}
In particular, \thref{thm:tcbaire_x_cbaire_not<_f_times_openRT} implies $\mathsf{TC}_\Baire\times \mathsf{C}_\Baire \not \le_{\mathrm{W}} \mathsf{UC}_\Baire \times \boldfaceSigma^0_1\mathsf{-RT}$.
\medskip

Let us now turn our attention to $\mathsf{FindHS}_{\boldfaceSigma^0_1} $. We first notice the following useful property:
\begin{proposition}
	\thlabel{prop:findHopen_closed_product}
	$\mathsf{FindHS}_{\boldfaceSigma^0_1}  \times \mathsf{FindHS}_{\boldfaceSigma^0_1}  \le_{\mathrm{sW}} \mathsf{FindHS}_{\boldfaceSigma^0_1} $.
\end{proposition}
\begin{proof}
	Let $\coding{P_1},\coding{P_2}$ be names for two open sets $P_1, P_2\in \operatorname{dom}(\mathsf{FindHS}_{\boldfaceSigma^0_1} )$. Assume w.l.o.g.\ that every string $\sigma \in \coding{P_1}$ has length at least $2$ (there is no loss of generality as we can computably modify the code of $P_1$ by replacing a string with length $1$ with all its extensions of length $2$).

	Let $P$ be the open set with name $\coding{P_1}\boxtimes \coding{P_2}$. Recall that $P$ is computable from $P_1$ and $P_2$ (see \thref{lem:computable_operations}). Moreover, by \thref{lem:opencodepairing_properties}
	\[ \mathrm{HS}(P)\cap P = \{ f\boxtimes g: f\in \mathrm{HS}(P_1)\cap P_1 \text{ and } g\in \mathrm{HS}(P_2)\cap P_2\}.  \]
	Since the projections $\pi_i$ are computable, it is clear that, from every solution of $\mathsf{FindHS}_{\boldfaceSigma^0_1} (P)$, we obtain two homogeneous solutions that land in $P_1$ and $P_2$ respectively.
\end{proof}

\begin{corollary}
	\thlabel{thm:findHopen_cylinder}
	$\mathsf{FindHS}_{\boldfaceSigma^0_1} $ is a cylinder.
\end{corollary}
\begin{proof}
	This follows from \thref{prop:findHopen_closed_product} and the fact that $\idBaire \le_{\mathrm{sW}} \mathsf{FindHS}_{\boldfaceSigma^0_1} $, as it then follows that
	\[ \idBaire \times \mathsf{FindHS}_{\boldfaceSigma^0_1}  \le_{\mathrm{sW}} \mathsf{FindHS}_{\boldfaceSigma^0_1}  \times \mathsf{FindHS}_{\boldfaceSigma^0_1}  \equiv_{\mathrm{sW}} \mathsf{FindHS}_{\boldfaceSigma^0_1} . \]
	To prove that $\idBaire\le_{\mathrm{sW}}\mathsf{FindHS}_{\boldfaceSigma^0_1} $ we proceed as follows: let $p\in{\mathbb{N}^\mathbb{N}}$ and assume w.l.o.g.\ that $p\in{[\mathbb{N}]}^\mathbb{N} $.
	Consider the tree $T:=\{ p[k]: k\in\mathbb{N} \}$ of prefixes of $p$ and let $D:=\describepath{}(T)$. By \thref{lem:clopen_describes_paths} we have that $D\in\operatorname{dom}(\mathsf{FindHS}_{\boldfaceSigma^0_1} )$ and that every $f\in \mathrm{HS}(D)\cap D$ uniformly computes $p$.
\end{proof}

The problem $\mathsf{FindHS}_{\boldfaceSigma^0_1} $ is much stronger than all of the other Ramsey-related problems we introduced. We will in fact show that $\boldfaceSigma^0_1\mathsf{-RT}<_\mathrm{W} \mathsf{FindHS}_{\boldfaceSigma^0_1} $ (and this holds even if we consider arithmetic reductions, see \thref{thm:openRamsey_arith<_findHopen}).

Although we will prove much stronger results it is worth it to sketch a short proof for the reduction $\boldfaceSigma^0_1\mathsf{-RT}\le_{\mathrm{W}}\mathsf{FindHS}_{\boldfaceSigma^0_1} $. Given a name $\coding{P}$ for an open set $P$ build the open set
\[ Q:=\elementpower{2}(\coding{P})\cup \describepath{\psi_3}(\closedsidesoltree{\coding{P}}),\]
where $\psi_3:=\sigma \mapsto 3^{\coding{\sigma}+1}$ and $\coding{\sigma}$ is the code of $\sigma$. Using \thref{lem:elementpower_preserves_solutions} and \thref{lem:clopen_describes_paths} one can prove that $Q\in\operatorname{dom}(\mathsf{FindHS}_{\boldfaceSigma^0_1} )$ and that every $f\in\mathrm{HS}(Q)\cap Q$ computes a solution for $P$.

\begin{proposition}
\thlabel{prop:tcbaire<=findHopen}
$\mathsf{sTC}_{\Baire} \le_{\mathrm{W}} \mathsf{FindHS}_{\boldfaceSigma^0_1} $ and hence $\chi_{\Pi^1_1}<_\mathrm{W}\mathsf{FindHS}_{\boldfaceSigma^0_1} $.
\end{proposition}
\begin{proof}
Let $\stringcodepower{n}:{\mathbb{N}^{<\mathbb{N}}}\to \mathbb{N}:=\sigma\mapsto n^{\coding{\sigma}+1}$, where $\coding{\sigma}$ is the code of $\sigma$.

Let $T\subset{[\mathbb{N}]}^{<\mathbb{N}} $ be a tree. We can define the open set $P\subset{[\mathbb{N}]}^\mathbb{N} $ as $P:=P_1 \cup P_2$, where $P_1 := \describepath{\stringcodepower{2}}(T)$ and $P_2 := \solovay{\stringcodepower{3}}(T)$.
Notice that, by \thref{lem:clopen_describes_paths} and \thref{lem:solutions_solovay_open_set} we have
\[ [T]=\emptyset \iff \mathrm{HS}(P_1)\cap P_1= \emptyset \iff  \mathrm{HS}(P_2)\cap P_2\neq\emptyset. \]
Moreover, by \thref{prop:sets_with_disjoint_solutions},
\[ \mathrm{HS}(P)\cap P=(\mathrm{HS}(P_1)\cap P_1) \cup (\mathrm{HS}(P_2)\cap P_2).  \]
This implies that
\begin{gather*}
	[T]\neq\emptyset \Rightarrow \mathrm{HS}(P)\cap P = \mathrm{HS}(P_1)\cap P_1, \\
	[T]=\emptyset \Rightarrow \mathrm{HS}(P)\cap P = \mathrm{HS}(P_2)\cap P_2.
\end{gather*}
In particular, given a $f\in \mathrm{HS}(P)\cap P$ we can know whether $f\in \mathrm{HS}(P_1)\cap P_1$ or $f\in \mathrm{HS}(P_2)\cap P_2$ just by checking $f(0)$. If $f(0)$ is a power of $2$ then $[T]\neq\emptyset$ and we can compute a path through $T$ by considering the string $x\in {[\mathbb{N}]}^\mathbb{N} $ s.t.\
\[ x = \bigcup_{i\in\mathbb{N}} \stringcodepower{2}^{-1}(f(i)).  \]
In the other case $[T]=\emptyset$ hence we can just return $\coding{0}\raisebox{.9ex}{\ensuremath\smallfrown}  f$.

The result about $\chi_{\Pi^1_1}$ follows from $\chi_{\Pi^1_1}\le_{\mathrm{W}}\mathsf{sTC}_{\Baire}$ and $\mathsf{sTC}_{\Baire}\not\le_{\mathrm{W}}\chi_{\Pi^1_1}$ as $\chi_{\Pi^1_1}$ always has computable output.
\end{proof}

\begin{corollary}
	\thlabel{thm:tcbaire^*<findHopen}
	$\mathsf{TC}_\Baire^* <_\mathrm{W} \mathsf{FindHS}_{\boldfaceSigma^0_1} $.
\end{corollary}
\begin{proof}
	The reduction follows from $\mathsf{TC}_\Baire\le_{\mathrm{W}}\mathsf{FindHS}_{\boldfaceSigma^0_1} $ (\thref{prop:tcbaire<=findHopen}) and the fact that $\mathsf{FindHS}_{\boldfaceSigma^0_1} $ is closed under product (\thref{prop:findHopen_closed_product}).
	The fact the reduction is strict follows from the fact that $\mathsf{FindHS}_{\boldfaceSigma^0_1} $ computes $\chi_{\Pi^1_1}$ (\thref{prop:tcbaire<=findHopen}), while $\mathsf{TC}_\Baire^*$ does not (\cite[Cor.\ 8.6]{KMP20}).
\end{proof}

This shows that $\mathsf{FindHS}_{\boldfaceSigma^0_1} $ is properly stronger than any multivalued function arising from statements related to $\mathrm{ATR}_0$ studied so far.

\begin{theorem}
	\thlabel{thm:lim^n*openRT<=findHopen}
	$\mathsf{C}_\Baire*\boldfaceSigma^0_1\mathsf{-RT} \le_{\mathrm{W}} \mathsf{FindHS}_{\boldfaceSigma^0_1} $.
\end{theorem}
\begin{proof}
	By the cylindrical decomposition we can write
	\[ \mathsf{C}_\Baire*\boldfaceSigma^0_1\mathsf{-RT} \equiv_{\mathrm{W}} \mathsf{C}_\Baire\circ \Phi_e \circ (\id{}\times \boldfaceSigma^0_1\mathsf{-RT}) \]
	for some computable function $\Phi_e$. It is enough to show that
	\[ \mathsf{C}_\Baire\circ\Phi_e\circ (\id{}\times\boldfaceSigma^0_1\mathsf{-RT})\le_{\mathrm{W}} \mathsf{FindHS}_{\boldfaceSigma^0_1} \times \mathsf{FindHS}_{\boldfaceSigma^0_1} \times \chi_{\Pi^1_1} \]
	and the claim will follow from $\chi_{\Pi^1_1}\le_{\mathrm{W}}\mathsf{FindHS}_{\boldfaceSigma^0_1} $ (\thref{prop:tcbaire<=findHopen}) and the fact that $\mathsf{FindHS}_{\boldfaceSigma^0_1} $ is closed under product (\thref{prop:findHopen_closed_product}).

	Let $\coding{p_1,p_2}$ be an input for $\mathsf{C}_\Baire\circ\Phi_e\circ (\id{}\times\boldfaceSigma^0_1\mathsf{-RT})$ and let $P$ be the open set with name $p_2$. We can consider the tree $\closedsidesoltree{p_2}$ of homogeneous solutions for $P$ that avoid $P$. We can now compute a tree $R$ s.t.\ for every $x,y\in{\mathbb{N}^\mathbb{N}}$,
	\[x\in [\closedsidesoltree{p_2}] \text{ and } y\in [\Phi_e (p_1,x)] \iff \coding{x,y}\in [R].  \]
	Using the canonical computable bijection between ${\mathbb{N}^\mathbb{N}}$ and ${[\mathbb{N}]}^\mathbb{N} $ it is easy to transform $R$ into a tree $S\in \mathbf{Ti}$ so that from any path through $S$ we can compute a path through $R$.

	Recall that $\mathsf{TwFindHS}_{\boldfaceSigma^0_1} \le_{\mathrm{W}}\mathsf{C}_\Baire$ (see \thref{thm:twfindopen<=atr2}). Since $\mathsf{C}_\Baire$ is closed under compositional product we have that $\mathsf{C}_\Baire\circ\Phi_e\circ (\id{}\times\mathsf{TwFindHS}_{\boldfaceSigma^0_1} )\le_{\mathrm{W}} \mathsf{C}_\Baire$. Let $\Phi_A,\Psi_A$ be two computable maps witnessing the reduction. In particular, $\Phi_A(\coding{p_1,p_2})$ is an ill-founded subtree of ${\mathbb{N}^{<\mathbb{N}}}$ and every path through $\Phi_A(\coding{p_1,p_2})$ computes a solution for $\mathsf{C}_\Baire\circ\Phi_e\circ (\id{}\times\mathsf{TwFindHS}_{\boldfaceSigma^0_1} )$ via $\Psi_A$. Let also $\stringcodepower{n}$ be the function that maps $\sigma$ to $n^{\coding{\sigma}+1}$, where $\coding{\sigma}$ is the code of $\sigma$.

	Let $D:= \describepath{\psi_2}(S)$ and define
	\begin{gather*}
		U:= D \cup \describepath{\psi_3}(\Phi_A(\coding{p_1,p_2}));\\
		V:= D \cup \solovay{\psi_3}(S).
	\end{gather*}

	Let us first show that $U,V\in \operatorname{dom}(\mathsf{FindHS}_{\boldfaceSigma^0_1} )$. Notice that if $P\in\operatorname{dom}(\mathsf{FindHS}_{\boldfacePi^0_1})$ then $[\closedsidesoltree{p_2}]\neq \emptyset$ and $[S]\neq\emptyset$. By \thref{lem:clopen_describes_paths} we have that $\mathrm{HS}(D)\cap D\neq\emptyset$ and therefore $U,V\in\operatorname{dom}(\mathsf{FindHS}_{\boldfaceSigma^0_1} )$. On the other hand, assume $P\notin\operatorname{dom}(\mathsf{FindHS}_{\boldfacePi^0_1})$. Since $\mathsf{TwFindHS}_{\boldfaceSigma^0_1} $ is total we have that $\Phi_A(\coding{p_1,p_2})$ is ill-founded. This implies that $\describepath{\psi_3}(\Phi_A(\coding{p_1,p_2}))$ has solutions that land in itself (again by \thref{lem:clopen_describes_paths}), and hence $U\in\operatorname{dom}(\mathsf{FindHS}_{\boldfaceSigma^0_1} )$. Moreover, since $P\notin\operatorname{dom}(\mathsf{FindHS}_{\boldfacePi^0_1})$ we have that $[S]=\emptyset$ and therefore $\mathrm{HS}(\solovay{\psi_3}(S))\cap \solovay{\psi_3}(S)\neq \emptyset$, which shows that $V\in\operatorname{dom}(\mathsf{FindHS}_{\boldfaceSigma^0_1} )$.

	Let $(f,g,b)\in (\mathsf{FindHS}_{\boldfaceSigma^0_1} \times \mathsf{FindHS}_{\boldfaceSigma^0_1} \times \chi_{\Pi^1_1})(U,V,S)$. We distinguish $2$ cases:
\begin{itemize}
	\item if $b=1$ then $[S]=\emptyset$, and hence $P\in \operatorname{dom}(\mathsf{wFindHS}_{\boldfaceSigma^0_1} )$. By \thref{prop:sets_with_disjoint_solutions} $f$ lands in $\describepath{\psi_3}(\Phi_A(\coding{p_1,p_2}))$.

	In particular $f$ computes a path through $\Phi_A(\coding{p_1,p_2})$ (\thref{lem:clopen_describes_paths}). Moreover $\mathsf{TwFindHS}_{\boldfaceSigma^0_1} (P)=\mathrm{HS}(P)=\boldfaceSigma^0_1\mathsf{-RT}(P)$, so that $f$ computes also a solution for the compositional product (by applying $\Psi_A$ to the path).
	\item if $b=0$ then $[S]\neq\emptyset$ and hence $P\in\operatorname{dom}(\mathsf{FindHS}_{\boldfacePi^0_1})$. Moreover $\mathrm{HS}(V)\cap V = \mathrm{HS}(D)\cap D$. Indeed, by \thref{prop:sets_with_disjoint_solutions},
	\[ \mathrm{HS}(V)\cap V = (\mathrm{HS}(D)\cap D)\cup (\mathrm{HS}(\solovay{\psi_3}(S)) \cap \solovay{\psi_3}(S)) \]
	and $\mathrm{HS}(\solovay{\psi_3}(S)) \cap \solovay{\psi_3}(S)=\emptyset$ by \thref{lem:solutions_solovay_open_set}.
	In this case $g$ computes a path through $S$, hence a path through $R$, and eventually a solution for the compositional product (by projecting the path through $R$).
\end{itemize}
	The previous two points describe a way to compute a solution for the compositional product given a solution to $\mathsf{FindHS}_{\boldfaceSigma^0_1} \times \mathsf{FindHS}_{\boldfaceSigma^0_1} \times \chi_{\Pi^1_1}$, and therefore conclude the proof.
\end{proof}

Notice that if $P\notin\operatorname{dom}(\mathsf{wFindHS}_{\boldfaceSigma^0_1} )$ then we cannot (in general) use $U$ to compute a solution for the compositional product. Indeed, it may be that $\mathrm{HS}(P)\cap P\neq \emptyset$ and the solution obtained from $\mathsf{FindHS}_{\boldfaceSigma^0_1} (U)$ lands in $\describepath{\psi_3}(\Phi_A(\coding{p_1,p_2}))$. However, since every string is a valid solution for $\mathsf{TwFindHS}_{\boldfaceSigma^0_1} (P)$, the solution we obtain is not guaranteed to have any connection with the original problem.

Notice moreover that $\boldfaceSigma^0_1\mathsf{-RT}<_\mathrm{W}\mathsf{FindHS}_{\boldfaceSigma^0_1} $ as the former is not closed under product with $\mathsf{C}_\Baire$ (\thref{cor:openRamsey_<_cbaire_x_openRamsey}) while the latter is closed under product (\thref{prop:findHopen_closed_product}) and computes $\mathsf{C}_\Baire$ (see \thref{prop:tcbaire<=findHopen}). We will prove a stronger result in \thref{thm:openRamsey_arith<_findHopen}.

\subsection{A \texorpdfstring{$0-1$}{0-1} law for strong Weihrauch reducibility}
\label{subsec:strong_wei}
We now characterize the strength of the Ramsey-related multivalued functions from the point of view of strong Weihrauch reducibility.

\begin{proposition}
	\thlabel{thm:strong_wei_characterization}
	Let $\boldsymbol{\Gamma}$ be a definable (boldface) pointclass that is downward closed with respect to Wadge reducibility. Assume also that every $P\in\boldsymbol{\Gamma}({[\mathbb{N}]}^\mathbb{N} )$ is Ramsey and that, for every $h\in{[\mathbb{N}]}^\mathbb{N} $,
	\[ \boldsymbol{\Gamma}([h]^\mathbb{N}) = \{ P\cap [h]^\mathbb{N} : P \in \boldsymbol{\Gamma}({[\mathbb{N}]}^\mathbb{N} ) \}. \]
	If $\mathsf{R}\pmfunction{\boldsymbol{\Gamma}({[\mathbb{N}]}^\mathbb{N} )}{{[\mathbb{N}]}^\mathbb{N} }$ is a multivalued function, s.t.\ for every $x\in\operatorname{dom}(\mathsf{R})$, $\mathsf{R}(x)=\mathrm{HS}(x)$, then
	\[ \id{2} \not\le_{\mathrm{sW}} \mathsf{R}. \]
	In particular $\id{2}$ (and, a fortiori, $\mathsf{UC}_\Baire$) is not strongly Weihrauch reducible to $\mathsf{wFindHS}_{\boldfaceSigma^0_1} $, $\mathsf{wFindHS}_{\boldfacePi^0_1}$, $\mathsf{wFindHS}_{\boldfaceDelta^0_1}$, $\boldfaceSigma^0_1\mathsf{-RT}$, $\boldfaceDelta^0_1\mathsf{-RT}$.
\end{proposition}
\begin{proof}
	Assume there is a strong Weihrauch reduction witnessed by the computable maps $\Phi,\Psi$. Let $p_i:=\Phi(i)$ (with a small abuse of notation we are identifying $i$ with its name) and let $P_i:=\repmap{\boldsymbol{\Gamma}({[\mathbb{N}]}^\mathbb{N} )}(p_i)$. By definition of strong Weihrauch reducibility, for every $f\in\mathrm{HS}(P_i)$ we have $\Psi(f)=i$. Fix $f\in\mathrm{HS}(P_0)$ and consider the set $[f]^\mathbb{N}\cap P_1 \in \boldsymbol{\Gamma}([f]^\mathbb{N})$. By \thref{prop:galvin_prikry_subset} we have that every pointset in $\boldsymbol{\Gamma}([f]^\mathbb{N})$ has the Ramsey property, therefore there is a $g\preceq f$ s.t.\ $[g]^\mathbb{N}\subset P_1 \cap [f]^\mathbb{N}$ or $[g]^\mathbb{N}\subset \setcomplement[{[f]^\mathbb{N}}]{P_1}$. In both cases $g\in\mathrm{HS}(P_1)$ and therefore $\Psi(g)=1$. However $g\preceq f$, hence $g\in\mathrm{HS}(P_0)$ and so $\Psi(g)=0$, which is a contradiction.
\end{proof}

On the other hand, \thref{thm:findclopen=findclosed=cbaire} shows that $\mathsf{C}_\Baire\equiv_{\mathrm{sW}} \mathsf{FindHS}_{\boldfacePi^0_1} \equiv_{\mathrm{sW}} \mathsf{FindHS}_{\boldfaceDelta^0_1}$, which implies that $\mathsf{FindHS}_{\boldfacePi^0_1}$ and $\mathsf{FindHS}_{\boldfaceDelta^0_1}$ are cylinders. Since $\mathsf{FindHS}_{\boldfaceSigma^0_1} $ is also a cylinder (\thref{thm:findHopen_cylinder}) we have that, for every $g$ and every $f\in \{\mathsf{FindHS}_{\boldfaceSigma^0_1} ,\mathsf{FindHS}_{\boldfacePi^0_1},\mathsf{FindHS}_{\boldfaceDelta^0_1} \}$
\[ g\le_{\mathrm{W}} f \iff g \le_{\mathrm{sW}} f. \]
This shows that, from the point of view of strong Weihrauch reducibility, the principles related to the open and clopen Ramsey theorems are either very weak (they do not strongly uniformly compute the identity on the $2$-element space) or they are as strong as possible (the notions of Weihrauch reducibility and strong Weihrauch reducibility coincide).

\section{Arithmetic Weihrauch reducibility}
\label{sec:artihemtic_reducibility}
Let us now define the notion of arithmetic Weihrauch reducibility, which is obtained by relaxing the computability requirements in the definition of Weihrauch reducibility. This was introduced in \cite[Def.\ 1.4]{GohThesis} (see also \cite[Def.\ 2.2]{GohWCWO} and \cite[Sec.\ 2.4]{KiharaADauriacChoice}).

\begin{definition}[Arithmetic Weihrauch reducibility]
Let $f\pmfunction{X}{Y}$, $g\pmfunction{Z}{W}$ be partial multivalued functions between represented spaces. We say that
$f$ is \textdef{arithmetically Weihrauch reducible} to $g$, and we write $f\le^a_{\mathrm{W}} g$, if
\[ (\exists \text{ arithmetic } \Phi,\Psi:\subseteq{\mathbb{N}^\mathbb{N}}\to{\mathbb{N}^\mathbb{N}})(\forall G \vdash g )~ \Psi\coding{ (\idBaire, G\Phi) } \vdash f \]
where a function $F:\subseteq{\mathbb{N}^\mathbb{N}}\to{\mathbb{N}^\mathbb{N}}$ is called \textdef{arithmetic} if there is $n\in\mathbb{N}$ s.t.\ $F\le_{\mathrm{W}} \mathsf{lim}^{(n)}$.
\end{definition}
It is straightforward to see that $f\le_{\mathrm{W}} g \Rightarrow f \le^a_{\mathrm{W}} g$. Notice moreover that if $f \le^a_{\mathrm{W}} g$ then there exists $n$ s.t.\ $f\le_{\mathrm{W}} \mathsf{lim}^{(n)}* g * \mathsf{lim}^{(n)}$ (this follows directly from the definition of the compositional product).

\begin{proposition}
	\thlabel{thm:f_arith<_id}
	For every multivalued function $f$
	\[ (\exists n)(f\le_{\mathrm{W}} \mathsf{lim}^{(n)}) \Rightarrow f\le^a_{\mathrm{W}} \id{}. \]
\end{proposition}
\begin{proof}
	Assume there is a strong reduction $f\le_{\mathrm{sW}}\mathsf{lim}^{(n)}$ witnessed by the computable maps $\Phi_f,\Psi_f$. It is easy to see that the maps $\Phi:= \Psi_f\circ \mathsf{lim}^{(n)} \circ \Phi_f$ and $\Psi:= \id{}$ witness the reduction $f\le^a_{\mathrm{W}} \id{}$.
\end{proof}

\begin{corollary}
\thlabel{prop:ccantor_arith_equiv_id}
$\id{}\equiv^a_{\mathrm{W}} \mathsf{C}_\Cantor  \equiv^a_{\mathrm{W}}  \mathsf{LPO}  \equiv^a_{\mathrm{W}} \mathsf{lim}^{(n)}$.
\end{corollary}
\begin{proof}
	Straightforward from \thref{thm:f_arith<_id} and the fact that $\id{}$ is Weihrauch reducible to $\mathsf{C}_\Cantor$, $ \mathsf{LPO} $ and $\mathsf{lim}^{(n)}$.
\end{proof}

\begin{proposition}
\thlabel{prop:compprod_arith_reduction}
For every (partial) multivalued functions $f,g$, if $f\le^a_{\mathrm{W}} \id{}$ then $f* g \equiv^a_{\mathrm{W}} g* f \equiv^a_{\mathrm{W}} g$.
\end{proposition}
\begin{proof}
Let us first prove $f* g \equiv^a_{\mathrm{W}} g$, the other equivalence is analogous. We only need to prove that $f* g \le^a_{\mathrm{W}} g$ as the converse reduction is trivial. We can assume w.l.o.g.\ that $f,g$ are (partial) multivalued functions $\pmfunction{{\mathbb{N}^\mathbb{N}}}{{\mathbb{N}^\mathbb{N}}}$ (see e.g.\ \cite[Lem.\ 3.8]{BGP17}).
By the cylindrical decomposition, we can write
	\[ f* g \equiv_{\mathrm{W}} (\id{} \times f) \circ \Phi_e \circ (\id{}\times g)  \]
for some computable $\Phi_e$. In particular
	\[ (\id{}\times f )\circ \Phi_e \circ (\id{}\times g)(\coding{p_1,p_2}) = \coding{\Phi_1(p_1, g(p_2)),f\circ \Phi_2(p_1, g(p_2)) }\]
where $\Phi_1,\Phi_2$ are the computable functions s.t.\ $\Phi_e(p)=\coding{\Phi_1(p),\Phi_2(p)}$.

Let $\Phi_f, \Psi_f$ be two arithmetic maps witnessing the reduction $f \le^a_{\mathrm{W}} \id{}$. It is straightforward to see that the maps
\[ \Phi := \coding{p_1,p_2}\mapsto p_2, \]
\[ \Psi := (\coding{p_1,p_2}, q) \mapsto \coding{\Phi_1(p_1, q),\Psi_f(\Phi_2(p_1,q), \Phi_f \Phi_2(p_1, q)) }\]
witness the reduction $(\id{} \times f) \circ \Phi_e \circ (\id{}\times g) \le^a_{\mathrm{W}} g$.
\end{proof}

\begin{corollary}
\thlabel{cor:wfindHclosed_arith_equiv_cbaire}
$\mathsf{wFindHS}_{\boldfacePi^0_1} \equiv^a_{\mathrm{W}} \mathsf{C}_\Baire$.
\end{corollary}
\begin{proof}
This follows from $\mathsf{C}_\Baire \equiv_{\mathrm{W}} \mathsf{C}_\Cantor * \mathsf{wFindHS}_{\boldfacePi^0_1}$ (\thref{prop:wfindHclosed<=cbaire}), using \thref{prop:ccantor_arith_equiv_id} and \thref{prop:compprod_arith_reduction}.
\end{proof}

\begin{lemma}
	\thlabel{lem:arit_reduction_implies_normal_reduction}
	Let $g$ be a (partial multivalued) function that computes every arithmetic function and is closed under compositional product. For every (partial) multivalued function $f$
	\[ f\le^a_{\mathrm{W}} g \Rightarrow f \le_{\mathrm{W}} g. \]
\end{lemma}
\begin{proof}
	It is enough to notice that $f\le^a_{\mathrm{W}} g$ implies that there exists $n$ s.t.
	\[ f\le_{\mathrm{W}} \mathsf{lim}^{(n)}* g * \mathsf{lim}^{(n)}.\]
	The hypotheses on $g$ immediately yield the claim.
\end{proof}

\begin{corollary}
	\thlabel{thm:cbaire_arith<_tcbaire}
$\mathsf{C}_\Baire<^a_\mathrm{W}\mathsf{TC}_\Baire$.
\end{corollary}
\begin{proof}
The fact that $\mathsf{C}_\Baire\le^a_{\mathrm{W}} \mathsf{TC}_\Baire$ is trivial as $\mathsf{C}_\Baire\le_{\mathrm{W}}\mathsf{TC}_\Baire$. The separation follows from \thref{lem:arit_reduction_implies_normal_reduction} (recall that, for every $n$, $\mathsf{lim}^{(n)}\le_{\mathrm{W}} \mathsf{UC}_\Baire$, see \cite[Prop.\ 7.50]{BGP17}) and the fact that $\mathsf{TC}_\Baire\not\le_{\mathrm{W}}\mathsf{C}_\Baire$.
\end{proof}

\begin{theorem}
	$\mathsf{TC}_\Baire\equiv^a_{\mathrm{W}} \mathsf{sTC}_{\Baire}$.
\end{theorem}
\begin{proof}
	This follows from \thref{thm:f_arith<_id}, \thref{prop:compprod_arith_reduction} and the fact that
	\begin{equation*}
	\mathsf{TC}_\Baire \le_{\mathrm{W}} \mathsf{sTC}_{\Baire} \le_{\mathrm{W}}  \mathsf{LPO} *\mathsf{TC}_\Baire.\qedhere
	\end{equation*}
\end{proof}

We will now prove the fact that $\mathsf{TC}_\Baire<^a_\mathrm{W}\boldfaceSigma^0_1\mathsf{-RT}$. To do so we will first need some additional results about compositional products of iterations of $\mathsf{lim}$ and $\mathsf{TC}_\Baire$.

\begin{lemma}
	\thlabel{thm:pi11_predicate}
	Let $D(X,Y, Z)$ be an arithmetic predicate with free variables among $X,Y,Z$ and let $\Phi\colon{\mathbb{N}^\mathbb{N}}\times{\mathbb{N}^\mathbb{N}}\to \mathbf{Tr}$ be computable. Define the $\Pi^1_1$ predicate $P(X, Y, Z)$ as
	\[ D(X,Y, Z) \land ([\Phi(X,Y)]\neq\emptyset \rightarrow Z\in[\Phi(X,Y)]). \]
	There exists a $\Pi^0_1$ predicate $S(X, Y, Z, W)$ s.t.\ an index for $S$ is computable from indices for $D$ and $\Phi$ s.t.
	\begin{gather*}
		(\exists W)( S(X, Y,Z,W) )\Rightarrow D(X,Y,Z) , \\
		[\Phi(X,Y)]\neq \emptyset \Rightarrow (~ P(X,Y,Z) \iff (\exists W)(S(X, Y,Z,W))~).
	\end{gather*}
\end{lemma}
\begin{proof}
	By Kleene's normal form theorem (see e.g.\ \cite[Thm.\ 16.IV]{Rogers67}), there is a $\Pi^0_1$ predicate $T$ s.t.\
	\[ D(X,Y,Z) \iff (\exists W)(T(X,Y,Z,W)). \]
	Define the $\Pi^0_1$ predicate $S(X,Y,Z,W):= T(X,Y,Z,W) \land Z\in [\Phi(X,Y)]$. It follows from Kleene's normal form theorem that an index for $S$ is computable from indices for $D$ and $\Phi$. The first property of $S$ is immediate. For the second notice that, if $[\Phi(X,Y)]\neq \emptyset$ then
	\begin{align*}
		P(X,Y,Z)  & \iff D(X,Y,Z) \land Z\in [\Phi(X,Y)]\\
			&  \iff (\exists W)(T(X,Y,Z,W) \land Z\in [\Phi(X,Y)]) \\
			&  \iff (\exists W)(S(X,Y,Z,W)).\qedhere
	\end{align*}
\end{proof}

The previous lemma can be interpreted as follows: the predicate $P$ describes the compositional product (on both sides) of $\mathsf{TC}_\Baire$ with an arithmetic problem $f$, while $D$ says that $Y$ is a solution for $f(X,Z)$. Notice that, if we are considering the composition $\mathsf{TC}_\Baire* f$ then $f$ (and therefore $D$) will not depend on the output $Z$ of $\mathsf{TC}_\Baire$. On the other hand, if we consider $f* \mathsf{TC}_\Baire$ then we need to keep track of $Z$. The lemma proves that there is a uniform way to build a tree (whose body is the set of solutions to $S$) s.t., by projecting its paths, we can obtain the solutions to the original problem $P$. Notice however that the lemma does not guarantee such a tree to be ill-founded. In other words, we can recover (some) solutions to the original problem only if the tree is ill-founded.

Obviously, if $D$ depends only on $X,Y$ and not on $Z$, then a solution for $D$ can be (arithmetically) computed without first finding a path through the tree $\Phi(X,Y)$.

\begin{lemma}
	\thlabel{thm:tcbaire*lim=tcbaire_x_lim}
	For every $n\in\mathbb{N}$, $\mathsf{TC}_\Baire* \mathsf{lim}^{(n)} \equiv_{\mathrm{W}} \mathsf{TC}_\Baire\times \mathsf{lim}^{(n)}.$
\end{lemma}
\begin{proof}
	Fix $n\in\mathbb{N}$. The reduction $\mathsf{TC}_\Baire\times \mathsf{lim}^{(n)}\le_{\mathrm{W}} \mathsf{TC}_\Baire*\mathsf{lim}^{(n)}$ trivially follows from the algebraic rules of the operations (see \cite[Prop.\ 4.4]{BP16}).

	To prove the converse reduction, by the cylindrical decomposition we can write
	\[ \mathsf{TC}_\Baire*\mathsf{lim}^{(n)}\equiv_{\mathrm{W}} (\id{} \times \mathsf{TC}_\Baire)\circ \Phi_e \circ \mathsf{lim}^{(n)}, \]
	for some computable function $\Phi_e$. In particular
	\[ (\id{} \times \mathsf{TC}_\Baire)\circ \Phi_e \circ \mathsf{lim}^{(n)}(p) = \coding{\Phi_1(\mathsf{lim}^{(n)}(p) ), \mathsf{TC}_\Baire \Phi_2(\mathsf{lim}^{(n)}(p) )} \]
	where $\Phi_1,\Phi_2$ are the computable functions s.t.\ $\Phi_e(p)=\coding{\Phi_1(p),\Phi_2(p)}$.

	Let $D(X,Y)$ be the predicate that says
	\[ Y = \coding{\Phi_1(\mathsf{lim}^{(n)}(X) ),  \Phi_2(\mathsf{lim}^{(n)}(X) )}. \]
	Notice that an index for $D$ can be (uniformly) computed from an index of $\Phi_e$. Define also the predicate $P(X,Y,Z)$ as
	\[ \quad D(X,Y) \land ([\pi_2 (Y)]\neq\emptyset\rightarrow Z\in [\pi_2 (Y)]), \]
	where $\pi_2:=\coding{Y_1,Y_2}\mapsto Y_2$. Since $D(X,Y)$ is arithmetic, we can use \thref{thm:pi11_predicate} to define a computable tree $S$ s.t.\
	\begin{gather*}
		(\exists W)( (X, Y,Z,W)\in[S] )\Rightarrow D(X,Y) , \\
		[\pi_2(Y)]\neq \emptyset \Rightarrow (~ P(X,Y,Z) \iff (\exists W)((X, Y,Z,W)\in [S] )~).
	\end{gather*}

	For every fixed $p\in \operatorname{dom}((\id{} \times \mathsf{TC}_\Baire)\circ \Phi_e \circ \mathsf{lim}^{(n)})$ we define $S_p:=\{ \sigma : \coding{p[\abslength{\sigma}],\sigma}\in S \}$. We now claim that, from an answer to $(\mathsf{TC}_\Baire\times\mathsf{lim}^{(n)})([S_p],p)$ we can compute a solution to $(\id{} \times \mathsf{TC}_\Baire)\circ \Phi_e \circ \mathsf{lim}^{(n)}(p)$.

	Indeed $\Phi_1\circ \mathsf{lim}^{(n)}(p)$ is trivially uniformly computed from $\mathsf{lim}^{(n)}(p)$. On the other hand, there is a unique $q$ s.t.\ $D(p,q)$. Assume $[\pi_2(q)]\neq\emptyset$ and let $z_0 \in[\pi_2(q)]$. Since $P(p,q,z_0)$ holds, we have that $(\exists w)(\coding{q,z_0,w}\in [S_p])$, in particular $[S_p]\neq\emptyset$. Let $\coding{y,z,w}\in\mathsf{TC}_\Baire([S_p])$. Notice that, since $\mathsf{lim}^{(n)}$ is single-valued, we have $y=q$. Hence we can conclude that $P(p,q,z)$ holds, and therefore, by projecting $\coding{y,z,w}$ on the second component we obtain a path through $[\pi_2(q)]$. If, on the other hand, $[\pi_2(q)]=\emptyset$, then any $z$ belongs to $\mathsf{TC}_\Baire([\pi_2(q)])$. In both cases, by projecting the output of $\mathsf{TC}_\Baire([S_p])$ we can compute a solution to $(\mathsf{TC}_\Baire\circ \Phi_2\circ \mathsf{lim}^{(n)})(p)$ and this concludes the proof.
\end{proof}

\begin{lemma}
	\thlabel{thm:lim^n*tcbaire_<_lpo*tcbaire_x_lim^k}
	For every $n\in\mathbb{N}$, $\mathsf{lim}^{(n)}*\mathsf{TC}_\Baire \le_{\mathrm{W}} \mathsf{sTC}_{\Baire} \times \mathsf{lim}^{(3n+5)}.$
\end{lemma}
\begin{proof}
    Fix $n\in\mathbb{N}$. By the cylindrical decomposition we can write
	\[ \mathsf{lim}^{(n)}*\mathsf{TC}_\Baire\equiv_{\mathrm{W}} \mathsf{lim}^{(n)}\circ \Phi_e \circ (\id{} \times\mathsf{TC}_\Baire) \]
	for some computable function $\Phi_e$.

	Let us define $F\mfunction{{\mathbb{N}^\mathbb{N}}\times{\mathbb{N}^\mathbb{N}}}{{\mathbb{N}^\mathbb{N}}}$ as $F:= \mathsf{T}(\mathsf{lim}^{(n)}\circ \Phi_e)$. Recalling that $\mathsf{lim}^{(n)}=\mathsf{lim}^{[n+1]}$, it is immediate that being in the domain of $\mathsf{lim}^{(n)}$ is a $\Pi^0_{2n+3}$ property. On the other hand, whether $\Phi_e(p,q)$ is defined is a $\Pi^0_2$ property. This implies that $F\le_{\mathrm{W}} \mathsf{lim}^{[2n+5+n+1]}=\mathsf{lim}^{(3n+5)}$ and hence to prove the lemma it suffices to show that $ \mathsf{lim}^{(n)}\circ \Phi_e \circ (\id{} \times\mathsf{TC}_\Baire)\le_{\mathrm{W}} \mathsf{sTC}_{\Baire} \times F$.

	Let $D(X,Y,Z)$ be the arithmetic predicate
	\[ Y = \mathsf{lim}^{(n)}\circ \,\Phi_e(\pi_1(X), Z). \]
	Clearly an index for $D$ is computable from an index of $\Phi_e$. Let also $P(X,Y,Z)$ be the predicate
	\[ D(X,Y,Z) \land ([\pi_2(X)]\neq\emptyset \rightarrow Z\in [\pi_2(X)]). \]

	Since $D(X,Y,Z)$ is arithmetic, we can use \thref{thm:pi11_predicate} to define a computable tree $S$ s.t.\
	\begin{gather*}
		(\exists W)( (X, Y,Z,W)\in[S] )\Rightarrow D(X,Y,Z) , \\
		[\pi_2(X)]\neq \emptyset \Rightarrow (~ P(X,Y,Z) \iff (\exists W)((X, Y,Z,W)\in [S] )~).
	\end{gather*}

	For every fixed $p=\coding{p_1,p_2}\in \operatorname{dom}(\mathsf{lim}^{(n)}\circ \Phi_e \circ (\id{} \times\mathsf{TC}_\Baire))$ we define $S_p:=\{ \sigma : \coding{p[\abslength{\sigma}],\sigma}\in S \}$.
	We define the forward Weihrauch functional as the map $\Phi:=\coding{p_1,p_2} \mapsto ([S_p], (p_1,0^\omega))$. Notice that, since $F$ is total, $\Phi(\coding{p_1,p_2})$ is a correct input for $\mathsf{sTC}_{\Baire}\times F$. Let $(\coding{b}\raisebox{.9ex}{\ensuremath\smallfrown}  \coding{y,z,w},r)\in (\mathsf{sTC}_{\Baire}\times F)([S_p], (p_1,0^\omega))$. We claim that a solution for $\mathsf{lim}^{(n)}\,\Phi_e (p_1,\mathsf{TC}_\Baire(p_2))$ is $y$ if $b=1$ or is $r$ if $b=0$.

    Assume that $b=1$, i.e.\ that $\coding{y,z,w}\in [S_p]$. Then $D(\coding{p_1,p_2},y,z)$ holds, i.e.\ $y=\mathsf{lim}^{(n)}(\Phi_e(p_1,z))$. Therefore it is enough to show that $z\in\mathsf{TC}_\Baire([p_2])$. Assume that $[p_2]\neq\emptyset$ (the other case is trivial). Since $\coding{y,z,w}\in [S_p]$, we have that $P(\coding{p_1,p_2},y,z)$ holds and therefore $z\in [p_2]$.

    Assume now that $b=0$, i.e.\ for all $y,z$ there is no $w$ s.t.\ $\coding{y,z,w}\in[S_p]$. If $[p_2]\neq\emptyset$ then choose $z\in [p_2]$ and let $y=\mathsf{lim}^{(n)}\Phi_e(p_1,z)$. We then have that $D(\coding{p_1,p_2},y,z)$ and $P(\coding{p_1,p_2},y,z)$ hold. Therefore there exists $w$ s.t.\ $\coding{y,z,w}\in[S_p]$, which is a contradiction. This implies that $[p_2]=\emptyset$ and therefore $0^\omega \in\mathsf{TC}_\Baire([p_2])$ and $(p_1,0^\omega)\in\operatorname{dom}(\mathsf{lim}^{(n)}\Phi_e)$. Therefore $r=F(p_1,0^\omega)\in \mathsf{lim}^{(n)}\Phi_e(p_1,\mathsf{TC}_\Baire([p_2]))$ and this concludes the proof.
\end{proof}
We are now ready to prove the following characterization of arithmetic reducibility to $\mathsf{TC}_\Baire$, conjectured by Arno Pauly during the BIRS-CMO 2019 workshop ``Reverse Mathematics of Combinatorial Principles".
\begin{theorem}
	\thlabel{thm:arith_reduction_tcbaire}
	For every multivalued function $f$,
	\[ f\le^a_{\mathrm{W}} \mathsf{TC}_\Baire \iff (\exists n)(f\le_{\mathrm{W}} \mathsf{sTC}_{\Baire}\times \mathsf{lim}^{(n)}). \]
\end{theorem}
\begin{proof}
	The right-to-left implication follows from \thref{prop:ccantor_arith_equiv_id} and \thref{prop:compprod_arith_reduction}, as $\mathsf{sTC}_{\Baire} \le_{\mathrm{W}}  \mathsf{LPO} *\mathsf{TC}_\Baire$.

	To prove the left-to-right implication, assume that there exists $m$ s.t.\ $f\le_{\mathrm{W}} \mathsf{lim}^{(m)}*\mathsf{TC}_\Baire*\mathsf{lim}^{(m)}$. Notice that for every single-valued $k$ and every $g,h$ we have
	\begin{equation}\tag{$\star$}
		(g\times h)* k \le_{\mathrm{W}} (g* k) \times (h* k).
	\end{equation}
	This fails for multivalued $k$, as shown in \cite[Prop.\ 4.9(19)]{BP16}. We can therefore write
	\begin{align*}
		\mathsf{lim}^{(m)}*\mathsf{TC}_\Baire*\mathsf{lim}^{(m)} & \le_{\mathrm{W}} (\mathsf{sTC}_{\Baire}\times \mathsf{lim}^{[3m+6]})*\mathsf{lim}^{[m+1]} &  \text{\thref{thm:lim^n*tcbaire_<_lpo*tcbaire_x_lim^k}} \\
			& \le_{\mathrm{W}} (\mathsf{sTC}_{\Baire}*\mathsf{lim}^{[m+1]}) \times \mathsf{lim}^{[4m+7]} & (\star)\\
			& \le_{\mathrm{W}} ( \mathsf{LPO} *\mathsf{TC}_\Baire*\mathsf{lim}^{[m+1]}) \times \mathsf{lim}^{[4m+7]} & \\
			& \equiv_{\mathrm{W}} ( \mathsf{LPO} *(\mathsf{TC}_\Baire \times \mathsf{lim}^{[m+1]}))\times \mathsf{lim}^{[4m+7]} & \text{\thref{thm:tcbaire*lim=tcbaire_x_lim}} \\
			& \le_{\mathrm{W}} ( \mathsf{LPO} *\mathsf{lim}^{[m+1]}*\mathsf{TC}_\Baire) \times \mathsf{lim}^{[4m+7]} & \\
			& \le_{\mathrm{W}} (\mathsf{lim}^{[m+2]}*\mathsf{TC}_\Baire) \times \mathsf{lim}^{[4m+7]} &  \\
			& \le_{\mathrm{W}} \mathsf{sTC}_{\Baire} \times\mathsf{lim}^{[3m+9]}\times \mathsf{lim}^{[4m+7]}  &  \text{\thref{thm:lim^n*tcbaire_<_lpo*tcbaire_x_lim^k}} \\
			& \equiv_{\mathrm{W}} \mathsf{sTC}_{\Baire} \times\mathsf{lim}^{[n]}, &
	\end{align*}
	where $n=\max\{3m+9, 4m+7\}$.
\end{proof}

\begin{corollary}
	\thlabel{thm:tcbaire_arit_<_openRT}
	$\mathsf{TC}_\Baire<^a_\mathrm{W} \boldfaceSigma^0_1\mathsf{-RT}$.
\end{corollary}
\begin{proof}
	The reduction follows from $\mathsf{TC}_\Baire\le_{\mathrm{W}} \mathsf{C}_\Cantor* \boldfaceSigma^0_1\mathsf{-RT}$ (\thref{prop:tcbaire<=ccantor_comp_openRamsey}) using \thref{prop:ccantor_arith_equiv_id} and \thref{prop:compprod_arith_reduction}. The fact that the reduction is strict follows from \thref{thm:arith_reduction_tcbaire} as $\boldfaceSigma^0_1\mathsf{-RT}\not\le_{\mathrm{W}} \mathsf{sTC}_{\Baire} \times \mathsf{lim}^{(k)}$ for any $k$ (\thref{thm:openRT_not_<=_sTCbaire_x_lim^n}).
\end{proof}

\begin{theorem}
	\thlabel{thm:openRamsey_arith<_findHopen}
	$\boldfaceSigma^0_1\mathsf{-RT}<^a_\mathrm{W} \mathsf{FindHS}_{\boldfaceSigma^0_1} $.
\end{theorem}
\begin{proof}
It suffices to show that $\boldfaceSigma^0_1\mathsf{-RT}<^a_\mathrm{W} \mathsf{C}_\Baire\times \boldfaceSigma^0_1\mathsf{-RT}$, as $\mathsf{C}_\Baire\times \boldfaceSigma^0_1\mathsf{-RT} \le_{\mathrm{W}} \mathsf{FindHS}_{\boldfaceSigma^0_1} $ follows from $\boldfaceSigma^0_1\mathsf{-RT}\le_{\mathrm{W}} \mathsf{FindHS}_{\boldfaceSigma^0_1} $ (see \thref{thm:lim^n*openRT<=findHopen}), $\mathsf{C}_\Baire\le_{\mathrm{W}} \mathsf{FindHS}_{\boldfaceSigma^0_1} $ (see \thref{prop:tcbaire<=findHopen}) and the fact that $\mathsf{FindHS}_{\boldfaceSigma^0_1} $ is closed under parallel product (\thref{prop:findHopen_closed_product}).

The reduction is trivial, so we only need to prove the separation. Notice
that the analogue of \thref{prop:product_with_NHA_general} for arithmetic
Weihrauch reduction holds (the same proof works by replacing ``computable"
with ``arithmetic'' and $\le_{\mathrm{W}}$ with $\le^a_{\mathrm{W}}$). This allows us to repeat the proof of \thref{prop:product_with_NHA}, obtaining that $\mathsf{C}_\Baire \times \boldfaceSigma^0_1\mathsf{-RT} \le^a_{\mathrm{W}} \boldfaceSigma^0_1\mathsf{-RT}$ implies $\boldfaceSigma^0_1\mathsf{-RT}\le^a_{\mathrm{W}}\mathsf{C}_\Baire$. This contradicts \thref{thm:cbaire_arith<_tcbaire} and \thref{thm:tcbaire_arit_<_openRT}.
\end{proof}

\begin{theorem}
	$\boldfaceSigma^0_1\mathsf{-RT}^* \equiv^a_{\mathrm{W}} \mathsf{TC}_\Baire^*$.
\end{theorem}
\begin{proof}
	The right-to-left reduction is a trivial consequence of $\mathsf{TC}_\Baire<^a_\mathrm{W} \boldfaceSigma^0_1\mathsf{-RT}$ (\thref{thm:tcbaire_arit_<_openRT}).

	To prove the left-to-right reduction we first notice that
	\[ \boldfaceSigma^0_1\mathsf{-RT} \le_{\mathrm{W}} \mathsf{sTC}_{\Baire}\times \mathsf{TwFindHS}_{\boldfaceSigma^0_1} . \]
	Indeed, given an open set $P$ we can consider the input $([\closedsidesoltree{\coding{P}}],P)$ for $\mathsf{sTC}_{\Baire}\times \mathsf{TwFindHS}_{\boldfaceSigma^0_1} $. This is clearly a valid input as both functions are total. Let $(\coding{b}\raisebox{.9ex}{\ensuremath\smallfrown}  x,f)\in (\mathsf{sTC}_{\Baire}\times \mathsf{TwFindHS}_{\boldfaceSigma^0_1} )([\closedsidesoltree{\coding{P}}],P)$. If $b=1$ then $x\in \mathrm{HS}(P)\backslash{P}$ (\thref{lem:solution_closed_side_iff_path_through_tree}), and therefore $x\in\boldfaceSigma^0_1\mathsf{-RT}(P)$. If $b=0$ then $[\closedsidesoltree{\coding{P}}]=\emptyset$, which implies that $P\in\operatorname{dom}(\mathsf{wFindHS}_{\boldfaceSigma^0_1} )$ and hence $f\in\mathsf{wFindHS}_{\boldfaceSigma^0_1} (P)$.

	We then have
	\[ \boldfaceSigma^0_1\mathsf{-RT} \le_{\mathrm{W}} \mathsf{sTC}_{\Baire}\times \mathsf{TwFindHS}_{\boldfaceSigma^0_1}  \le_{\mathrm{W}} \mathsf{sTC}_{\Baire}\times \mathsf{C}_\Baire \le^a_{\mathrm{W}} \mathsf{TC}_\Baire\times \mathsf{TC}_\Baire, \]
	where $\mathsf{TwFindHS}_{\boldfaceSigma^0_1}  \le_{\mathrm{W}} \mathsf{C}_\Baire$ follows from $\mathsf{TwFindHS}_{\boldfaceSigma^0_1} \le_{\mathrm{W}} { \mathsf{ATR} }_2$ (\thref{thm:twfindopen<=atr2}). From this $\boldfaceSigma^0_1\mathsf{-RT}^*\le^a_{\mathrm{W}}\mathsf{TC}_\Baire^*$ follows immediately.
\end{proof}

\section{Conclusions}
\label{sec:conclusions}
Some problems resisted full characterization. In particular two questions remain open:

\begin{question}
	$\mathsf{wFindHS}_{\boldfacePi^0_1}\equiv_{\mathrm{W}} \mathsf{C}_\Baire$?
\end{question}
\begin{question}
	$\mathsf{C}_\Baire\le_{\mathrm{W}}\boldfaceSigma^0_1\mathsf{-RT}$?
\end{question}

Observe that a positive answer to the first question automatically yields a positive answer to the second one by \thref{cor:wfindHclosed<openRT}. We can expect that answering one of the two questions can shed light on the other.

As already observed in \cite{KMP20}, there is not a single ``analogue'' of $\mathrm{ATR}_0$ in the context of Weihrauch reducibility, and theorems that are equivalent from the reverse mathematics point of view can exhibit very different behaviors when phrased as multivalued functions.

Notice in particular that the classical proofs of the equivalences, over $\mathrm{RCA}_0$, of $\mathrm{ATR}_0$ and the open and clopen Ramsey theorems (\cite{Simpson09}) are useful only to establish that $\mathsf{UC}_\Baire\equiv_{\mathrm{W}} \mathsf{wFindHS}_{\boldfaceSigma^0_1}  \equiv_{\mathrm{W}} \mathsf{wFindHS}_{\boldfaceDelta^0_1}$.

Finding a homogeneous solution that lands in an open set, when there are also solutions that avoid it, is a much harder problem. In particular, notice that a natural candidate for $\boldsymbol{\Pi}^1_1\mathrm{-CA}_0$ in the Weihrauch lattice is $\parallelization{\chi_{\Pi^1_1}}$. The fact that $\mathsf{FindHS}_{\boldfaceSigma^0_1} $ computes $\chi_{\Pi^1_1}$ and is closed under parallel product implies that $\chi_{\Pi^1_1}^*\le_{\mathrm{W}} \mathsf{FindHS}_{\boldfaceSigma^0_1} $. This naturally leads to the following question:
\begin{question}
	$\parallelization{\mathsf{FindHS}_{\boldfaceSigma^0_1} }\le_{\mathrm{W}}\mathsf{FindHS}_{\boldfaceSigma^0_1} $?
\end{question}
A positive answer to this question would locate $\mathsf{FindHS}_{\boldfaceSigma^0_1} $ in the realm of $\boldsymbol{\Pi}^1_1\mathrm{-CA}_0$, in sharp contrast with what happens in reverse mathematics.

Let us now derive a few computability-theoretic corollaries.

\begin{corollary}[{Solovay's theorem \cite[Thm.\ 1.8]{Solovay78}}]
	\thlabel{thm:solovay} If $P\subset{[\mathbb{N}]}^\mathbb{N} $ is open with computable code then either there is an hyperarithmetic homogeneous solution
landing in $P$ or there is a homogeneous solution avoiding $P$.
\end{corollary}
\begin{proof}
This follows from \thref{thm:ucbaire_hyperarithmetic_solution} and the fact that $\mathsf{wFindHS}_{\boldfaceSigma^0_1} \equiv_{\mathrm{W}} \mathsf{UC}_\Baire$ (\thref{thm:open<ucbaire}).
\end{proof}

The following result is attributed to Solovay \cite{Solovay78} (see \cite[Thm.\ 1]{Mansfield78} for an explicit proof).
\begin{corollary}
	The set of homogeneous solutions for a clopen set with computable code always contains an hyperarithmetic element.
\end{corollary}
\begin{proof}
	This follows from \thref{thm:ucbaire_hyperarithmetic_solution} and the fact that $\boldfaceDelta^0_1\mathsf{-RT}\equiv_{\mathrm{W}}\mathsf{UC}_\Baire$ (\thref{thm:ucbaire=clopenramsey}).
\end{proof}

\begin{corollary}
	There is a clopen set $D\subset{[\mathbb{N}]}^\mathbb{N} $ with computable code s.t.\ every homogeneous solution that lands in $D$ is not hyperarithmetic.
\end{corollary}
\begin{proof}
	This follows from the fact that $\mathsf{FindHS}_{\boldfaceDelta^0_1}\equiv_{\mathrm{W}}\mathsf{C}_\Baire$ (\thref{thm:findclopen=findclosed=cbaire}): if every computable clopen set had an hyperarithmetic solution landing in itself then every computable instance of $\mathsf{C}_\Baire$ would have a hyperarithmetic solution, contradicting $ \mathsf{NHA} \le_{\mathrm{W}}\mathsf{C}_\Baire$ (\cite[Cor.\ 3.6]{KMP20}).
\end{proof}

\begin{corollary}
	\thlabel{cor:complexity_of_solutions}
	Every open set $P\subset{[\mathbb{N}]}^\mathbb{N} $ with computable code has a homogeneous solution $f$ that is strictly Turing reducible to Kleene's ${\mathcal{O}}$.
\end{corollary}
\begin{proof}
	It follows from the proof of Gandy basis theorem (see \cite[Chap.\ III, Thm.\ 1.4]{SacksHRT}) that $\{f: f<_T {\mathcal{O}}\}$ is a basis for the $\Sigma^1_1$ predicates. If $P\in\operatorname{dom}(\mathsf{wFindHS}_{\boldfaceSigma^0_1} )$ then, by \thref{thm:solovay}, it has an hyperarithmetic solution. Otherwise $P\in\operatorname{dom}(\mathsf{FindHS}_{\boldfacePi^0_1})$ hence, by \thref{lem:solution_closed_side_iff_path_through_tree}, a homogeneous solution for $P$ can be computed from any element of $[\closedsidesoltree{\coding{P}}]$ (the tree $\closedsidesoltree{\coding{P}}$ is computable from $\coding{P}$, see \thref{lem:computable_operations}). By the Gandy basis theorem the claim follows.
\end{proof}
In particular \thref{cor:complexity_of_solutions} shows that the difference, in the (arithmetic) Weihrauch lattice, between $\boldfaceSigma^0_1\mathsf{-RT}$ and $\mathsf{C}_\Baire$ cannot be explained in terms of complexity of the solutions but rests entirely on the lack of uniformity.

\let\oldaddcontentsline\addcontentslin
\renewcommand{\addcontentsline}[3]{
\bibliographystyle{mbibstyle}

redpajama_set_name: RedPajamaArXiv