[proofplan]
We first isolate the leading term of any nonzero ordinal $\alpha<\varepsilon_0$: there is a unique exponent $\beta<\varepsilon_0$ such that
\begin{align*}
\omega^\beta\leq\alpha<\omega^{\beta+1},
\end{align*}
and then a unique positive integer $n$ such that
\begin{align*}
\omega^\beta n\leq\alpha<\omega^\beta(n+1).
\end{align*}
Subtracting this initial segment leaves a remainder strictly below $\omega^\beta$, so repeating the construction gives strictly decreasing exponents. The recursion must terminate because ordinals admit no infinite strictly descending sequence. Uniqueness follows by showing that the leading exponent and leading coefficient are determined by the interval bounds, then cancelling the common leading term and repeating on the remainder.
[/proofplan]
[step:Choose the leading exponent from the interval between consecutive powers of $\omega$]
Let $\alpha$ be a nonzero ordinal with $\alpha<\varepsilon_0$. Let $\operatorname{Ord}$ denote the class of all ordinals. Define
\begin{align*}
S_\alpha:=\{\gamma\in \operatorname{Ord}:\alpha<\omega^\gamma\}.
\end{align*}
Since $\varepsilon_0$ is a fixed point of $\gamma\mapsto\omega^\gamma$ and $\alpha<\varepsilon_0=\omega^{\varepsilon_0}$, the set $S_\alpha$ is nonempty. By well-ordering of the ordinals, $S_\alpha$ has a least element; denote it by $\delta$.
We claim that $\delta$ is a successor ordinal. It is not $0$, because $\omega^0=1\leq\alpha$ for every nonzero ordinal $\alpha$. If $\delta$ were a nonzero limit ordinal, then continuity of ordinal exponentiation in the exponent gives
\begin{align*}
\omega^\delta=\sup_{\gamma<\delta}\omega^\gamma.
\end{align*}
Since $\alpha<\omega^\delta$, there would be some $\gamma<\delta$ with $\alpha<\omega^\gamma$, contradicting the minimality of $\delta$. Hence $\delta=\beta+1$ for a unique ordinal $\beta$.
By minimality of $\delta=\beta+1$, we have $\alpha\not<\omega^\beta$, hence $\omega^\beta\leq\alpha$, while the definition of $\delta$ gives $\alpha<\omega^{\beta+1}$. Thus
\begin{align*}
\omega^\beta\leq\alpha<\omega^{\beta+1}.
\end{align*}
Moreover $\beta<\varepsilon_0$: if $\beta\geq\varepsilon_0$, then monotonicity of ordinal exponentiation gives
\begin{align*}
\omega^\beta\geq\omega^{\varepsilon_0}=\varepsilon_0,
\end{align*}
contradicting $\omega^\beta\leq\alpha<\varepsilon_0$.
[guided]
We need a canonical way to find the first exponent. The correct exponent is the unique $\beta$ for which $\alpha$ lies between $\omega^\beta$ and the next power $\omega^{\beta+1}$. To construct it, define
\begin{align*}
S_\alpha:=\{\gamma\in \operatorname{Ord}:\alpha<\omega^\gamma\}.
\end{align*}
This set is nonempty because $\alpha<\varepsilon_0$ and $\varepsilon_0$ is a fixed point:
\begin{align*}
\alpha<\varepsilon_0=\omega^{\varepsilon_0}.
\end{align*}
Therefore $\varepsilon_0\in S_\alpha$. Since ordinals are well-ordered, $S_\alpha$ has a least element; call it $\delta$.
The point is now to show that this least $\delta$ is exactly one step above the desired exponent. It cannot be $0$, since $\omega^0=1$ and $\alpha\neq 0$, so $1\leq\alpha$, which means $\alpha<\omega^0$ is false. It also cannot be a nonzero limit ordinal. Indeed, if $\delta$ were a nonzero limit ordinal, then ordinal exponentiation by base $\omega$ is continuous at $\delta$, so
\begin{align*}
\omega^\delta=\sup_{\gamma<\delta}\omega^\gamma.
\end{align*}
The inequality $\alpha<\omega^\delta$ would then place $\alpha$ below some earlier $\omega^\gamma$ with $\gamma<\delta$, contradicting the minimality of $\delta$ in $S_\alpha$.
Thus $\delta$ must be a successor ordinal. Write $\delta=\beta+1$. Since $\delta$ is the first exponent with $\alpha<\omega^\delta$, we have
\begin{align*}
\alpha<\omega^{\beta+1}.
\end{align*}
But $\beta<\delta$, so $\beta\notin S_\alpha$, which means $\alpha<\omega^\beta$ is false. Therefore
\begin{align*}
\omega^\beta\leq\alpha.
\end{align*}
Combining these gives the desired leading-exponent interval:
\begin{align*}
\omega^\beta\leq\alpha<\omega^{\beta+1}.
\end{align*}
Finally, the exponent $\beta$ itself lies below $\varepsilon_0$. If $\beta\geq\varepsilon_0$, monotonicity of $\gamma\mapsto\omega^\gamma$ gives
\begin{align*}
\omega^\beta\geq\omega^{\varepsilon_0}=\varepsilon_0,
\end{align*}
which contradicts $\omega^\beta\leq\alpha<\varepsilon_0$. Hence $\beta<\varepsilon_0$.
[/guided]
[/step]
[step:Choose the leading coefficient and produce a smaller remainder]
Fix the exponent $\beta<\varepsilon_0$ obtained above. Since
\begin{align*}
\omega^{\beta+1}=\omega^\beta\omega=\sup_{m\in\mathbb N}\omega^\beta m,
\end{align*}
and $\alpha<\omega^{\beta+1}$, not every positive integer $m$ satisfies $\omega^\beta m\leq\alpha$. Therefore the set
\begin{align*}
A_\alpha:=\{m\in\mathbb N:\omega^\beta m\leq\alpha\}
\end{align*}
is a nonempty finite initial segment of $\mathbb N$. Let $n:=\max A_\alpha$. Then $n\geq 1$ and
\begin{align*}
\omega^\beta n\leq\alpha<\omega^\beta(n+1).
\end{align*}
We use the following standard division property for ordinal addition: for fixed ordinals $\eta$ and $\alpha$ with $\eta\leq\alpha$, there is a unique ordinal $\rho$ such that $\alpha=\eta+\rho$; uniqueness follows because the map $\xi\mapsto\eta+\xi$ is strictly increasing. Applying this with $\eta:=\omega^\beta n$ gives a unique ordinal $\rho$ such that
\begin{align*}
\alpha=\omega^\beta n+\rho.
\end{align*}
The upper bound $\alpha<\omega^\beta(n+1)=\omega^\beta n+\omega^\beta$ and strict monotonicity of the map $\xi\mapsto\omega^\beta n+\xi$ imply
\begin{align*}
\rho<\omega^\beta.
\end{align*}
Thus the remainder after removing the leading block is strictly smaller than the leading power.
[guided]
Once the leading exponent $\beta$ is known, the next question is how many copies of $\omega^\beta$ fit into $\alpha$. Define
\begin{align*}
A_\alpha:=\{m\in\mathbb N:\omega^\beta m\leq\alpha\}.
\end{align*}
This set is nonempty because the previous step gave $\omega^\beta\leq\alpha$, so $1\in A_\alpha$.
It is also finite. The reason is that the limit of the increasing sequence
\begin{align*}
\omega^\beta,\quad \omega^\beta 2,\quad \omega^\beta 3,\quad \dots
\end{align*}
is
\begin{align*}
\sup_{m\in\mathbb N}\omega^\beta m=\omega^\beta\omega=\omega^{\beta+1}.
\end{align*}
But $\alpha<\omega^{\beta+1}$. If every $m\in\mathbb N$ belonged to $A_\alpha$, then $\omega^\beta m\leq\alpha$ for all $m$, so taking the supremum over $m$ would give
\begin{align*}
\omega^{\beta+1}=\sup_{m\in\mathbb N}\omega^\beta m\leq\alpha,
\end{align*}
contradicting $\alpha<\omega^{\beta+1}$. Therefore $A_\alpha$ has a largest element; call it $n$.
By definition of $n$, we have
\begin{align*}
\omega^\beta n\leq\alpha.
\end{align*}
By maximality of $n$, the next integer does not belong to $A_\alpha$, so
\begin{align*}
\alpha<\omega^\beta(n+1).
\end{align*}
Thus
\begin{align*}
\omega^\beta n\leq\alpha<\omega^\beta(n+1).
\end{align*}
Now remove the initial block $\omega^\beta n$. We use the standard division property for ordinal addition: if $\eta\leq\alpha$, then there is a unique ordinal $\rho$ with $\alpha=\eta+\rho$; uniqueness is a consequence of strict monotonicity of $\xi\mapsto\eta+\xi$. Applying this with $\eta:=\omega^\beta n$ gives a unique ordinal $\rho$ satisfying
\begin{align*}
\alpha=\omega^\beta n+\rho.
\end{align*}
The inequality
\begin{align*}
\alpha<\omega^\beta(n+1)=\omega^\beta n+\omega^\beta
\end{align*}
then becomes
\begin{align*}
\omega^\beta n+\rho<\omega^\beta n+\omega^\beta.
\end{align*}
Strict monotonicity of $\xi\mapsto\omega^\beta n+\xi$ gives
\begin{align*}
\rho<\omega^\beta.
\end{align*}
This is the key descent: the remainder is not merely smaller than $\alpha$; it is smaller than the entire leading scale $\omega^\beta$.
[/guided]
[/step]
[step:Iterate the leading term construction until the remainder vanishes]
Starting from $\rho_0:=\alpha$, apply the preceding two steps recursively while the current remainder is nonzero. Thus, whenever $\rho_{j-1}\neq 0$, choose the unique ordinal $\alpha_j<\varepsilon_0$, the unique positive integer $n_j\in\mathbb N$, and the unique ordinal $\rho_j$ such that
\begin{align*}
\rho_{j-1}=\omega^{\alpha_j}n_j+\rho_j
\end{align*}
and
\begin{align*}
\rho_j<\omega^{\alpha_j}\leq\rho_{j-1}.
\end{align*}
If $\rho_j\neq 0$, then applying the leading-exponent interval to $\rho_j$ gives
\begin{align*}
\omega^{\alpha_{j+1}}\leq\rho_j<\omega^{\alpha_j}.
\end{align*}
By monotonicity of $\gamma\mapsto\omega^\gamma$, this implies
\begin{align*}
\alpha_{j+1}<\alpha_j.
\end{align*}
Therefore the recursive construction produces a strictly decreasing sequence
\begin{align*}
\alpha_1>\alpha_2>\alpha_3>\cdots
\end{align*}
as long as it does not terminate. There is no infinite strictly descending sequence of ordinals, so the process terminates after finitely many steps. Hence there is some $k\in\mathbb N$ with $\rho_k=0$, and substituting the recursive identities gives
\begin{align*}
\alpha=\omega^{\alpha_1}n_1+\omega^{\alpha_2}n_2+\cdots+\omega^{\alpha_k}n_k,
\end{align*}
where $n_j>0$, $\alpha_j<\varepsilon_0$, and
\begin{align*}
\alpha_1>\alpha_2>\cdots>\alpha_k\geq 0.
\end{align*}
[guided]
We now repeat the leading-term extraction. Define the initial remainder by
\begin{align*}
\rho_0:=\alpha.
\end{align*}
If $\rho_0=0$, there would be nothing to prove, but the theorem assumes $\alpha\neq 0$. So the previous steps produce an exponent $\alpha_1<\varepsilon_0$, a positive integer $n_1$, and a remainder $\rho_1$ such that
\begin{align*}
\rho_0=\omega^{\alpha_1}n_1+\rho_1
\end{align*}
and
\begin{align*}
\rho_1<\omega^{\alpha_1}.
\end{align*}
If $\rho_1=0$, the process stops. If not, we apply the same construction to $\rho_1$. In general, whenever $\rho_{j-1}\neq 0$, we obtain $\alpha_j<\varepsilon_0$, $n_j\in\mathbb N$ with $n_j>0$, and an ordinal $\rho_j$ satisfying
\begin{align*}
\rho_{j-1}=\omega^{\alpha_j}n_j+\rho_j
\end{align*}
and
\begin{align*}
\rho_j<\omega^{\alpha_j}\leq\rho_{j-1}.
\end{align*}
The important point is that the exponents strictly decrease. If $\rho_j\neq 0$, then the next leading exponent $\alpha_{j+1}$ is chosen so that
\begin{align*}
\omega^{\alpha_{j+1}}\leq\rho_j.
\end{align*}
Together with $\rho_j<\omega^{\alpha_j}$, this gives
\begin{align*}
\omega^{\alpha_{j+1}}<\omega^{\alpha_j}.
\end{align*}
Since ordinal exponentiation by base $\omega$ is strictly increasing, we get
\begin{align*}
\alpha_{j+1}<\alpha_j.
\end{align*}
Thus, if the process never stopped, it would produce an infinite strictly descending sequence of ordinals:
\begin{align*}
\alpha_1>\alpha_2>\alpha_3>\cdots.
\end{align*}
Such a sequence cannot exist, because the ordinals are well-founded. Therefore the recursion stops after finitely many steps. Let $k\in\mathbb N$ be the first index with $\rho_k=0$. Substituting
\begin{align*}
\rho_{j-1}=\omega^{\alpha_j}n_j+\rho_j
\end{align*}
successively from $j=1$ to $j=k$ yields
\begin{align*}
\alpha=\omega^{\alpha_1}n_1+\omega^{\alpha_2}n_2+\cdots+\omega^{\alpha_k}n_k.
\end{align*}
The construction gives $n_j>0$ and $\alpha_j<\varepsilon_0$ for every $j$, and the descent just proved gives
\begin{align*}
\alpha_1>\alpha_2>\cdots>\alpha_k\geq 0.
\end{align*}
This proves existence.
[/guided]
[/step]
[step:Identify the leading exponent and coefficient from the ordinal itself]
Suppose
\begin{align*}
\alpha=\omega^{\beta_1}m_1+\omega^{\beta_2}m_2+\cdots+\omega^{\beta_\ell}m_\ell
\end{align*}
is any expression with $\ell\in\mathbb N$, positive integers $m_i$, and ordinals
\begin{align*}
\beta_1>\beta_2>\cdots>\beta_\ell\geq 0.
\end{align*}
If $\ell=1$, the tail after the first term is $0$. If $\ell>1$, define the tail ordinal
\begin{align*}
\tau:=\omega^{\beta_2}m_2+\cdots+\omega^{\beta_\ell}m_\ell.
\end{align*}
Since every exponent in $\tau$ is strictly below $\beta_1$, the additively indecomposable property of powers of $\omega$ gives
\begin{align*}
\tau<\omega^{\beta_1}.
\end{align*}
Indeed, if $\mu,\nu<\omega^{\beta_1}$, then $\mu+\nu<\omega^{\beta_1}$; applying this finitely to the summands of $\tau$ proves the displayed bound.
Therefore
\begin{align*}
\omega^{\beta_1}m_1\leq\alpha
\end{align*}
and
\begin{align*}
\alpha=\omega^{\beta_1}m_1+\tau<\omega^{\beta_1}m_1+\omega^{\beta_1}=\omega^{\beta_1}(m_1+1).
\end{align*}
In particular,
\begin{align*}
\omega^{\beta_1}\leq\alpha<\omega^{\beta_1+1}.
\end{align*}
Thus the leading exponent $\beta_1$ is exactly the unique ordinal $\beta$ satisfying
\begin{align*}
\omega^\beta\leq\alpha<\omega^{\beta+1},
\end{align*}
and the leading coefficient $m_1$ is exactly the unique positive integer $m$ satisfying
\begin{align*}
\omega^\beta m\leq\alpha<\omega^\beta(m+1).
\end{align*}
[guided]
To prove uniqueness, we first show that the first exponent and first coefficient are not choices: they are encoded in the ordinal $\alpha$.
Assume we are given some expression
\begin{align*}
\alpha=\omega^{\beta_1}m_1+\omega^{\beta_2}m_2+\cdots+\omega^{\beta_\ell}m_\ell,
\end{align*}
where $\ell\in\mathbb N$, each $m_i$ is a positive integer, and
\begin{align*}
\beta_1>\beta_2>\cdots>\beta_\ell\geq 0.
\end{align*}
Let $\tau$ denote the part after the first term. If $\ell=1$, set $\tau:=0$. If $\ell>1$, set
\begin{align*}
\tau:=\omega^{\beta_2}m_2+\cdots+\omega^{\beta_\ell}m_\ell.
\end{align*}
Because every exponent in $\tau$ is strictly smaller than $\beta_1$, the whole finite tail remains below the next leading unit:
\begin{align*}
\tau<\omega^{\beta_1}.
\end{align*}
This follows by finite induction on the length of the tail: each summand has leading exponent below $\beta_1$, and a finite sum of ordinals whose leading exponents are below $\beta_1$ is still below $\omega^{\beta_1}$.
Now rewrite $\alpha$ as
\begin{align*}
\alpha=\omega^{\beta_1}m_1+\tau.
\end{align*}
Since $\tau\geq 0$, we have
\begin{align*}
\omega^{\beta_1}m_1\leq\alpha.
\end{align*}
Since $\tau<\omega^{\beta_1}$, we also have
\begin{align*}
\alpha=\omega^{\beta_1}m_1+\tau<\omega^{\beta_1}m_1+\omega^{\beta_1}=\omega^{\beta_1}(m_1+1).
\end{align*}
Therefore
\begin{align*}
\omega^{\beta_1}m_1\leq\alpha<\omega^{\beta_1}(m_1+1).
\end{align*}
In particular,
\begin{align*}
\omega^{\beta_1}\leq\alpha<\omega^{\beta_1}\omega=\omega^{\beta_1+1}.
\end{align*}
The interval
\begin{align*}
\omega^\beta\leq\alpha<\omega^{\beta+1}
\end{align*}
has only one possible $\beta$, by the construction of the leading exponent. Hence $\beta_1$ is determined by $\alpha$. Once this $\beta_1$ is known, the integer $m_1$ is also determined, because it is the unique positive integer satisfying
\begin{align*}
\omega^{\beta_1}m_1\leq\alpha<\omega^{\beta_1}(m_1+1).
\end{align*}
Thus the first exponent and first coefficient of any Cantor normal form for $\alpha$ must agree.
[/guided]
[/step]
[step:Cancel matching leading blocks and finish by finite induction]
Suppose $\alpha$ has two such forms:
\begin{align*}
\alpha&=\omega^{\alpha_1}n_1+\omega^{\alpha_2}n_2+\cdots+\omega^{\alpha_k}n_k,\\
\alpha&=\omega^{\beta_1}m_1+\omega^{\beta_2}m_2+\cdots+\omega^{\beta_\ell}m_\ell.
\end{align*}
The preceding step implies
\begin{align*}
\alpha_1=\beta_1
\end{align*}
and
\begin{align*}
n_1=m_1.
\end{align*}
Let
\begin{align*}
\eta:=\omega^{\alpha_1}n_1.
\end{align*}
Define the two tails by
\begin{align*}
\rho&:=\omega^{\alpha_2}n_2+\cdots+\omega^{\alpha_k}n_k,\\
\sigma&:=\omega^{\beta_2}m_2+\cdots+\omega^{\beta_\ell}m_\ell,
\end{align*}
with the convention that the empty sum is $0$. Then
\begin{align*}
\eta+\rho=\alpha=\eta+\sigma.
\end{align*}
Left cancellation for ordinal addition gives
\begin{align*}
\rho=\sigma.
\end{align*}
If $\rho=\sigma=0$, then $k=\ell=1$ and the two forms agree. If the common tail is nonzero, the same argument applies to $\rho=\sigma$. Since the original forms have finite length, repeated cancellation terminates after finitely many applications. Hence $k=\ell$, and for every $i\in\{1,\dots,k\}$,
\begin{align*}
\alpha_i=\beta_i
\end{align*}
and
\begin{align*}
n_i=m_i.
\end{align*}
This proves uniqueness and completes the proof.
[/step]