For a finite-dimensional Irreducible Lie algebra representation of a complex semisimple Lie algebra with highest weight , this recursion computes its weight multiplicities from . Here is the half-sum of positive roots and the inner product is induced by the Killing form. Write the Casimir operator on the weight- space as . The cyclic trace identity between adjacent weight spaces gives . Taking the trace and using the Casimir eigenvalue proves the formula. Only finitely many terms are nonzero.
Use the sl2 Lie algebra relations , and . A highest-weight vector satisfies and , and . For , . Assuming the formula at , one gets
Thus the sl2 highest-weight lowering formula is
In particular a finite-dimensional Irreducible Lie algebra representation has highest weight and weight vectors , as in the classification of finite-dimensional sl2 representations.
Let be a finite-dimensional Irreducible Lie algebra representation of a complex semisimple Lie algebra, with highest weight . Write , taking it to be zero when is not a weight, and let be the half-sum of positive roots. The Killing form induces an inner product on the real span of weights. Freudenthal multiplicity formula states
The sums are finite. For a weight , the coefficient on the left is positive: move into the dominant Weyl chamber, use that a weight is below in dominance order, and note that does not increase on moving back out of that chamber. The resulting recursion starts from .
Here is a proof using the allowed Casimir operator. Choose root vectors for positive and negative roots, normalized by , and let satisfy . Invariance of a bilinear form on a Lie algebra gives . If are dual bases of the Cartan subalgebra under , the Casimir operator is
On the weight space of , the first sum acts by . Replacing with gives
Define . The cyclic trace identity between adjacent weight spaces and the commutator relation yield
Iterate upwards until the weight spaces vanish to obtain . Finally take the trace of the displayed restriction of . Its Casimir eigenvalue is , so subtracting proves the formula. This trace argument handles weight multiplicities greater than one without choosing a separate sl2 Lie algebra string through each vector.