Weyl Kac products are formal not analytic identities here

The completion in Kac Moody formal character completion consists of coefficient arrays supported in finitely many downward cones. Equality on this page means equality of those coefficients. For a fixed difference $\sum b_i{\alpha }_i\in Q^{+}$, each contributing summand of a product has simple coordinates bounded by the $b_i$, so there are finitely many pairs. In an inverse of $1+u$, with strictly positive-depth $u$, only powers up to $\sum b_i$ contribute. The root product of Kac Moody denominator product with root multiplicities has finitely many relevant roots and finite multiplicities at that same bound.

These bounds justify the sums, products, inverses and coefficient extractions used in the proofs. They do not supply a numerical value for $e^{\lambda }$, an analytic region of convergence, or permission to rearrange a conditionally convergent complex series. Even a specialization making a displayed denominator zero is not an operation asserted here. The zero coefficient, empty product and unit inverse are ordinary formal algebra conventions. Weyl symmetry was proved for the particular arrays used, not assumed for arbitrary elements of the completion. No AC or analytic assertion is being added.