Casimir norm excludes nonzero denominator corrections

Apply F2 to the one-dimensional trivial module, whose highest weight is zero and character one. Multiplying its Verma expansion by $e^{\rho }P$ using F3 and identifying this factor as $D$ by F6 gives $D={\sum }_{\mu }{c}_{\mu }{e}^{\mu +\rho }$. Therefore a nonzero coefficient of $e^{\rho -\beta }$ in $D$ must satisfy $(\rho -\beta {)}^2={\rho }^2$, or ${\beta }^2=2(\rho ,\beta )$. All multiplications are coefficientwise finite by F1 and F2.

If $C$ has nonconstant support, take a least-height $\beta ={\sum }_i{k}_i{\alpha }_i\mathrm{\ne }0$ in it. F1 gives $k_i\ge 0$ and $\beta (h_i)\le 0$ for every $i$. F4 gives $({\alpha }_i,\xi )=d_i\xi (h_i)$ with $d_i>0$. Thus ${\beta }^2={\sum }_i{k}_i{d}_i\beta (h_i)\le 0,2(\rho ,\beta )=2{\sum }_i{k}_i{d}_i>0.$ This contradicts the equality required in step 1.1, if that coefficient of $D$ is nonzero.

It is nonzero. Write $a=e^{-\rho }{A}_{\rho }$ and $p=e^{-\rho }D=aC$. In the coefficient at $e^{-\beta }$ every mixed product with a nonzero degree of $C$ strictly smaller than $\beta$ vanishes by minimality. Hence $p_{\beta }=C_{\beta }+a_{\beta }$. A nonzero $a_{\beta }$ would require $\beta =\rho -w\rho$ for some $w$. The reflection formula and F4 show the form is Weyl invariant: expansion of a reflected pairing cancels its two cross terms against $({\alpha }_i,{\alpha }_i)=2d_i$. Thus such a $\beta$ would satisfy $(\rho -\beta {)}^2={\rho }^2$, contradicting the two inequalities of step 2.1. So $a_{\beta }=0$ and $p_{\beta }=C_{\beta }\mathrm{\ne }0$, contradicting step 1.1 after all. There is no nonconstant support, and F1's unit constant coefficient gives $C=1$. The choice of a least-height term is finite, so no AC is used.