Clopen Cylinder Domain

Clopen cylinder = local Hartogs bulk restricted to a primorial level. The cylinder algebra is Boolean (intersection, union, complement all clopen). Domain building blocks for τ-admissible fluid data.

Clopen Cylinder Domain

Summary

Clopen cylinder = local Hartogs bulk restricted to a primorial level. The cylinder algebra is Boolean (intersection, union, complement all clopen). Domain building blocks for τ-admissible fluid data.

Statement

\label{def:clopen-cylinder-domain}
A \emph{clopen cylinder} in $\tau^3$ at primorial depth $k$ is a set of the form
\begin{equation}
C_{k,S} \;=\; \bigl\{\, x \in \tau^3_{\le k} \;\big|\; x \bmod p_i \in S_i \text{ for each } 1 \le i \le k \,\bigr\},
\label{eq:ch34-clopen-cylinder}
\end{equation}
where $S = (S_1, \ldots, S_k)$ is a $k$-tuple with each $S_i \subseteq \Z / p_i\Z$ non-empty. The restriction is to the local Hartogs bulk (III.D01) at level $\mathrm{Prim}(k)$: each $C_{k,S}$ is a simultaneous residue class condition on all primes up to $p_k$.

Proof / Justification

This item is definitional. No manuscript proof is required.

Source Context

• Registry source: book-03.jsonl line 89
• Manuscript source: 2nd-edition/book-iii-categorical-spectrum/02_mainmatter/part05/ch34-tau-admissible-fluid-data.tex lines 121-129

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookIII.Physics.FluidData
• Name: cylinder_assignment_check

Dependencies

• Canonical: III.D01, III.T09

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.