Integrability can be checked on simple root sl2 subalgebras

By F2 and F3 their span has exactly the three independent standard ${\mathfrak{s}\mathfrak{l}}_2$ generators and brackets. Repeatedly using the three commutation relations puts every enveloping word into a linear combination of $f_i^a{e}_i^b{h}_i^c$: an adjacent swap decreases the number of out-of-order pairs, and its commutator term has shorter word length. Induction on length and inversions terminates. On a weight vector $v$, the last factor acts by the scalar $\mu (h_i{)}^c$, so the cyclic span is spanned by $f_i^a{e}_i^{b}v$. Only spanning is needed, not PBW independence or semisimplicity.

For the reverse implication, let a vector lie in a finite-dimensional ${\mathfrak{g}}_i$-invariant subspace $W$. The operator $h_i$ is diagonalizable on $W$: on each vector it has a finite eigen-expansion inherited from the ambient weight module, and polynomial interpolation in $h_i$ keeps its components in $W$. Since $W$ is finite dimensional, only finitely many eigenvalues occur. By F2, $e_i$ and $f_i$ shift these eigenvalues by $2$ and $-2$. On an $h_i$-eigenvector, a nonzero string of length greater than the number of eigenvalues would require more distinct eigenvalues than $W$ has. Thus both operators are nilpotent on $W$, and locally nilpotent on $V$. F1 gives integrability.

Assume integrability. For a weight vector $v$, local nilpotence of $e_i$ permits only finitely many nonzero $e_i^{b}v$. For each of these finitely many vectors, local nilpotence of $f_i$ permits only finitely many nonzero $f_i^a{e}_i^{b}v$. Their span in 1.1 is therefore finite dimensional and is the cyclic ${\mathfrak{g}}_i$-submodule. Every vector of a weight module is a finite sum of weight vectors. The sum of their finite-dimensional cyclic submodules is again finite dimensional and invariant, proving local finiteness.

This works for every simple index. Zero vectors and the zero module have zero cyclic spans, while a one-dimensional cyclic submodule satisfies the same spectral argument. Each spanning calculation and each choice of a bound concerns only finitely many vectors; no choice principle or complete-reducibility theorem was used. Both implications are proved.