Self-Containment Partition

Self-Containment Partition: X in Set(X) iff X in O_alpha union {omega}. The alpha-orbit and omega are ‘opaque’ (self-containing); the solenoidal orbits O_pi, O_gamma, O_eta are ‘transparent’ (non-self-containing organizing principles). Third position between ZFC (never reflexive) and divisibility (always reflexive).

Self-Containment Partition

Summary

Self-Containment Partition: X in Set(X) iff X in O_alpha union {omega}. The alpha-orbit and omega are ‘opaque’ (self-containing); the solenoidal orbits O_pi, O_gamma, O_eta are ‘transparent’ (non-self-containing organizing principles). Third position between ZFC (never reflexive) and divisibility (always reflexive).

Statement

%
\label{prop:self-containment}
A $\tau$-element $X$ belongs to its own set
if and only if $X$ lies in $O_\alpha \cup \{\omega\}$:
\[
    \boxed{%
    X \in \mathrm{Set}(X)
    \quad\iff\quad
    X \in O_\alpha \cup \{\omega\}.}
\]

Proof / Justification

We check each orbit.

\medskip
\noindent
\textbf{$\alpha$-orbit.}
$\mathrm{Set}(\alpha_n) = \{\alpha_k : k \mid n\}$.
Since $n \mid n$ (divisibility is reflexive),
$\alpha_n \in \mathrm{Set}(\alpha_n)$.

\medskip
\noindent
\textbf{Crossing point.}
$\mathrm{Set}(\omega) = O_\alpha \cup \{\omega\}$,
and $\omega \in \{\omega\} \subseteq \mathrm{Set}(\omega)$.

\medskip
\noindent
\textbf{$\pi$-orbit.}
$\mathrm{Set}(\pi_n) \subseteq O_\alpha$,
but $\pi_n \in O_\pi$.
Since $O_\alpha$ and $O_\pi$ are disjoint
(Proposition~\ref{prop:orbit-disjoint}),
$\pi_n \notin \mathrm{Set}(\pi_n)$.

\medskip
\noindent
\textbf{$\gamma$-orbit.}
$\mathrm{Set}(\gamma_n) \subseteq O_\alpha$,
but $\gamma_n \in O_\gamma$.
Orbit disjointness gives $\gamma_n \notin \mathrm{Set}(\gamma_n)$.

\medskip
\noindent
\textbf{$\eta$-orbit.}
$\mathrm{Set}(\eta_n) \subseteq O_\alpha$,
but $\eta_n \in O_\eta$.
Orbit disjointness gives $\eta_n \notin \mathrm{Set}(\eta_n)$.

Source Context

• Registry source: book-01.jsonl line 214
• Manuscript source: 2nd-edition/book-i-categorical-foundations/02_mainmatter/part08/ch83-orbit-set-correspondence.tex lines 377-388

Lean / Formalization Notes

• Formalization: formalized
• Module: TauLib.BookI.Sets.OrbitSets
• Name: Tau.Sets.self_containment_iff

Dependencies

• Canonical: I.D94, I.P03

Related Results

Generated by later projection phases.

Related Publications

Generated by later projection phases.

Revision Notes

• 2026-04-24: Initial pilot migration.