Dominant representatives, wall stabilizers and terminating reflection descent

For a positive real coroot $\beta$, if $w^{-1}\beta$ is positive then $\lambda (\beta )=\eta (w^{-1}\beta )\ge 0$ by F2, since a positive coroot is a nonnegative integral combination of simple coroots. Hence $N(\lambda )=\{\beta >0:\lambda (\beta )<0\}$ is contained in $\mathrm{Inv}(w^{-1})$, and is finite by F1. Each negative-label reflection keeps the weight integral: its new labels are $\lambda (h_j)-\lambda (h_i)a_{ji}$ by F3. It also stays in the same orbit, so finiteness persists.

Suppose $\eta ,\zeta =w\eta$ are both dominant, and take a reduced expression $w=s_{i_1}\cdots s_{i_t}$. We prove by induction on $t$ that $\zeta =\eta$ and this word is a product of zero-label reflections of $\eta$. For $t=0$ both conclusions are immediate. For $t>0$, canceling the last factor gives an expression of length $t-1$ for $w{s}_{i_t}$, so F1 gives $w{h}_{i_t}<0$. By duality and dominance, $0\le \eta (h_{i_t})=\zeta (w{h}_{i_t})\le 0$. Thus $\eta (h_{i_t})=0$, and F3 gives $s_{i_t}\eta =\eta$. The prefix represents $w{s}_{i_t}$ and is reduced: a shorter prefix would shorten the original word after appending its last factor. The prefix still sends $\eta$ to $\zeta$, so the induction hypothesis proves both assertions, and the deleted last factor is also a zero-label reflection.

Suppose $\lambda (h_i)<0$. On positive coroots other than $h_i$, the bijection $\beta \mapsto s_i\beta$ identifies negative pairings for $s_i\lambda$ with those for $\lambda$. The pairing at $h_i$ changes from negative to positive. Thus $\mathrm{\mid }N(s_i\lambda )\mathrm{\mid }=\mathrm{\mid }N(\lambda )\mathrm{\mid }-1$. If no simple label is negative, every positive coroot pairs nonnegatively and the weight belongs to $P^{+}$ by F2 and integrality. Therefore after at most $\mathrm{\mid }N(\lambda )\mathrm{\mid }$ reflections any such process must stop at a dominant weight: a further negative label would require a negative integer cardinality. Selecting the least negative index specifies each finite step without AC.

Step 1.2 proves uniqueness of the dominant endpoint in 2.1. Applying it when $w\eta =\eta$ proves that every stabilizing element belongs to the stated generated subgroup. Conversely, each displayed generator fixes $\eta$ directly by F3, so every product does too. At a strictly positive-label weight the subgroup is trivial; at zero labels nontrivial stabilizers are permitted. If the starting weight is already dominant, $N$ is empty and zero reflections are performed. Empty simple systems have trivial $W$. The zero weight is fixed by every simple reflection, giving stabilizer $W$. No choice axiom or reality assumption on complementary Cartan values was used.