Alpha-Ray Line

A line in tau^3 along the alpha-ray direction, defined using the prime-indexed coordinate A and the ultrametric distance. The one-dimensional subspace traced by varying the address coordinate.

Alpha-Ray Line

Summary

A line in tau^3 along the alpha-ray direction, defined using the prime-indexed coordinate A and the ultrametric distance. The one-dimensional subspace traced by varying the address coordinate.

Statement

%
\label{def:alpha-ray}
The \textbf{$\alpha$-ray} is the subset of~$\tau^3$
defined by
\[
    \boxed{%
    \ell_\alpha
    \;:=\;
    \bigl\{\,\alpha_n : n \geq 1\,\bigr\}
    \;\cup\;
    \bigl\{\omega\bigr\},}
\]
where $\alpha_n := \pi_n(\alpha)$
is the stage-$n$ CRT reduction of~$\alpha$
(I.T18, Book~I),
and $\omega$ is the profinite limit point
(the coherent family exhausting all stages).

The \textbf{$\alpha$-ray metric} is the restriction
of the ultrametric distance
(Definition~\ref{def:ultrametric-distance}, II.D13):
\[
    d(\alpha_m, \alpha_n)
    \;=\;
    2^{-\min(m,n)}
    \quad\text{for } m \neq n,
    \qquad
    d(\alpha_n, \omega)
    \;=\;
    2^{-n}.
\]

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-02.jsonl line 60
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part05/ch23-lines-countable.tex lines 101-133

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.Transcendentals.Lines
• Name: alpha_ray

Dependencies

• Canonical: I.T04, I.D19, II.D13, II.D14

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.