The compact Weyl group is finite

Let $g\in C_G(S)$ and let $A$ be the closure in $G$ of the subgroup generated by $S$ and $g$, that is, of ${\bigcup }_{n\in \mathbb{Z}}{g}^{n}S$. Then $A$ is closed by definition, compact because $G$ is compact, abelian and a subgroup by [L2], and hence by [L2] an embedded Lie subgroup: a compact abelian Lie group. Its identity component $A^0$ is a compact connected abelian Lie group, hence by [L1] a torus, and $A^0$ is open in $A$ because identity components of Lie groups are open.

If $a\in G$ lies in a maximal torus $M$, then by the surjectivity of the exponential map of the torus $M$ in [L1] there is $X\in \mathrm{Lie}(M)\subseteq \mathfrak{g}$ with $a=\exp (X)$; in particular every element of $A$ has this form.

A torus $U$ has surjective $N$-th power maps: write $u=\exp V$ by [L1] and take $\exp (V\mathrm{/}N)$. It also has a dense cyclic generator, as follows. Use [L1] to identify $U$ with ${\mathbb{R}}^r\mathrm{/}{\mathbb{Z}}^r$. Choose $x_1,\dots ,x_r$ so that $1,x_1,\dots ,x_r$ are rationally independent: at each of the finitely many stages the rational span of the previous choices is countable (enumerate rational tuples), so [L5] supplies a real outside it. Let $H$ be the closure of the subgroup generated by $x+{\mathbb{Z}}^r$. If $H\mathrm{\ne }U$, [L2, L4] make $U\mathrm{/}H$ a nontrivial compact connected abelian Lie group, hence a positive-dimensional torus by [L1]. Projection to one circle factor gives a nontrivial smooth homomorphism $\chi :U\to \mathbb{R}\mathrm{/}\mathbb{Z}$ vanishing on $H$. By [L6], $\chi (v+{\mathbb{Z}}^r)=\mathrm{\ell }(v)+\mathbb{Z}$ for the real-linear differential $\mathrm{\ell }$; since each coordinate vector represents zero in $U$, its coefficients $m_j=\mathrm{\ell }(e_j)$ are integers. At least one is nonzero, since otherwise naturality and surjectivity of the exponential would make $\chi$ trivial. But $\chi (x)=0$ says $\sum m_j{x}_j\in \mathbb{Z}$, contradicting the chosen independence. Thus $H=U$. For $r=0$ the identity generates $U$.

The set ${\bigcup }_{n\in \mathbb{Z}}{g}^n{A}^0$ is an open subgroup of $A$ containing ${\bigcup }_{n\in \mathbb{Z}}{g}^{n}S$, whose closure is $A$; an open subgroup is closed and its cosets partition $A$, so this union is all of $A$. Hence $A\mathrm{/}{A}^0$ is generated by the coset $g{A}^0$, and being a discrete compact group it is finite, of some order $N$; consequently $g^N\in A^0$.

There exists $a\in A$ whose powers are dense in $A$: since $A^0$ is a torus, step 1.3 supplies an element $a_0$ with dense powers; let $b\in A$ represent a generator of the cyclic group $A\mathrm{/}{A}^0$ of order $N$ from step 2.1; the $N$-th power map of the torus $A^0$ is surjective by step 1.3, so there is $c\in A^0$ with $c^N=b^{-N}{a}_0$; then $(bc{)}^N=b^N{c}^N=a_0$, so the closure of the powers of $bc$ contains the dense powers of $a_0$ and hence $A^0$, and $(bc{)}^k\in b^k{A}^0$ for every $k$, so it contains a representative of each coset of $A\mathrm{/}{A}^0$; therefore the closure of the cyclic subgroup generated by $a:=bc$ is all of $A$.

Write $a=\exp (X)$ by step 1.2 and let $S^{\mathrm{\prime }}$ be the closure of $\{\exp (tX):t\in \mathbb{R}\}$; this is a compact connected abelian subgroup of $G$ by [L2] and hence a torus, and it contains $A$: indeed $a^k=\exp (kX)$ for every integer $k$, so the cyclic subgroup generated by $a$ lies in $\{\exp (tX)\}$, and taking closures gives $A\subseteq S^{\mathrm{\prime }}$; in particular $S^{\mathrm{\prime }}$ contains $S$ and $g$.

If $x\in C_G(S)$ and $S^{\mathrm{\prime }}$ is constructed for $x$ as in step 4.1, then $S^{\mathrm{\prime }}$ is a torus containing $S$ and $x$; conversely every torus containing $S$ lies in $C_G(S)$, since it is abelian. Hence $C_G(S)=\bigcup \{S^{\mathrm{\prime }}:S^{\mathrm{\prime }}\text{ a torus},S\subseteq S^{\mathrm{\prime }}\}$, a union of connected sets all containing the nonempty connected set $S$, which is therefore connected.

For a maximal torus $T$, applying step 4.1 to $x\in C_G(T)$ produces a torus $S^{\mathrm{\prime }}$ containing $T$ and $x$; maximality of $T$ forces $S^{\mathrm{\prime }}=T$, so $x\in T$. Hence $C_G(T)=T$; in particular ${\mathfrak{c}}_{\mathfrak{g}}(\mathfrak{t})=\mathfrak{t}$ for $\mathfrak{t}=\mathrm{Lie}(T)$, because if $X$ centralizes $\mathfrak{t}$, then $\mathrm{Ad}(\exp (tX))H=H$ for $H\in \mathfrak{t}$: by [L6] this curve satisfies the linear equation $v\mathrm{\prime }={\mathrm{ad}}_{X}v$ with constant solution $H$. Naturality and the surjectivity of ${\exp }_T$ show $\exp (tX)\in C_G(T)=T$, so differentiating gives $X\in \mathfrak{t}$.

The normalizer $N:=N_G(T)$ is closed, because it is the intersection, over $t\in T$, of the closed conditions $gt{g}^{-1}\in T$ and $g^{-1}tg\in T$; hence $N$ is a compact Lie subgroup by [L2] and contains $T$ as a closed normal subgroup, so $N\mathrm{/}T$ is a compact Lie group by [L4]. Its Lie algebra is $\mathfrak{n}\mathrm{/}\mathfrak{t}$, where $\mathfrak{n}=\mathrm{Lie}(N)$; for $X\in \mathfrak{n}$ and $H\in \mathfrak{t}$ the curve $t\mapsto \mathrm{Ad}(\exp tX)H$ lies in $\mathfrak{t}$, so differentiating at $0$ gives $[X,H]\in \mathfrak{t}$, and then for every $H^{\mathrm{\prime }}\in \mathfrak{t}$ the invariance identity of [L3] gives $⟨[X,H],H^{\mathrm{\prime }}⟩=⟨X,[H,H^{\mathrm{\prime }}]⟩=0$ because $\mathfrak{t}$ is abelian; positive definiteness yields $[X,H]=0$, so $X\in {\mathfrak{c}}_{\mathfrak{g}}(\mathfrak{t})=\mathfrak{t}$ by step 5.2. Hence $\mathfrak{n}=\mathfrak{t}$ and the Lie algebra of $N\mathrm{/}T$ is zero; by [L2] the group $N\mathrm{/}T$ is discrete, and being compact it is finite. Thus $W(G,T)=N_G(T)\mathrm{/}T$ is finite.

The action of $W(G,T)$ on $T$ has kernel $\{gT:g\in N,gt{g}^{-1}=t\text{ for all }t\in T\}=C_G(T)\mathrm{/}T=T\mathrm{/}T=\{T\}$ by step 5.2, so it is faithful; if $gT$ acts trivially on $\mathfrak{t}=\mathrm{Lie}(T)$ then $\mathrm{Ad}(g)$ fixes $\mathfrak{t}$ pointwise, hence $g\exp (X)g^{-1}=\exp (\mathrm{Ad}(g)X)=\exp (X)$ for all $X\in \mathfrak{t}$ and $g$ centralizes $T$, so $gT=T$; thus the action on the Lie algebra is faithful as well. The Axiom of Choice entered through the cited metric and structure theory.