Integrable affine highest weights have nonnegative integral level

For dominant integral $\lambda$, its level is $k=\lambda (c_A)={\sum }_i{b}_i\lambda (h_i)$. Each $b_i$ is a positive integer by F1 and each label is a nonnegative integer by F2. Thus the finite sum belongs to ${\mathbb{Z}}_{\ge 0}$. Zero labels and $k=0$ are permitted in this assertion.

Suppose a nonzero highest-weight module of positive level $k$ were finite dimensional, of dimension $d\ge 1$. Fix a finite basis and write $E_i,F_i$ for the matrices of the simple generators. In finite indices, $\mathrm{tr}(E_i{F}_i)={\sum }_{r,s}(E_i{)}_{rs}(F_i{)}_{sr}={\sum }_{r,s}(F_i{)}_{rs}(E_i{)}_{sr}=\mathrm{tr}(F_i{E}_i)$, by interchanging $r,s$ and commuting scalars. Therefore F1 and F3 give $\mathrm{tr}(c_A)={\sum }_i{b}_i\mathrm{tr}(E_i{F}_i-F_i{E}_i)=0$. Its scalar action from F1 instead gives $\mathrm{tr}(c_A)=kd\mathrm{\ne }0$ over $\mathbb{C}$, a contradiction. Thus the module is infinite dimensional. This trace argument needs only nonzero level; positive level is the stated case.

Together 1.1 and 1.2 prove both assertions, including the integrable simple specialization whenever such a module is given. The zero module was explicitly excluded; dimension one is included in the trace contradiction with $d=1$. At level zero no nonzero trace contradiction is claimed. The finite basis and finite index exchanges use finite linear algebra and no AC, loop realization, or character formula.