%
\label{lem:no-tie}
Let $\underline{A} \in \mathbb{P}_\tau$
and $X \in \tau\text{-Idx}$ with $\underline{A} \mid X$.
\begin{enumerate}
    \item The set
          $\{\underline{c} \geq \underline{1} :
          \underline{A} \uparrow\uparrow \underline{c} \mid X\}$
          has a well-defined maximum $\underline{C}$.
    \item If
          $T(\underline{A}, \underline{b_1}, \underline{c_1})
          = T(\underline{A}, \underline{b_2}, \underline{c_2})$
          with $\underline{b_1}, \underline{b_2} \geq \underline{1}$
          and $\underline{c_1}, \underline{c_2} \geq \underline{1}$,
          then $\underline{c_1} = \underline{c_2}$
          and $\underline{b_1} = \underline{b_2}$.
\end{enumerate}

\emph{Part~(1).}
The tetration $\underline{A} \uparrow\uparrow \underline{c}$
is strictly monotone in $\underline{c}$
for $\underline{A} \geq \underline{2}$
(Proposition~\ref{prop:tetration-injective}).
In particular,
$\underline{A} \uparrow\uparrow (\underline{c}+\underline{1})
> \underline{A} \uparrow\uparrow \underline{c}$
for all $\underline{c} \geq \underline{1}$.
Since $\underline{A} \uparrow\uparrow \underline{c}$
grows without bound and $X$ is fixed,
there exists a largest $\underline{c}$ with
$\underline{A} \uparrow\uparrow \underline{c} \leq X$.
Beyond this bound,
$\underline{A} \uparrow\uparrow \underline{c} > X$,
so divisibility fails.
The maximum of the finite set of valid $\underline{c}$
is well-defined by the well-ordering of $\tau$-Idx
(Proposition~\ref{prop:well-ordering}).

\emph{Part~(2).}
Suppose
$(\underline{A} \uparrow\uparrow \underline{c_1})^{\underline{b_1}}
= (\underline{A} \uparrow\uparrow \underline{c_2})^{\underline{b_2}}$.

Both sides have $\underline{A}$ as their only prime factor
(since $\underline{A}$ is prime and tetration
$\underline{A} \uparrow\uparrow \underline{c}$
is a power of $\underline{A}$).

Let $v_1$ be the $\underline{A}$-adic valuation of the left side
and $v_2$ that of the right side.
Then:
\begin{align*}
    v_1 &= \underline{b_1} \cdot
    v_{\underline{A}}(\underline{A} \uparrow\uparrow \underline{c_1}), \\
    v_2 &= \underline{b_2} \cdot
    v_{\underline{A}}(\underline{A} \uparrow\uparrow \underline{c_2}).
\end{align*}

The $\underline{A}$-adic valuation of
$\underline{A} \uparrow\uparrow \underline{c}$ is:
\[
    v_{\underline{A}}(\underline{A} \uparrow\uparrow \underline{c})
    = \underline{A} \uparrow\uparrow (\underline{c} - \underline{1})
\]
(since $\underline{A} \uparrow\uparrow \underline{c}
= \underline{A}^{\underline{A} \uparrow\uparrow (\underline{c}-\underline{1})}$
by the recursive definition of tetration).

So equality gives:
$\underline{b_1} \cdot
(\underline{A} \uparrow\uparrow (\underline{c_1} - \underline{1}))
= \underline{b_2} \cdot
(\underline{A} \uparrow\uparrow (\underline{c_2} - \underline{1}))$.

If $\underline{c_1} \neq \underline{c_2}$,
say $\underline{c_1} < \underline{c_2}$,
then
$\underline{A} \uparrow\uparrow (\underline{c_2} - \underline{1})
\geq \underline{A} \uparrow\uparrow \underline{c_1}
= \underline{A}^{\underline{A} \uparrow\uparrow (\underline{c_1} - \underline{1})}
> \underline{A} \cdot
(\underline{A} \uparrow\uparrow (\underline{c_1} - \underline{1}))$
for $\underline{A} \geq \underline{2}$.
This forces
$\underline{b_2} < \underline{b_1} / \underline{A}
< \underline{b_1}$,
but the same argument with the growth rate
of tetration shows that $\underline{b_2}$
would need to compensate for the
super-exponential gap between
$\underline{A} \uparrow\uparrow (\underline{c_2} - \underline{1})$
and $\underline{A} \uparrow\uparrow (\underline{c_1} - \underline{1})$,
which is impossible for finite $\underline{b_1}$.

More precisely: if $\underline{c_2} = \underline{c_1} + \underline{1}$,
then the right factor is
$\underline{A}^{\underline{A} \uparrow\uparrow (\underline{c_1}-1)}$
times larger than the left factor,
while $\underline{b_1}$ is at most polynomially larger
than $\underline{b_2}$.
For $\underline{c_2} > \underline{c_1} + \underline{1}$,
the gap is even more extreme.
In all cases, equality is impossible.

Therefore $\underline{c_1} = \underline{c_2}$,
and then
$\underline{b_1} \cdot
(\underline{A} \uparrow\uparrow (\underline{c_1}-\underline{1}))
= \underline{b_2} \cdot
(\underline{A} \uparrow\uparrow (\underline{c_1}-\underline{1}))$
gives $\underline{b_1} = \underline{b_2}$
by cancellation.