[proofplan] We construct a nonzero highest-weight quotient of the Verma module $M(\lambda)$ by imposing the finite rank-one string relation in every simple-root direction. The quotient is integrable for the simple-root $\mathfrak{sl}_2$ subalgebras, and a local Weyl-polytope argument bounds all of its weights in a finite subset of the root lattice. Since Verma module weight spaces are finite-dimensional, this quotient is finite-dimensional, and its irreducible quotient is $L(\lambda)$. [/proofplan]

[step:Choose Chevalley generators and impose the finite $\mathfrak{sl}_2$ string relations]For each $1\le i\le r$, choose root vectors $e_i\in\mathfrak g_{\alpha_i}$ and $f_i\in\mathfrak g_{-\alpha_i}$ such that \begin{align*} [e_i,f_i]=\alpha_i^\vee. \end{align*} Let $v_\lambda\in M(\lambda)$ denote the highest-weight vector. Then $\mathfrak n^+v_\lambda=0$, and $h v_\lambda=\lambda(h)v_\lambda$ for every $h\in\mathfrak h$. For each $i$, define $m_i := \lambda(\alpha_i^\vee)\in\mathbb Z_{\ge 0}$ and let $u_i := f_i^{m_i+1}v_\lambda\in M(\lambda)$. We claim that each $u_i$ is singular. First, the subalgebra \begin{align*} \mathfrak s_i := \operatorname{span}_{\mathbb C}\{e_i,\alpha_i^\vee,f_i\} \end{align*} is isomorphic to $\mathfrak{sl}_2(\mathbb C)$, and $v_\lambda$ has $\alpha_i^\vee$-weight $m_i$ for this subalgebra. By the $\mathfrak{sl}_2$ highest-weight calculation used in [citetheorem:9363], \begin{align*} e_i f_i^{m_i+1}v_\lambda = 0. \end{align*} If $j\ne i$, then $\alpha_j-\alpha_i$ is not a root because $\alpha_i$ and $\alpha_j$ are distinct simple roots. Hence \begin{align*} [e_j,f_i]=0. \end{align*} Since $e_jv_\lambda=0$, this gives \begin{align*} e_j u_i = e_j f_i^{m_i+1}v_\lambda = f_i^{m_i+1}e_jv_\lambda = 0. \end{align*} The positive nilpotent [Lie algebra](/page/Lie%20Algebra) $\mathfrak n^+$ is generated as a Lie algebra by the simple positive root vectors $e_1,\dots,e_r$, so $u_i$ is killed by all of $\mathfrak n^+$. Therefore $u_i$ is a singular vector of weight \begin{align*} \lambda-(m_i+1)\alpha_i. \end{align*}[/step]

[guided]The purpose of this step is to identify the relations that a finite-dimensional highest-weight module must satisfy along each simple root direction. Fix $i$. The chosen elements $e_i$, $f_i$, and $\alpha_i^\vee$ form a copy \begin{align*} \mathfrak s_i := \operatorname{span}_{\mathbb C}\{e_i,\alpha_i^\vee,f_i\} \end{align*} of $\mathfrak{sl}_2(\mathbb C)$, because their brackets are the standard simple-root brackets. The highest-weight vector $v_\lambda$ has $\alpha_i^\vee$-weight \begin{align*} m_i := \lambda(\alpha_i^\vee). \end{align*} The hypothesis $\lambda\in P^+$ says exactly that $m_i$ is a non-negative integer. For a finite-dimensional irreducible $\mathfrak{sl}_2(\mathbb C)$-module of highest weight $m_i$, the lowering string has length $m_i+1$. The calculation in [citetheorem:9363] gives \begin{align*} e_i f_i^{m_i+1}v_\lambda = 0. \end{align*} Thus $f_i^{m_i+1}v_\lambda$ is killed by the raising operator $e_i$ in the $i$-th simple-root direction. We must also check the other simple raising operators. Let $j\ne i$. Since $\alpha_i$ and $\alpha_j$ are distinct simple roots, the difference $\alpha_j-\alpha_i$ is not a root. Therefore the bracket of root spaces satisfies \begin{align*} [e_j,f_i]\in\mathfrak g_{\alpha_j-\alpha_i}=0. \end{align*} So $e_j$ commutes with $f_i$. Because $v_\lambda$ is a highest-weight vector, $e_jv_\lambda=0$, and hence \begin{align*} e_j f_i^{m_i+1}v_\lambda = f_i^{m_i+1}e_jv_\lambda = 0. \end{align*} Since the Lie algebra $\mathfrak n^+$ is generated by $e_1,\dots,e_r$, being killed by every $e_j$ implies being killed by all of $\mathfrak n^+$. Therefore \begin{align*} u_i := f_i^{m_i+1}v_\lambda \end{align*} is a singular vector of weight $\lambda-(m_i+1)\alpha_i$.[/guided]

[step:Form a nonzero quotient in which the simple lowering strings terminate] Let $N\subset M(\lambda)$ be the $\mathfrak g$-submodule generated by the singular vectors $u_1,\dots,u_r$, namely $N := U(\mathfrak g)u_1+\cdots+U(\mathfrak g)u_r$. Define the quotient module $Q := M(\lambda)/N$, let $q: M(\lambda)\to Q$ be the quotient homomorphism, and set $\bar v_\lambda := q(v_\lambda)\in Q$. Let \begin{align*} Q_+ := \mathbb Z_{\ge 0}\alpha_1+\cdots+\mathbb Z_{\ge 0}\alpha_r \end{align*} denote the positive root lattice cone. The submodule generated by $u_i$ has weights contained in \begin{align*} \lambda-(m_i+1)\alpha_i-Q_+, \end{align*} Thus $N$ has no weight $\lambda$ component, because every generator has weight strictly below $\lambda$ in the root order and applying elements of $U(\mathfrak n^-)$ lowers weights while applying elements of $\mathfrak h$ preserves weights and applying elements of $\mathfrak n^+$ cannot raise a singular generator above its own highest weight. Hence $v_\lambda\notin N$, so $\bar v_\lambda\ne 0$ and $Q$ is nonzero. By construction, for every $1\le i\le r$ we have $e_i\bar v_\lambda=0$, $\alpha_i^\vee \bar v_\lambda=m_i\bar v_\lambda$, and $f_i^{m_i+1}\bar v_\lambda=0$. [/step]

[step:Use the standard integrability lemma for highest-weight quotients] We use the following standard integrability lemma for semisimple Lie algebras. [claim:Simple-root nilpotence gives integrability of the quotient] Let $V$ be a highest-weight $\mathfrak g$-module generated by a highest-weight vector $v$ of weight $\lambda\in P^+$. Suppose that, for every $1\le i\le r$, \begin{align*} f_i^{\lambda(\alpha_i^\vee)+1}v=0. \end{align*} Then, for every $1\le i\le r$, the operators $e_i:V\to V$ and $f_i:V\to V$ are locally nilpotent. [/claim] [proof] Fix $i$. Let $\mathfrak s_i:=\operatorname{span}_{\mathbb C}\{e_i,\alpha_i^\vee,f_i\}$. The relation $f_i^{\lambda(\alpha_i^\vee)+1}v=0$, together with $e_i v=0$ and $\alpha_i^\vee v=\lambda(\alpha_i^\vee)v$, implies by the $\mathfrak{sl}_2$ highest-weight calculation in [citetheorem:9363] that the $\mathfrak s_i$-submodule generated by $v$ is finite-dimensional. Hence $e_i$ and $f_i$ are locally nilpotent on $U(\mathfrak s_i)v$. Choose an ordering of the negative simple-root vectors and write a spanning set of $V$ by PBW monomials $f_{j_1}\cdots f_{j_k}v$. We prove by induction on $k$ that each such vector lies in a finite-dimensional $\mathfrak s_i$-submodule. The case $k=0$ is the previous paragraph. For the induction step, suppose $w$ lies in a finite-dimensional $\mathfrak s_i$-submodule $E\subset V$ and consider $f_j w$. If $j=i$, then $f_iE\subset U(\mathfrak s_i)E$, which is finite-dimensional because $E$ is finite-dimensional as an $\mathfrak s_i$-module. If $j\ne i$, let $\alpha_j(\alpha_i^\vee)$ denote the corresponding Cartan integer. The Serre relations imply that the $\mathfrak s_i$-submodule \begin{align*} A_j:=U(\mathfrak s_i)f_j\subset \mathfrak g \end{align*} for the adjoint action is finite-dimensional; equivalently, it is spanned by finitely many iterated commutators $(\operatorname{ad} e_i)^a(\operatorname{ad} f_i)^b(f_j)$. Let $A_jE\subset V$ denote the complex linear span of all vectors $ae$ with $a\in A_j$ and $e\in E$. This space is finite-dimensional because $A_j$ and $E$ are finite-dimensional. It is also stable under $\mathfrak s_i$: for $x\in\mathfrak s_i$, $a\in A_j$, and $e\in E$, the module identity gives \begin{align*} x(ae)=[x,a]e+a(xe). \end{align*} Here $[x,a]\in A_j$ because $A_j$ is an adjoint $\mathfrak s_i$-submodule, and $xe\in E$ because $E$ is an $\mathfrak s_i$-submodule. Thus $x(ae)\in A_jE$, so $A_jE$ is a finite-dimensional $\mathfrak s_i$-submodule containing $f_jw$. This proves the induction claim. Every element of $V$ is a finite linear combination of such PBW monomial vectors, so it lies in a finite-dimensional $\mathfrak s_i$-submodule. On each finite-dimensional $\mathfrak s_i\cong\mathfrak{sl}_2(\mathbb C)$-module, $e_i$ and $f_i$ are nilpotent by the finite-dimensional $\mathfrak{sl}_2$ weight-string calculation. Thus $e_i$ and $f_i$ act locally nilpotently on $V$. [/proof] Applying the claim to $V=Q$ and $v=\bar v_\lambda$ is legitimate because $Q$ is generated by the image $\bar v_\lambda$ of the highest-weight vector, and the relations \begin{align*} f_i^{m_i+1}\bar v_\lambda=0 \end{align*} hold by construction. Therefore $Q$ is integrable for every simple-root subalgebra $\mathfrak s_i$. [/step]

[step:Bound the weights of the quotient by the Weyl orbit polytope] Let $\operatorname{Wt}(Q)\subset\mathfrak h^*$ denote the set of weights $\mu$ for which the weight space \begin{align*} Q_\mu := \{w\in Q : hw=\mu(h)w \text{ for every }h\in\mathfrak h\} \end{align*} is nonzero. Let $W$ be the Weyl group of the root system $\Phi$, generated by the simple reflections $s_1,\dots,s_r$ associated to $\alpha_1,\dots,\alpha_r$. For a subset $A\subset\mathfrak h^*$, write $\operatorname{conv}(A)$ for its convex hull in the finite-dimensional real [vector space](/page/Vector%20Space) $\mathbb R\Phi\subset\mathfrak h^*$ spanned by the roots; in particular, $\operatorname{conv}(W\lambda)$ denotes the convex hull of the finite orbit $W\lambda:=\{w\lambda:w\in W\}$. Since $Q$ is a quotient of $M(\lambda)$, every weight of $Q$ is a weight of $M(\lambda)$, and therefore \begin{align*} \operatorname{Wt}(Q)\subset \lambda-Q_+. \end{align*} [claim:Integrability gives the Weyl-polytope bound] If a highest-weight $\mathfrak g$-module $V$ has highest weight $\lambda$, has all weights contained in $\lambda-Q_+$, and is locally finite for every simple-root subalgebra $\mathfrak s_i$, then every weight of $V$ lies in $\operatorname{conv}(W\lambda)$. [/claim] [proof] Let $\operatorname{Wt}(V)$ denote the set of weights of $V$. First we prove that $\operatorname{Wt}(V)$ is stable under every simple reflection. Fix a simple root $\alpha_i$ and a weight $\mu\in\operatorname{Wt}(V)$. Choose a nonzero vector $v_\mu\in V_\mu$. The $\mathfrak s_i$-submodule generated by $v_\mu$ is finite-dimensional, because $V$ is locally finite for $\mathfrak s_i$. Finite-dimensional $\mathfrak{sl}_2$ weight-string symmetry therefore implies that the reflected $\mathfrak h$-weight \begin{align*} s_i\mu=\mu-\mu(\alpha_i^\vee)\alpha_i \end{align*} also occurs in this submodule. Hence $s_i\mu\in\operatorname{Wt}(V)$. Since the simple reflections generate $W$, the whole Weyl group preserves $\operatorname{Wt}(V)$. Now let $\omega_1^\vee,\dots,\omega_r^\vee$ be the fundamental coweights in the real span of the simple coroots, characterized by $\alpha_j(\omega_i^\vee)=\delta_{ij}$. We use the standard supporting-hyperplane description of the Weyl polytope: \begin{align*} \operatorname{conv}(W\lambda)=\{\nu\in\mathbb R\Phi: \nu(w\omega_i^\vee)\le \lambda(\omega_i^\vee)\text{ for every }w\in W\text{ and every }i\}. \end{align*} This description follows because the displayed inequalities are exactly the Weyl translates of the dominant-chamber walls supporting the orbit polytope at the dominant vertex $\lambda$. Take $\mu\in\operatorname{Wt}(V)$. Since $\operatorname{Wt}(V)$ is $W$-stable, $w^{-1}\mu$ is also a weight for every $w\in W$. The hypothesis on the weights gives $w^{-1}\mu\in\lambda-Q_+$, so there are nonnegative integers $n_1,\dots,n_r$ such that \begin{align*} \lambda-w^{-1}\mu=n_1\alpha_1+\cdots+n_r\alpha_r. \end{align*} Evaluating on $\omega_i^\vee$ gives \begin{align*} \mu(w\omega_i^\vee)=(w^{-1}\mu)(\omega_i^\vee)=\lambda(\omega_i^\vee)-n_i\le \lambda(\omega_i^\vee). \end{align*} These inequalities hold for every $w$ and every $i$, so the supporting-hyperplane description gives $\mu\in\operatorname{conv}(W\lambda)$. [/proof] The preceding step shows that $Q$ is locally finite for every simple-root subalgebra $\mathfrak s_i$, and $Q$ is a highest-weight quotient whose weights are contained in $\lambda-Q_+$. Applying the claim to $V=Q$ gives \begin{align*} \operatorname{Wt}(Q)\subset \operatorname{conv}(W\lambda). \end{align*} Combining the two inclusions gives \begin{align*} \operatorname{Wt}(Q)\subset (\lambda-Q_+)\cap \operatorname{conv}(W\lambda). \end{align*} The Weyl group $W$ is finite, so $\operatorname{conv}(W\lambda)$ is a compact polytope in the finite-dimensional real vector space spanned by the roots. The set $\lambda-Q_+$ is a translate of a lattice cone. Hence the intersection \begin{align*} (\lambda-Q_+)\cap \operatorname{conv}(W\lambda) \end{align*} is finite. Therefore $Q$ has only finitely many nonzero weights. [/step]

[step:Conclude finite-dimensionality from finite weight support and finite weight multiplicities] For each $\mu\in\operatorname{Wt}(Q)$, let \begin{align*} M(\lambda)_\mu := \{w\in M(\lambda): hw=\mu(h)w \text{ for every }h\in\mathfrak h\} \end{align*} denote the $\mu$-weight space of the Verma module. The quotient map $q:M(\lambda)\to Q$ restricts to a surjective [linear map](/page/Linear%20Map) \begin{align*} M(\lambda)_\mu\to Q_\mu. \end{align*} Thus \begin{align*} \dim_{\mathbb C}Q_\mu\le \dim_{\mathbb C}M(\lambda)_\mu. \end{align*} The Verma module weight [multiplicity formula](/theorems/2420) in [citetheorem:9376] gives finite-dimensionality of every weight space $M(\lambda)_\mu$. Since $\operatorname{Wt}(Q)$ is finite, we obtain \begin{align*} \dim_{\mathbb C}Q=\sum_{\mu\in\operatorname{Wt}(Q)}\dim_{\mathbb C}Q_\mu<\infty. \end{align*} By [citetheorem:9370], $M(\lambda)$ has a unique irreducible highest-weight quotient $L(\lambda)$. Since $Q$ is a nonzero highest-weight quotient of $M(\lambda)$, its irreducible quotient is the same $L(\lambda)$; equivalently, the canonical map $M(\lambda)\to L(\lambda)$ factors through $Q$. Therefore $L(\lambda)$ is a quotient of the finite-dimensional vector space $Q$, and hence \begin{align*} \dim_{\mathbb C}L(\lambda)\le \dim_{\mathbb C}Q<\infty. \end{align*} This proves that $L(\lambda)$ is finite-dimensional. [/step]