Solution (source code)

= Solution

This assertion is \b[always true]. <Ordinal addition> obeys $\alpha+\beta\geq\alpha$ and $\alpha+\beta\geq\beta$. Thus both summands are at most $\omega_1$. If $0<\beta<\omega_1$ and $\alpha<\omega_1$, both <ordinals> are <countable>, and their disjoint ordered union is <countable>, so their sum cannot be $\omega_1$. If instead $\alpha=\omega_1$ and $\beta>0$, appending a nonempty second block gives a sum strictly larger than $\omega_1$. These exhaust the possibilities with $0<\beta<\omega_1$; hence \b[$\beta=0$ or $\beta=\omega_1$].