%
\label{lem:remainder-descent}
Let $X \geq \underline{2}$ with ABCD encoding
$X = T(\underline{A}, \underline{B}, \underline{C})
\cdot \underline{D}$.
Then:
\begin{enumerate}
    \item $T(\underline{A}, \underline{B}, \underline{C})
          \geq \underline{2}$.
    \item $\underline{D} \leq X / \underline{2} < X$.
    \item If $\underline{D} > \underline{1}$,
          the largest prime dividing $\underline{D}$
          is strictly less than $\underline{A}$.
\end{enumerate}

\emph{Part~(1).}
$\underline{A} \geq \underline{2}$ (since $\underline{A}$
is prime).
$\underline{A} \uparrow\uparrow \underline{1}
= \underline{A} \geq \underline{2}$.
For $\underline{C} \geq \underline{1}$,
$\underline{A} \uparrow\uparrow \underline{C}
\geq \underline{A} \geq \underline{2}$.
Since $\underline{B} \geq \underline{1}$,
$T(\underline{A}, \underline{B}, \underline{C})
= (\underline{A} \uparrow\uparrow \underline{C})^{\underline{B}}
\geq \underline{2}^{\underline{1}}
= \underline{2}$.

\emph{Part~(2).}
$X = T(\underline{A}, \underline{B}, \underline{C})
\cdot \underline{D}$
with $T(\underline{A}, \underline{B}, \underline{C})
\geq \underline{2}$.
Dividing both sides by
$T(\underline{A}, \underline{B}, \underline{C})$:
\[
    \underline{D}
    = \frac{X}{T(\underline{A}, \underline{B}, \underline{C})}
    \leq \frac{X}{\underline{2}}
    < X.
\]
The strict inequality $X / \underline{2} < X$
holds because $X \geq \underline{2} > \underline{0}$.

\emph{Part~(3).}
This is Proposition~\ref{prop:nf-properties}(4),
already proved in Chapter~\ref{ch:nf-encoding}:
the greedy peel extracts $\underline{A}$
as the largest prime dividing $X$,
and the tower atom accounts for all factors of
$\underline{A}$ at the extracted level.