Ultrametric Distance

Ultrametric Distance

Ultrametric Distance

Summary

Ultrametric Distance

Statement

%
\label{def:ultrametric-distance}
The \textbf{ultrametric distance} on~$\tau^3$
is the function $d : \tau^3 \times \tau^3 \to [0,1]$
defined by
\[
    \boxed{d(x, y)
    \;:=\;
    2^{-\delta(x,y)}}
\]
with the convention $2^{-\infty} = 0$.
Explicitly:
\begin{align}
    d(x, y) &= 0 &\quad&\text{if } x = y, \label{eq:ch10-d-zero}\\
    d(x, y) &= 2^{-k} &\quad&\text{if } \delta(x,y) = k < \infty.
    \label{eq:ch10-d-finite}
\end{align}
The distance takes values in the discrete set
$\{0\} \cup \{2^{-k} : k \geq 0\} = \{0, 1, \tfrac{1}{2}, \tfrac{1}{4}, \tfrac{1}{8}, \ldots\}$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-02.jsonl line 24
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part02/ch10-ultrametric-depth.tex lines 158-178

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.Domains.Ultrametric
• Name: ultra_dist

Dependencies

• Canonical: II.D12

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.