Is the undecidable function $UC$ well-defined for proving the undecidability of Halting Problem?
In classical logic it is possible to define a function which is not computable, and $UC$ is such a function. What probably confuses you is that you think that a function must always be given in a symbolic form, or as a set of instructions on how to compute it, or some such. But this is not necessary. Officially a function $f : A \to B$ is the same thing as a subset $F \subseteq A \times B$ satisfying the functionality condition:


  For every $x \in A$ there is exactly one $y \in B$ such that $(x,y) \in F$.


We may apply this to our situation to define $UC$ as the set of pairs
$$UC = \lbrace
((\alpha, x), d) \mid
(\text{$M_\alpha$ halts on $x$ and $d = 1$})
\lor
(\text{$M_\alpha$ does not halt on $x$ and $d = 0$})
\rbrace.$$
Even though nobody told us how to discover the output $d$ for a given input $(a, x)$, it is still the case that for every $(a,x)$ there is exactly one $d$. Indeed, if there were more than one then we would have a machine $M_\alpha$ which both halts and does not halt on input $x$. And if there were no such $d$, that would mean we have a machine $M_\alpha$ which neither halts nor not halts on input $x$.

In constructive logic one cannot define a non-computable function. And neither can one show that all functions are computable. So there $UC$ would not satisfy the functionality condition, and it would only define a partial function. But we could still talk about the fact that the Hlating problem is not decidable because the same classical argument still applies (we just avoid talking about $UC$). Assume there is a Turing machine $H$ such that:


$H$ halts on every input.
If $M_\alpha$ halts on $x$ then $H$ on input $(\alpha, x)$ outputs $1$.
If $M_\alpha$ does not halt on $x$ then $H$ on input $(\alpha, x)$ outputs $0$.


We now proceed with the usual diagonalization argument and construct a machine $B$ with a code $\beta$ such that $B(\beta)$ halts if, and only if, $H(\beta, \beta)$ outputs $0$. Everything here is perfectly constructive. I only took care never to assume that every machine either halts or not (such an assumption is implicit in the definition of $UC$).

So perhaps you should stick to constructive mathematics, and there will be fewer surprises for you.