Weyl orbit sums form a basis of finite Weyl invariants

Invariance of $f={\sum }_{\mu }{c}_{\mu }{e}^{\mu }$ is equivalent, by equality of coefficients in the formal basis, to $c_{w\mu }=c_{\mu }$ for all $w,\mu$. Thus its support is a finite union of entire orbits and its restriction to each orbit is one scalar times that orbit sum. This proves spanning by a finite sum. Distinct orbits have disjoint supports and each orbit sum has coefficient one at every point of its orbit, so a vanishing finite linear combination has every coefficient zero. This proves independence.

If $\lambda ,\mu$ are dominant and $\mu \le \lambda$, write $\lambda -\mu ={\sum }_i{n}_i{\alpha }_i$ with $n_i\ge 0$ integers. Both dominance inequalities give $({\alpha }_i,\lambda +\mu )\ge 0$, so $\mathrm{\parallel }\lambda {\mathrm{\parallel }}^2-\mathrm{\parallel }\mu {\mathrm{\parallel }}^2=(\lambda -\mu ,\lambda +\mu )={\sum }_i{n}_i({\alpha }_i,\lambda +\mu )\ge 0.$ For $\mu ={\sum }_i{a}_i{\omega }_i\in P$, the integer coordinate is $a_i=(\mu ,{\alpha }_i^{\vee })$ and satisfies $\mathrm{\mid }{a}_i\mathrm{\mid }\le \mathrm{\parallel }\lambda \mathrm{\parallel }\mathrm{\parallel }{\alpha }_i^{\vee }\mathrm{\parallel }$ by Cauchy–Schwarz. Hence only finitely many coordinate tuples, and therefore finitely many such $\mu$, exist.

F2 gives a unique dominant index for each orbit sum in step 1.1; in particular no ambiguity arises from a singular stabilizer. This reindexes the basis without any family choice. Step 1.2 proves the supplementary finiteness and norm bounds. The zero invariant has the empty expansion; the rank-zero system has only $m_0=1$; and at $\lambda =0$ the norm bound forces $\mu =0$. These cases obey the same arguments.