[proofplan] We construct a realizer for the implication by taking a realizer $a$ of the premise and extracting from it a total computable choice procedure. For each input $n$, the computation $\varphi_a(n)$ realizes $\exists m\,A(n,m)$, so its first projection is a witness $m$ and its second projection realizes $A(n,m)$. Using the $s$-$m$-$n$ theorem, we uniformly obtain an index $e$ for the partial computable function that computes this witness $m$ from $n$. We then build the realizer of the consequent by packaging $e$, and for each $n$ packaging a computation code $c$ for $\varphi_e(n)$ together with the inherited realizer of $A(n,U(c))$. [/proofplan]

[step:Fix the realizability conventions used in the construction] We use the standard clauses of Kleene realizability. For implication, an integer $r$ realizes $B\to C$ if, whenever $b\Vdash B$, the computation $\varphi_r(b)$ is defined and $\varphi_r(b)\Vdash C$. For universal quantification, $r\Vdash \forall n\,B(n)$ means that $\varphi_r(n)$ is defined and $\varphi_r(n)\Vdash B(n)$ for every $n\in\mathbb{N}$. For existential quantification, $r\Vdash \exists n\,B(n)$ means that $\pi_1(r)\Vdash B(\pi_0(r))$. For conjunction, $r\Vdash B\land C$ means that $\pi_0(r)\Vdash B$ and $\pi_1(r)\Vdash C$. For atomic formulas, we use the usual convention that every number realizes a true atomic formula and no number realizes a false atomic formula. In particular, once $T(e,n,c)$ is true, the fixed numeral $0$ realizes $T(e,n,c)$. We also use the substitution invariance of realizability under equality of numerals: if $r\Vdash A(n,m)$ and $m=k$ as natural numbers, then $r\Vdash A(n,k)$. This is proved by induction on the structure of the arithmetic formula $A$, using the atomic equality and relation clauses at the base case and the defining clauses for the logical connectives and quantifiers at the inductive steps. [/step]

[step:Extract witnesses from a realizer of the premise]Let $a\in\mathbb{N}$ be arbitrary, and assume \begin{align*} a\Vdash \forall n\,\exists m\,A(n,m). \end{align*} By the universal clause, for every $n\in\mathbb{N}$ the computation $\varphi_a(n)$ is defined and \begin{align*} \varphi_a(n)\Vdash \exists m\,A(n,m). \end{align*} For each $n\in\mathbb{N}$, define \begin{align*} p_n := \varphi_a(n). \end{align*} By the existential clause applied to $p_n$, the natural number \begin{align*} m_n := \pi_0(p_n) \end{align*} is a witness, and \begin{align*} r_n := \pi_1(p_n) \end{align*} satisfies \begin{align*} r_n\Vdash A(n,m_n). \end{align*}[/step]

[guided]We start with an arbitrary possible realizer $a$ of the premise. The premise is \begin{align*} \forall n\,\exists m\,A(n,m). \end{align*} The universal realizability clause says more than pointwise truth: it says that $a$ is an algorithm which, on input $n$, returns a realizer of the existential statement $\exists m\,A(n,m)$. Thus, for every $n\in\mathbb{N}$, the computation $\varphi_a(n)$ halts and realizes that existential statement. Define $p_n:=\varphi_a(n)$. The existential realizability clause says that an existential realizer is a coded pair. Its first projection is the witness, and its second projection realizes the formula at that witness. Therefore we define \begin{align*} m_n := \pi_0(p_n) \end{align*} and \begin{align*} r_n := \pi_1(p_n). \end{align*} Then the clause for $\exists m\,A(n,m)$ gives \begin{align*} r_n\Vdash A(n,m_n). \end{align*} This is the key extraction step: the premise realizer does not merely assert that witnesses exist; it computes a witness $m_n$ and a realizer of $A(n,m_n)$ uniformly in $n$.[/guided]

[step:Uniformly construct the program index for the extracted choice function] Consider the partial computable transformation which, with parameter $a$, acts on input $n$ as follows: compute $\varphi_a(n)$, call the result $p$, and output $\pi_0(p)$. By the $s$-$m$-$n$ theorem for the fixed acceptable enumeration from the theorem statement, there is a total computable function \begin{align*} S:\mathbb{N}\to\mathbb{N} \end{align*} such that, for every $a,n\in\mathbb{N}$, \begin{align*} \varphi_{S(a)}(n) \simeq \pi_0(\varphi_a(n)), \end{align*} where $\simeq$ denotes equality of partial computations, including simultaneous divergence. Define \begin{align*} e := S(a). \end{align*} Since $\varphi_a(n)$ is defined for every $n$, the computation $\varphi_e(n)$ is defined for every $n$, and \begin{align*} \varphi_e(n)=m_n. \end{align*} [/step]

[step:Produce computation codes witnessing the arithmetized computation predicate] For each $n\in\mathbb{N}$, since $\varphi_e(n)$ halts with output $m_n$, the defining property of the Kleene computation predicate gives a natural number $c_n\in\mathbb{N}$ such that \begin{align*} T(e,n,c_n) \end{align*} is true and \begin{align*} U(c_n)=m_n. \end{align*} Moreover, by the effective computation coding assumed in the theorem statement, there is a partial computable function \begin{align*} K:\mathbb{N}\times\mathbb{N}\rightharpoonup\mathbb{N} \end{align*} which, on input $(e,n)$, simulates the computation of the program with index $e$ on input $n$ until it halts and then outputs a finite computation code for that halting computation. Define \begin{align*} C_a:\mathbb{N}\to\mathbb{N} \end{align*} by \begin{align*} C_a(n):=K(S(a),n). \end{align*} Since $a$ realizes the premise, $\varphi_{S(a)}(n)$ halts for every $n\in\mathbb{N}$, so $C_a$ is total and $C_a(n)=c_n$. [/step]

[step:Build the realizer for the inner existential statement]Fix $n\in\mathbb{N}$. Define \begin{align*} d_n := \langle 0,r_n\rangle. \end{align*} Since $T(e,n,c_n)$ is true, the atomic realizability convention gives \begin{align*} 0\Vdash T(e,n,c_n). \end{align*} Since $U(c_n)=m_n$ and $r_n\Vdash A(n,m_n)$, substitution invariance for realizability gives \begin{align*} r_n\Vdash A(n,U(c_n)). \end{align*} Therefore, by the conjunction clause, \begin{align*} d_n\Vdash T(e,n,c_n)\land A(n,U(c_n)). \end{align*} Now define \begin{align*} q_n := \langle c_n,d_n\rangle. \end{align*} By the existential clause, \begin{align*} q_n\Vdash \exists c\,\bigl(T(e,n,c)\land A(n,U(c))\bigr). \end{align*}[/step]

[guided]Fix $n\in\mathbb{N}$. From the preceding construction, define $p_n:=\varphi_a(n)$, define the extracted witness $m_n:=\pi_0(p_n)$, and define the accompanying realizer $r_n:=\pi_1(p_n)$. The existential realizability clause applied to $p_n\Vdash \exists m\,A(n,m)$ gives \begin{align*} r_n\Vdash A(n,m_n). \end{align*} Also define $c_n:=K(e,n)$, where $K:\mathbb{N}\times\mathbb{N}\rightharpoonup\mathbb{N}$ is the partial computable computation-code extractor from the theorem statement. Since $e=S(a)$ and $\varphi_e(n)=m_n$ halts, the defining property of $K$ gives that $T(e,n,c_n)$ is true and \begin{align*} U(c_n)=m_n. \end{align*} The target formula for this fixed $n$ is \begin{align*} \exists c\,\bigl(T(e,n,c)\land A(n,U(c))\bigr). \end{align*} To realize an existential statement, we must provide a coded pair whose first component is the witness $c$ and whose second component realizes the body at that witness. We choose the witness to be $c_n$. It remains to realize the conjunction \begin{align*} T(e,n,c_n)\land A(n,U(c_n)). \end{align*} For the first conjunct, $T(e,n,c_n)$ is a true atomic arithmetic formula by the definition of $c_n$ as a halting computation code. Under the standard atomic clause for Kleene realizability, the fixed number $0$ realizes every true atomic formula. Hence \begin{align*} 0\Vdash T(e,n,c_n). \end{align*} For the second conjunct, we have not directly extracted a realizer of $A(n,U(c_n))$; we extracted $r_n\Vdash A(n,m_n)$. The bridge is the equality $U(c_n)=m_n$, which is part of the defining property of the computation code. By substitution invariance of realizability under equal numerical values, the same realizer $r_n$ realizes the formula after replacing $m_n$ by the equal number $U(c_n)$: \begin{align*} r_n\Vdash A(n,U(c_n)). \end{align*} Now the conjunction clause says that the pair of these two realizers realizes the conjunction. Thus, with \begin{align*} d_n := \langle 0,r_n\rangle, \end{align*} we have \begin{align*} d_n\Vdash T(e,n,c_n)\land A(n,U(c_n)). \end{align*} Finally, pairing the witness $c_n$ with the conjunction realizer $d_n$ gives \begin{align*} q_n := \langle c_n,d_n\rangle, \end{align*} and the existential clause yields \begin{align*} q_n\Vdash \exists c\,\bigl(T(e,n,c)\land A(n,U(c))\bigr). \end{align*}[/guided]

[step:Package the construction into a realizer of the consequent] Define a partial computable two-variable procedure $P:\mathbb{N}\times\mathbb{N}\rightharpoonup\mathbb{N}$ as follows. On input $(a,n)$, first compute $p:=\varphi_a(n)$. If this computation halts, compute $r:=\pi_1(p)$ and compute the halting computation code $c:=K(S(a),n)$ for the computation of $\varphi_{S(a)}(n)$. Then output \begin{align*} \langle c,\langle 0,r\rangle\rangle. \end{align*} The procedure is partial computable uniformly in $(a,n)$ because $S$, the projections, pairing, and $K$ are computable or partial computable in the senses fixed in the theorem statement. When $a\Vdash \forall n\,\exists m\,A(n,m)$, the computation $\varphi_a(n)$ halts for every $n\in\mathbb{N}$, and the construction of $S(a)$ gives that $\varphi_{S(a)}(n)$ halts for every $n\in\mathbb{N}$. Hence $P(a,n)$ is defined for every $n$, and its value is exactly $q_n$. By the $s$-$m$-$n$ theorem for the fixed acceptable enumeration again, there is a total computable function \begin{align*} R:\mathbb{N}\to\mathbb{N} \end{align*} such that $\varphi_{R(a)}(n)=q_n$ for every $n\in\mathbb{N}$. Therefore, by the universal clause, \begin{align*} R(a)\Vdash \forall n\,\exists c\,\bigl(T(e,n,c)\land A(n,U(c))\bigr). \end{align*} With $e=S(a)$, the existential clause gives \begin{align*} \langle e,R(a)\rangle\Vdash \exists e\,\forall n\,\exists c\,\bigl(T(e,n,c)\land A(n,U(c))\bigr). \end{align*} [/step]

[step:Abstract over the premise realizer to realize the implication] The construction of the pair \begin{align*} \langle S(a),R(a)\rangle \end{align*} is computable uniformly from $a$. Hence there is an index $h\in\mathbb{N}$ such that, for every $a\in\mathbb{N}$, \begin{align*} \varphi_h(a)=\langle S(a),R(a)\rangle. \end{align*} We have proved that whenever \begin{align*} a\Vdash \forall n\,\exists m\,A(n,m), \end{align*} the value $\varphi_h(a)$ realizes \begin{align*} \exists e\,\forall n\,\exists c\,\bigl(T(e,n,c)\land A(n,U(c))\bigr). \end{align*} By the implication clause, this means \begin{align*} h\Vdash \bigl(\forall n\,\exists m\,A(n,m)\bigr)\to \exists e\,\forall n\,\exists c\,\bigl(T(e,n,c)\land A(n,U(c))\bigr). \end{align*} Thus the Church's Thesis schema instance for $A(n,m)$ is realized. [/step]