%
\label{thm:cantor-inapplicable}
Within the internal logic of Category~$\tau$ ---
bounded powerset
(Definition~\ref{def:bounded-powerset}),
no comprehension
(Proposition~\ref{prop:no-comprehension}),
diagonal discipline
(Definition~\ref{def:diagonal-discipline}) ---
no form of Cantor's diagonal argument
can produce an object outside $\Obj(\tau)$
or establish $|\mathbb{R}_\tau| > |\mathbb{N}_\tau|$.

Cantor's diagonal argument proceeds in three steps:
\begin{enumerate}
    \item[(C1)] \textbf{Diagonal extraction.}
          Construct the function $d(n) := 1 - f(n)(n)$
          by extracting the $n$-th digit
          of the $n$-th listed real.
    \item[(C2)] \textbf{Anti-diagonal formation.}
          Form the set
          $\{x : x \neq f(n) \text{ for all } n\}$
          and observe that $d$ belongs to it.
    \item[(C3)] \textbf{Diagonal self-pairing.}
          Use the map $n \mapsto (n, f(n)(n))$
          to walk the diagonal of $\mathbb{N} \times \mathbb{N}$.
\end{enumerate}

Each step requires infrastructure
that $\tau$ does not provide:

\medskip
\noindent\textbf{Step (C1) fails} by
Proposition~\ref{prop:no-unearned-decimal} (I.P34):
the diagonal digit-extraction
is not a total computable function
on the constructive reals $\mathbb{R}_\tau$.

\medskip
\noindent\textbf{Step (C2) fails} by
Proposition~\ref{prop:no-comprehension} (I.P35):
$\tau$ has no comprehension schema.
The anti-diagonal set cannot be formed
within $\tau$-set theory.

\medskip
\noindent\textbf{Step (C3) fails} by
Proposition~\ref{prop:no-free-cartesian} (I.P36):
the self-pairing map $\Delta \colon n \mapsto (n,n)$
is an unearned diagonal
that the diagonal discipline does not permit
as a generator of new objects.

\medskip
Since every step of the argument
requires at least one of the three
prohibited ingredients,
the argument cannot be executed within~$\tau$.
In particular, no object outside $\Obj(\tau)$
can be produced by the diagonal method,
and no cardinality inequality
$|\mathbb{R}_\tau| > |\mathbb{N}_\tau|$
can be derived.