Registry · Definition I.D94 established formalized

I.D94 — Orbit-Set Map

Orbit-Set Map: assigns to every tau-element a structurally determined set via five families. Set(alpha_n) = {alpha_k : k | n} (divisor set = tau-membership); Set(pi_n) = first n primes; Set(gamma_n) = vertical prime tower; Set(eta_n) = horizontal prime sweep; Set(omega) = O_alpha union {omega}. The alpha-orbit case is exactly tau-membership (I.D31). All set-elements from O_alpha only (plus omega in Set(omega)).

Book I Part 8 Ch. 83

Dependency Graph

Depends on (6)

Depended on by (6)

Lean Formalization

Module: TauLib.BookI.Sets.OrbitSets

Symbol: Tau.Sets.orbit_set