%
\label{thm:fta-tau-idx}
Every $\underline{n} \geq \underline{2}$ in $\tau$-Idx
has a unique representation as a product of primes:
\[
    \boxed{\underline{n}
    = \underline{p_1}^{\underline{e_1}}
    \times \underline{p_2}^{\underline{e_2}}
    \times \cdots
    \times \underline{p_k}^{\underline{e_k}}}
\]
where $\underline{p_1} < \underline{p_2} < \cdots
< \underline{p_k}$ are primes
and each $\underline{e_i} \geq \underline{1}$.
The representation is unique up to reordering
(and we fix ascending order by convention).

\emph{Existence.}
By strong induction on $\underline{n}$.
If $\underline{n}$ is prime, the factorization is
$\underline{n}$ itself.
If not, $\underline{n} = \underline{a} \times \underline{b}$
with $\underline{2} \leq \underline{a}, \underline{b}
< \underline{n}$.
By induction, both $\underline{a}$ and $\underline{b}$
have prime factorizations;
their product gives a factorization of $\underline{n}$.

\emph{Uniqueness.}
Suppose $\underline{n} = \underline{p_1}^{\underline{e_1}}
\times \cdots \times \underline{p_k}^{\underline{e_k}}
= \underline{q_1}^{\underline{f_1}}
\times \cdots \times \underline{q_l}^{\underline{f_l}}$.
Since $\underline{p_1} \mid \underline{n}$,
we have $\underline{p_1} \mid
\underline{q_j}^{\underline{f_j}}$ for some $j$
(by Euclid's Lemma, which holds on $\tau$-Idx
because the cancellation law holds in the semiring).
Since $\underline{q_j}$ is prime, $\underline{p_1}
= \underline{q_j}$.
By induction on the total number of prime factors,
the remaining factors agree.