%
\label{prop:no-unearned-decimal}
In the constructive framework of $\tau$,
the diagonal function
\[
    d(n) := \text{``$n$-th digit of $f(n)$''}
\]
is not a total computable function
on the space of programs-for-reals.
The diagonal construction requires
uniform decidability of digit extraction
across all computable Cauchy sequences,
which is not constructively available.

Suppose $f \colon \mathbb{N} \to \mathbb{R}_\tau$
is an enumeration of the computable reals,
where each $f(n)$ is given by a program $P_n$
that outputs a Cauchy sequence $(q_{n,k})_{k \geq 0}$
with explicit modulus of convergence $M_n$.
To extract the $n$-th binary digit of $f(n)$,
one must:
\begin{enumerate}
    \item Find an index $k_0$ such that
          $|q_{n,k_0} - f(n)| < 2^{-(n+2)}$
          (sufficient precision to determine bit~$n$).
    \item Read the $n$-th bit from the binary expansion
          of $q_{n,k_0}$.
\end{enumerate}
Step~(1) requires computing $M_n(n+2)$:
the modulus of convergence of the $n$-th program
at precision $n+2$.
But the function $n \mapsto M_n(n+2)$
is a diagonalization across all moduli ---
a function that uniformly evaluates
an arbitrary program-index on an arbitrary input.
By a standard argument
(the diagonal function of an effective enumeration
of total computable functions
is not itself in the enumeration),
this uniform extraction is not a total computable function.
Hence $d$ is not constructively definable
as an element of $\mathbb{R}_\tau$.