Level Circle

The finite cyclic group at NF stage k in each angular direction. The finite-stage circle whose inverse limit yields the solenoidal circle.

Level Circle

Summary

The finite cyclic group at NF stage k in each angular direction. The finite-stage circle whose inverse limit yields the solenoidal circle.

Statement

%
\label{def:level-circle}
For each stage $k \geq 1$
and each coordinate axis $X \in \{A, B, C\}$,
the \textbf{level-$k$ circle in the $X$-direction}
is the subset
\[
    \boxed{%
    \Lambda_k^X
    \;:=\;
    \bigl\{\,
    x \in \tau^3
    \;\big|\;
    D(x) = k,\;
    Y(x) \text{ and } Z(x) \text{ fixed}
    \,\bigr\},}
\]
where $\{X, Y, Z\} = \{A, B, C\}$
and the residue classes of~$Y$ and~$Z$ are held constant.
The level circle inherits the cyclic structure
of $\mathbb{Z}/p_k\mathbb{Z}$
(or more precisely, the CRT factor
$\mathbb{Z}/p_j\mathbb{Z}$
corresponding to the $X$-direction at stage~$k$).

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

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

Lean / Formalization Notes

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

Dependencies

• Canonical: II.D15, II.T11, I.T18

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.