Solution (source code)

= Solution

Use the <sl2 Lie algebra> relations $[H,X]=2X$, $[H,Y]=-2Y$ and $[X,Y]=H$. A <highest-weight vector> satisfies $Xv=0$ and $Hv=mv$, and $HY^jv=(m-2j)Y^jv$. For $k=0$, $XYv=YXv+Hv=mv$. Assuming the formula at $k-1$, one gets
$$
XY^{k+1}v=(YX+H)Y^kv=\bigl[k(m-k+1)+m-2k\bigr]Y^kv=(k+1)(m-k)Y^kv.
$$
Thus the <sl2 highest-weight lowering formula> is
$$
\boxed{XY^{k+1}v=(k+1)(m-k)Y^kv\qquad(k\geq0).}
$$
In particular a finite-dimensional <Irreducible Lie algebra representation> has highest weight $m\in\mathbb Z_{\geq0}$ and <weight vectors> $v,Yv,\ldots,Y^mv$, as in the <classification of finite-dimensional sl2 representations>.

Let $V_\lambda$ be a finite-dimensional <Irreducible Lie algebra representation> of a complex <semisimple Lie algebra>, with <highest weight> $\lambda$. Write $m_\lambda(\mu)=\dim(V_\lambda)_\mu$, taking it to be zero when $\mu$ is not a weight, and let $\rho$ be the <half-sum of positive roots>. The <Killing form> induces an <inner product> on the real span of weights. <Freudenthal multiplicity formula> states
$$
\boxed{\bigl((\lambda+\rho,\lambda+\rho)-(\mu+\rho,\mu+\rho)\bigr)m_\lambda(\mu)=2\sum_{\alpha>0}\sum_{j\geq1}(\mu+j\alpha,\alpha)m_\lambda(\mu+j\alpha).}
$$
The sums are finite. For a weight $\mu\ne\lambda$, the coefficient on the left is positive: move $\mu$ into the dominant <Weyl chamber>, use that a <weight> is below $\lambda$ in <dominance order>, and note that $(\mu,\rho)$ does not increase on moving back out of that chamber. The resulting recursion starts from $m_\lambda(\lambda)=1$.

Here is a proof using the allowed <Casimir operator>. Choose <root vectors> $E_\alpha,F_\alpha$ for positive and negative roots, normalized by $B(E_\alpha,F_\alpha)=1$, and let $t_\alpha\in\mathfrak h$ satisfy $B(t_\alpha,h)=\alpha(h)$. <Invariance of a bilinear form on a Lie algebra> gives $[E_\alpha,F_\alpha]=t_\alpha$. If $h_i,h^i$ are <dual bases> of the <Cartan subalgebra> under $B$, the <Casimir operator> is
$$
C=\sum_i h_ih^i+\sum_{\alpha>0}(E_\alpha F_\alpha+F_\alpha E_\alpha).
$$
On the <weight space> of $\mu$, the first sum acts by $(\mu,\mu)$. Replacing $E_\alpha F_\alpha$ with $F_\alpha E_\alpha+t_\alpha$ gives
$$
C\big|_{(V_\lambda)_\mu}=(\mu,\mu+2\rho)I+2\sum_{\alpha>0}F_\alpha E_\alpha\big|_{(V_\lambda)_\mu}.
$$
Define $T_\alpha(\mu)=\operatorname{tr}(F_\alpha E_\alpha\big|_{(V_\lambda)_\mu})$. The <cyclic trace identity between adjacent weight spaces> and the commutator relation yield
$$
T_\alpha(\mu)=\operatorname{tr}(E_\alpha F_\alpha\big|_{(V_\lambda)_{\mu+\alpha}})=T_\alpha(\mu+\alpha)+(\mu+\alpha,\alpha)m_\lambda(\mu+\alpha).
$$
Iterate upwards until the <weight spaces> vanish to obtain $T_\alpha(\mu)=\sum_{j\geq1}(\mu+j\alpha,\alpha)m_\lambda(\mu+j\alpha)$. Finally take the <trace> of the displayed restriction of $C$. Its <Casimir eigenvalue> is $(\lambda,\lambda+2\rho)$, so subtracting $(\mu,\mu+2\rho)m_\lambda(\mu)$ proves the formula. This trace argument handles <weight multiplicities> greater than one without choosing a separate <sl2 Lie algebra> string through each vector.