Registry · Proposition I.P41 established formalized

I.P41 — 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).

Book I Part 8 Ch. 83

Dependency Graph

Depends on (2)

Lean Formalization

Module: TauLib.BookI.Sets.OrbitSets

Symbol: Tau.Sets.self_containment_iff