Positive restricted roots and nilpotent n algebra

Assume the Axiom of Choice. Let ${\mathfrak{g}}_0$ be a finite-dimensional real semisimple Lie algebra with Cartan decomposition ${\mathfrak{g}}_0={\mathfrak{k}}_0\oplus {\mathfrak{p}}_0$, let $\mathfrak{a}\subseteq {\mathfrak{p}}_0$ be a maximal abelian subspace, and let $\mathrm{\Sigma }=\mathrm{\Sigma }({\mathfrak{g}}_0,\mathfrak{a})$ be the restricted-root system with root spaces ${\mathfrak{g}}_0^{\lambda }$ (Restricted root and restricted root space, Restricted root space decomposition). An element $H_0\in \mathfrak{a}$ is regular (for $\mathrm{\Sigma }$) if $\lambda (H_0)\mathrm{\ne }0$ for every $\lambda \in \mathrm{\Sigma }$; such elements exist because $\mathrm{\Sigma }$ is finite and a finite union of proper subspaces of the real vector space $\mathfrak{a}$ cannot exhaust it (A finite-dimensional vector space over an infinite field is not a finite union of proper subspaces). A positive system of $\mathrm{\Sigma }$ is a subset ${\mathrm{\Sigma }}^{+}\subseteq \mathrm{\Sigma }$ for which there is a regular $H_0\in \mathfrak{a}$ with ${\mathrm{\Sigma }}^{+}=\{\lambda \in \mathrm{\Sigma }:\lambda (H_0)>0\};$ since $\lambda (H_0)\mathrm{\ne }0$ for every $\lambda \in \mathrm{\Sigma }$, such a set satisfies $\mathrm{\Sigma }={\mathrm{\Sigma }}^{+}\bigsqcup (-{\mathrm{\Sigma }}^{+})$ and is cut out on ${\mathfrak{a}}^{\ast }$ by the linear evaluation functional ${\mathrm{ev}}_{H_0}:{\mathfrak{a}}^{\ast }\to \mathbb{R}$, $\lambda \mapsto \lambda (H_0)$. Write ${\mathrm{\Sigma }}^{-}=-{\mathrm{\Sigma }}^{+}$ for the negative restricted roots.

Fix a positive system ${\mathrm{\Sigma }}^{+}$ and define $\mathfrak{n}=\mathfrak{n}({\mathrm{\Sigma }}^{+})={⨁}_{\lambda \in {\mathrm{\Sigma }}^{+}}{\mathfrak{g}}_0^{\lambda },$ the direct sum of the restricted-root spaces of the positive restricted roots. By the bracket relation of Restricted root space decomposition, $[{\mathfrak{g}}_0^{\lambda },{\mathfrak{g}}_0^{\mu }]\subseteq {\mathfrak{g}}_0^{\lambda +\mu }$ for all restricted roots, and a sum of positive functionals that is a restricted root is again positive for the same ordering; consequently $\mathfrak{n}$ is a Lie subalgebra of ${\mathfrak{g}}_0$. The subalgebra $\mathfrak{n}$ is nilpotent, the sum $\mathfrak{a}\oplus \mathfrak{n}$ is a solvable Lie subalgebra with $[\mathfrak{a}\oplus \mathfrak{n},\mathfrak{a}\oplus \mathfrak{n}]=\mathfrak{n}$, and ${\mathfrak{g}}_0={\mathfrak{k}}_0\oplus \mathfrak{a}\oplus \mathfrak{n}$ is a vector-space direct sum; these three assertions are proved in Iwasawa decomposition on the lie algebra level, where the nilpotency of $\mathfrak{n}$ is derived from the following positive bounds: if ${\mathrm{\Sigma }}^{+}$ is nonempty and $H_0$ is a regular element cutting out ${\mathrm{\Sigma }}^{+}$, the numbers $\lambda (H_0)>0$ for $\lambda \in {\mathrm{\Sigma }}^{+}$ have a positive minimum and a finite maximum, so every iterated bracket of sufficiently many elements of $\mathfrak{n}$ vanishes; and if ${\mathrm{\Sigma }}^{+}=\mathrm{\varnothing }$ then $\mathfrak{n}=0$ is trivially nilpotent.