Tau-Dimension

The minimal number of independent refinement rays whose joint cylinders separate all points of tau^3. Replaces classical covering dimension (which yields zero for profinite spaces).

Tau-Dimension

Summary

The minimal number of independent refinement rays whose joint cylinders separate all points of tau^3. Replaces classical covering dimension (which yields zero for profinite spaces).

Statement

%
\label{def:tau-dimension}
The \textbf{$\tau$-dimension} of~$\tau^3$ is
\[
\boxed{
\begin{aligned}
\dim_\tau \;:=\;
\min\bigl\{\, r \in \mathbb{N} \;\big|\;&
\text{there exist } r \text{ independent refinement rays} \\
&\text{whose joint cylinders separate all points}
\,\bigr\}.
\end{aligned}
}
\]
``Separate all points'': for any $x \neq y$ in~$\tau^3$,
there exists a stage~$k$ at which the joint constraint
along the selected rays distinguishes~$x$ from~$y$.
``Independent'': no ray's decomposition
is determined by the remaining $r - 1$ rays.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-02.jsonl line 36
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part03/ch15-dimension-four.tex lines 146-166

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.Topology.DimensionFour
• Name: tau_dim

Dependencies

• Canonical: II.D10, I.P08

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.