Post History

I think I've solved the problem: The formula is correct.

For the proof I'm using the decomposition $\alpha = \lambda + m$ and $\beta = \mu + n$ from the question. Also, I'll use the notation $A\cong B$ for “$A$ is order-equivalent to $B$”. Also note that $+$ and $\cdot$ denote the standard ordinal addition and multiplication.

Since the minimal sum is commutative by definition, it suffices to consider the case $\alpha\le\beta$. In that case, there exists an unique $\delta$ such that $\alpha+\delta = \beta$.

Now the first observation is that in this case, the right hand side of the explicit formula can be written as $2\cdot\alpha + \delta$. This can be seen by the fact that $2\cdot\alpha = \lambda + 2m$, and therefore for finite $\delta$ we have $m+\delta = n$ and therefore $2\cdot\alpha+\delta = \alpha + n$, while for infinite $\delta$ we have $m + \delta = \delta$ and therefore $2\cdot\alpha+\delta = \alpha + \delta = \beta$.

Next, we can see that $2\cdot\alpha+\delta$ is a sum of $\alpha$ and $\beta$, since by the definitions of the ordinal operations, we have the partition $2\cdot\alpha+\delta = 2\cdot\alpha\cup D$ where $D\cong\delta$, and $2\cdot\alpha\cong \alpha\times\\{0,1\\}$ under lexicographical order, giving rise to the partition $P=A\cup A'$ where $A\cong A'\cong\alpha$. Then $B=A'\cup D\cong\beta$, thus $A$ and $B$ are a partition of the form required by the definition of a sum. Therefore we have for the minimal sum $\alpha\boxplus\beta  \le 2\cdot\alpha + \delta$.

What remains to prove is that $\alpha\boxplus\delta\ge 2\cdot\alpha + \delta$. Now for infinite $\delta$, this is obvious, as there the right hand side is just $\beta$, and $\alpha\boxplus\beta\ge\beta$ by construction. For finite $\delta$, we know that the finite part of $\alpha$ and the finite part of $\beta$ must both necessarily be mapped to the finite part of $\alpha\boxplus\beta$, as otherwise we'd have a strictly increasing mapping from a larger to a smaller ordinal. Thus in this case the finite part of the minimal sum has to be a sum of the finite parts. But for finite numbers, the sum is unique, which concludes the proof.