Is, the following function $h$ computable?
Let $h: \mathbb N \to \mathbb N $ be the function defined by:$$h(\ulcorner s \urcorner) = \ulcorner D(E_s(v)) \urcorner$$
for each sentence $s$ in the language of theory $T$, and $h(n)=0$ otherwise.
Where $E_s(v)$, called the extended sentence form of $s$, is the sentence form:
$\forall x \forall y \, (\operatorname {Proof}_T(x,v) \land [y= \min z: \operatorname {Proof}_T(z, \ulcorner s \urcorner)] \to x \geq y)$
and $D(E_s(v))$ is the diagonal formula of the sentence form $E_s(v)$, defined (along lines given here) by:
$\forall v (\mathcal G_f (^o\ulcorner \forall v (\mathcal G_f (k, v ) \to E_s(v)) \urcorner, v ) \to E_s(v))$
Where $f: \mathbb N \to \mathbb N$ is the function defined by: $$ f(\ulcorner \mathcal A \urcorner)= \, \ulcorner A(^o\ulcorner A \urcorner) \urcorner $$, for any sentence form $A$ in the language of $T$, and $f(n)=0$ otherwise.
This question is connected to this posting. So, the rationale is that if this is correct, then there would be a formula $\mathcal G_h(x,y)$ representing $h$ in theory $T$. Namely:
$\vdash_T \forall y \, (\mathcal G_h( ^o\ulcorner s \urcorner, y) \to y= \, ^o \ulcorner D(E_s(v)) \urcorner)$
and then we can define the sentence form $remote(x)$ as:
$\textbf{Define: } \\\begin{align} remote(x) \iff \exists y \exists z \exists u: \ & \mathcal G_h(x,y) \land \\& z=\min n: \operatorname {Proof}_T(n, x) \land \\& u=\min m : \operatorname {Proof}_T(m, y) \land \\& u < z \end{align}$
I personally think that $h$ is computable, but I'm not sure. The reason why I think it is, because it appears to me that there is an exact syntactical way of producing $D(E_s(v))$ from $s$, so there must be an algorithm capturing it. However, I'm not sure if the underpinnings of Gödel's numbering assignment of the syntax may be incompatible with that?