Hausdorff Property

tau^3 is Hausdorff: any two distinct points are separated by disjoint cylinder neighborhoods at the first disagreement depth.

Hausdorff Property

Summary

tau^3 is Hausdorff: any two distinct points are separated by disjoint cylinder neighborhoods at the first disagreement depth.

Statement

%
\label{thm:hausdorff}
The topological space $\tau^3$ is Hausdorff:
for any two distinct points $x, y \in \tau^3$,
there exist disjoint open sets $U \ni x$ and $V \ni y$.

Proof / Justification

Let $x \neq y$.
The ultrametric distance satisfies
$d(x,y) > 0$
(Definition~\ref{def:ultrametric-distance},
identity of indiscernibles).
Let $\delta(x,y) = k < \infty$
be the first disagreement depth
(Definition~\ref{def:first-disagreement-depth}).
Then $\pi_{k+1}(x) \neq \pi_{k+1}(y)$,
so the stage-$(k{+}1)$ cylinders
$C_{k+1}(x)$ and $C_{k+1}(y)$ are disjoint:
they are distinct elements of the partition
$\{C_{k+1}(r) : r \in \mathbb{Z}/P_{k+1}\mathbb{Z}\}$.

Set $U = C_{k+1}(x)$ and $V = C_{k+1}(y)$.
Both are open (they are basis elements),
$x \in U$, $y \in V$,
and $U \cap V = \varnothing$.

Source Context

• Registry source: book-02.jsonl line 32
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part03/ch13-stone-space.tex lines 303-309

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.Topology.StoneSpace
• Name: hausdorff_check

Dependencies

• Canonical: II.D13, II.T05

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.