%
\label{prop:refinement-resolution}
Let $x, y \in \tau^3$ be $\tau$-admissible points
with first disagreement depth
$\delta(x,y) = k$.
Then:
\begin{enumerate}
    \item[\textup{(i)}]
          \textbf{Ultrametric bound.}
          $d(x,y) = 2^{-k}$.

    \item[\textup{(ii)}]
          \textbf{Euclidean bound.}
          $d_{\mathrm{Euc}}\bigl(
          \mathrm{den}(x),\, \mathrm{den}(y)
          \bigr)
          \;\leq\;
          4 / P_k$,
          where $P_k = p_1 \cdots p_k$
          is the $k$th primorial.

    \item[\textup{(iii)}]
          \textbf{Conversion.}
          The ratio of the two bounds satisfies
          \[
              \frac{4/P_k}{2^{-k}}
              \;=\;
              \frac{4 \cdot 2^k}{P_k}
              \;\xrightarrow{k \to \infty}\;
              0,
          \]
          because $P_k$ grows super-exponentially
          \textup{(}$P_k = e^{(1+o(1))\, p_k}$
          by Chebyshev's estimates\textup{)}.
          The Euclidean bound is eventually
          much tighter than the ultrametric bound:
          Archimedean resolution ``catches up''
          to non-Archimedean refinement
          and eventually surpasses it.

    \item[\textup{(iv)}]
          \textbf{Asymptotic coupling.}
          For large~$k$, the effective conversion
          between ultrametric depth~$k$
          and Euclidean precision~$1/P_k$ is:
          \[
              -\log_2(1/P_k)
              \;=\;
              \log_2 P_k
              \;\sim\;
              \frac{p_k}{\ln 2}
              \;\sim\;
              \frac{k \ln k}{\ln 2},
          \]
          where the last step uses the prime number theorem
          $p_k \sim k \ln k$.
          The ultrametric depth~$k$
          translates to $\sim k \ln k / \ln 2$
          bits of Euclidean precision.
\end{enumerate}

\textbf{(i)}
By definition of the ultrametric
(II.D13, Chapter~\ref{ch:ultrametric-depth}).

\textbf{(ii)}
Proved in Chapter~\ref{ch:orthodox-bridge},
Proposition~\ref{prop:ch22-cauchy}:
each ABCD component contributes
at most $1/P_k$ to the Euclidean distance,
and there are four components.

\textbf{(iii)}
$P_k = \prod_{j=1}^k p_j$.
By the prime number theorem,
$\ln P_k = \sum_{j=1}^k \ln p_j = \vartheta(p_k) \sim p_k$,
so $P_k \sim e^{p_k}$.
Meanwhile $2^k$ grows exponentially in~$k$.
Since $p_k \sim k \ln k \gg k$,
$P_k$ grows super-exponentially in~$k$,
and $4 \cdot 2^k / P_k \to 0$.

\textbf{(iv)}
$\log_2 P_k = (\ln P_k)/(\ln 2) \sim p_k / \ln 2
\sim k \ln k / \ln 2$
by the prime number theorem.