Stage-k Cylinder

The set C_k(x) of all points agreeing with x modulo the k-th primorial P_k. Equivalently, the preimage of the stage-k reduction map at x.

Stage-k Cylinder

Summary

The set C_k(x) of all points agreeing with x modulo the k-th primorial P_k. Equivalently, the preimage of the stage-k reduction map at x.

Statement

%
\label{def:stage-k-cylinder}
Let $x \in \tau^3$ and let $k \geq 1$.
The \textbf{stage-$k$ cylinder} at~$x$ is
\[
    \boxed{C_k(x)
    \;:=\;
    \bigl\{\, y \in \tau^3
    \;\big|\;
    \pi_k(y) = \pi_k(x)
    \,\bigr\}
    \;=\;
    \pi_k^{-1}\!\bigl(\pi_k(x)\bigr).}
\]
Equivalently:
$y \in C_k(x)$ if and only if $y \equiv x \pmod{P_k}$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-02.jsonl line 20
• Manuscript source: 2nd-edition/book-ii-categorical-holomorphy/02_mainmatter/part02/ch09-cylinder-domains.tex lines 114-131

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookII.Domains.Cylinders
• Name: CylinderDomain

Dependencies

• Canonical: I.T18, II.D02

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.