%
\label{prop:orbit-disjoint}
The five canonical sets
\[
    \{\omega\}, \quad O_\alpha, \quad O_\pi,
    \quad O_\gamma, \quad O_\eta
\]
are pairwise disjoint.

We must show ten pairwise disjointness claims.
We organize them into three groups.

\medskip
\textbf{Group 1: $\{\omega\}$ is disjoint from each orbit ray.}

Let $g \in \{\alpha, \pi, \gamma, \eta\}$.
Suppose $\omega \in O_g$, i.e., $\omega = \rho^n(g)$ for some $n \geq 0$.
If $n = 0$, then $\omega = g$, contradicting
the generator distinctness (Proposition~\ref{prop:gen-distinct}).
If $n \geq 1$, then $\rho^n(g) = \omega$,
contradicting $\KAxiom{5}$ (Beacon Non-Successor).
Hence $\{\omega\} \cap O_g = \emptyset$ for each $g \neq \omega$.

\medskip
\textbf{Group 2: Orbit rays with different seeds are disjoint.}

Let $g, h \in \{\alpha, \pi, \gamma, \eta\}$ with $g \neq h$.
Suppose $x \in O_g \cap O_h$,
so $x = \rho^n(g) = \rho^m(h)$ for some $n, m \geq 0$.

\emph{Case $n = m = 0$:}
Then $g = h$, contradicting $g \neq h$.

\emph{Case $n = 0$, $m \geq 1$:}
Then $g = \rho^m(h)$.
Since $g$ is a generator and $\rho^m(h)$ with $m \geq 1$
is a non-generator orbit element,
we need to show these cannot be equal.
By $\KAxiom{4}$, $\rho^m(h)$ has depth $m$ in $O_h$.
A generator has depth $0$ in its own orbit.
For $\rho^m(h)$ to equal a generator $g$ with $g \neq h$,
$\rho$ would have to map an $h$-seeded element to a $g$-seeded element,
but $\KAxiom{3}$ asserts $\rho(O_h) \subseteq O_h$:
the ray is closed under $\rho$.
Since $g \notin O_h$ (because $g$ has depth~$0$
and seed $g \neq h$), this is a contradiction.

\emph{Case $n \geq 1$, $m = 0$:}
Symmetric to the previous case.

\emph{Case $n \geq 1$, $m \geq 1$:}
Then $\rho^n(g) = \rho^m(h)$.
But $\rho^n(g)$ is an element of $O_g$
(by $\KAxiom{3}$: $\rho$ maps $O_g$ into $O_g$),
and $\rho^m(h)$ is an element of $O_h$.
By the same closure argument,
an element of $O_g$ cannot equal an element of $O_h$
unless the two rays overlap.
Since the Lean formalization
represents each object by its seed and depth,
two objects with different seeds are definitionally different.
In the axiomatic development,
we reason as follows:
$\rho^n(g)$ has seed $g$ (it was generated from $g$ by $n$ applications of $\rho$,
each of which preserves the seed by $\KAxiom{3}$),
and $\rho^m(h)$ has seed $h$.
Since $g \neq h$, the objects are distinct.

\medskip
\textbf{Group 3: Summary.}
All ten pairs are covered by Groups~1 and~2.