%
\label{prop:dim-tau}
The dimension of the ABCD coordinate system is exactly $4$:
\begin{enumerate}
    \item \textbf{Sufficiency:}
          The four coordinates $(A, B, C, D)$
          suffice to encode every object in $\Obj(\tau)$.
    \item \textbf{Necessity:}
          No three of the four coordinates
          suffice to encode all objects.
\end{enumerate}

\emph{Sufficiency.}
This is the content of the NF existence theorem
(Proposition~\ref{prop:nf-existence}):
every object has an ABCD encoding.

\emph{Necessity.}
We show that omitting any single coordinate
causes information loss.

Omit $D$:
Objects $\underline{p}$ and $\underline{p} \cdot \underline{q}$
(for primes $\underline{p} > \underline{q}$)
share $(A, B, C) = (\underline{p}, \underline{1}, \underline{1})$
but have $D = \underline{1}$ and $D = \underline{q}$ respectively.
Without $D$, they are conflated.

Omit $A$:
Objects $\underline{2}$ and $\underline{3}$
share $(B, C, D) = (\underline{1}, \underline{1}, \underline{1})$
but have $A = \underline{2}$ and $A = \underline{3}$.
Without $A$, they are conflated.

Omit $B$:
Objects $\underline{p}$ and $\underline{p}^2$
(for any prime $\underline{p}$)
share $(A, C, D) = (\underline{p}, \underline{1}, \underline{1})$
but have $B = \underline{1}$ and $B = \underline{2}$.
Without $B$, they are conflated.

Omit $C$:
Objects $\underline{p}$ and
$\underline{p} \uparrow\uparrow \underline{2}
= \underline{p}^{\underline{p}}$
share the same prime $A = \underline{p}$
but have $C = \underline{1}$ and $C = \underline{2}$.
The exponent changes from $B = \underline{1}$
to $B = \underline{1}$
(with the tetration height carrying the new structure),
so $(A, B, D) = (\underline{p}, \underline{1}, \underline{1})$
for both.
Without $C$, they are conflated.