Highest-weight characters are unitriangular in Weyl orbit sums

By F1 the character is a finite sum with nonnegative integral coefficients constant on each Weyl orbit, hence lies in $\mathbb{C}[P{]}^W$. F2 and F3 group these coefficients into orbit sums with the same nonnegative integral coefficient at each orbit. If its dominant representative $\mu$ occurs, then $\mu$ itself is a support weight and F1 gives $\lambda -\mu \in Q_{+}$. The orbit of $\lambda$ has coefficient one because the top space is one-dimensional. Every other dominant representative is distinct from $\lambda$, so is strictly below it. This proves exactly the displayed expansion, including its finiteness.

Fix $\lambda$ and let $D=\{\mu \text{ dominant}:\mu \le \lambda \}$. It is finite by F2 and is downward closed among dominant weights by transitivity of $Q_{+}$ addition. On its finite free span with basis $m_{\mu }$, step 1.1 gives the character change-of-basis matrix $1+N$, where $N$ strictly lowers this partial order and has integer entries. A product of $\mathrm{\mid }D\mathrm{\mid }$ strictly lowering entries would require a chain of $\mathrm{\mid }D\mathrm{\mid }+1$ distinct points in $D$, which is impossible; hence $N^{\mathrm{\mid }D\mathrm{\mid }}=0$. Its inverse is the finite integer matrix $1-N+N^2-\cdots +(-N{)}^{\mathrm{\mid }D\mathrm{\mid }-1}$. It has diagonal one and only lower entries. This proves the asserted finite inverse on each ideal.

F2 says every invariant is a finite combination of orbit sums. Replacing each by its finite inverse expansion in step 2.1 proves character spanning. A finite relation among characters is supported in the union of finitely many finite dominant ideals; the same nilpotent triangular argument on that finite downward-closed union proves independence. Distinct-element orbit sums ensure no stabilizer factor appears at a wall weight. For rank zero only $\lambda =0$ exists, $L(0)=\mathbb{C}$ and $\mathrm{ch}L(0)=m_0=1$; for $\lambda =0$ the dominant ideal is the singleton by F2's norm bound. All matrices and sums used are finite and no AC is involved.