$\let\T\mathrm\def\kr{\mathrel{\mathbf r}}$This is a follow up to Kleene realizability in Peano arithmetic.
We can summarize the results from Emil Jeřábek's answer as follows:
\begin{gather*}
T_1 = \{ \phi : \exists n. \T{PA} \vdash \overline n \kr \phi \} = \T{HA}+\T{ECT}_0+\T{MP} \\
T_3 = \{ \phi : \T{PA} \vdash \exists n. n \kr \phi \} = \T{HA}+\T{ECT}_0+\T{MP}+\T{SLEM}
\end{gather*}
where $\T{SLEM}$ is excluded middle for sentences.
My question is about finding a third theory, one for which PA can find a bound on the realizer (but not necessarily the exact value).
$$T_2 = \{ \phi : \exists k. \T{PA} \vdash \exists n < \overline k. n \kr \phi \} = \T{?}$$
Clearly we have $T_1 \subseteq T_2 \subseteq T_3$. We can also show that they are distinct.
$T_2$ proves excluded middle for all negated sentences, but $T_1$ does not. In particular, $T_2 \vdash \lnot \operatorname{Con}(\T{PA}) \lor \lnot \lnot \operatorname{Con}(\T{PA})$.
For any numeral $n$, $T_3$ can prove that the $n$th busy beaver number $\operatorname{BB}(n)$ exists because $\T{PA}$ proves it exists and knows how to turn it into a realizer (a different realizer for each $n$). $T_2$ is unable to prove this when $n$ is sufficiently large (say, 8000 or more) because for any numeral $k$, PA can't prove that $\operatorname{BB}(n) < k$.
So, what is $T_2$?
Best Answer
$\let\T\mathrm\def\kr{\mathrel{\mathbf r}}\let\LOR\bigvee$The same argument as in my linked answer shows that $$T_2=\T{HA+ECT_0+MP+SWLEM},$$ where $$\T{SWLEM}=\{\neg\phi\lor\neg\neg\phi:\text{$\phi$ sentence}\}.$$ You already observed that $T_2$ includes $T_1+\T{SWLEM}$.
On the other hand, assume $\T{PA}\vdash\exists x\le\overline n\,x\kr\phi$, and let $\psi(x)$ be a negative formula equivalent to $x\kr\phi$ in $\T{HA+MP}$. Then $\T{PA}\vdash\LOR_{m\le n}\psi(\overline m)$, thus $\T{HA}$ proves its double negation translation, which is equivalent to $\neg\neg\LOR_{m\le n}\psi(\overline m)$ as $\psi$ is negative. Consequently, $\T{HA+SWLEM}\vdash\LOR_{m\le n}\neg\neg\psi(\overline m)$, i.e., $\LOR_{m\le n}\psi(\overline m)$, using negativity again, thus $\T{HA+SWLEM+MA}\vdash\LOR_{m\le n}\overline m\kr\phi$, and $\T{HA+SWLEM+MA+ECT_0}\vdash\phi$.