The separating-root lemma, the exact facet halfspaces of the added cones, and the spherical convexity of |X(sigma)|

Inversion inside a subinterval. If $n=1$, (1) is vacuous because $P_{\sigma }$ has only its single positive root. Assume $n\ge 2$. Fix $u{\le }_{T}c$, $u\mathrm{\ne }1$, and let ${\mathrm{\Delta }}_u=\{d_1,\dots ,d_m\}$ be the simple system of $P_u$ given by [F3]. The item-18 factorization, in its second form with index $1$, is $u=R(d_1)\cdots R(d_m)$; it is reduced because ${\mathrm{\ell }}_T(u)=m$. Apply the inversion formula [F4] to the finite Coxeter system $W_u$ with simple system ${\mathrm{\Delta }}_u$. Its positive roots are exactly $P_u$, so $\{\alpha \in P_u:u^{-1}\alpha \in -P_u\}=\{{\epsilon }_1,\dots ,{\epsilon }_m\}=\{{\theta }_1,\dots ,{\theta }_m\}$, where the prefix roots are ${\epsilon }_j=R(d_1)\cdots R(d_{j-1})d_j$. The action of $u$ preserves $M(u)$, so a root in $M(u)$ is negative in this subsystem exactly when it is negative in the ambient positive system. Thus for $\alpha \in P_u\setminus \{{\theta }_1,\dots ,{\theta }_m\}$, $u^{-1}\alpha \in P_u$.

The first separator. Write $s=R({\tau }_s)$ and $a=R({\tau }_a)$. Since $B(\mu ({\tau }_s),{\tau }_a)=0$, [F2] and [F6] give ${\tau }_a\in M(sc)$ and hence $a{\le }_{T}sc$. The distinct reflections $s,a$ have product determinant $+1$ and nonidentity image, whereas every reflection has determinant $-1$; hence ${\mathrm{\ell }}_T(sa)=2$. Writing $sc=az$ gives $c=saz$ with $2+{\mathrm{\ell }}_T(z)={\mathrm{\ell }}_T(c)$, so $sa{\le }_{T}c$. Its moved space is contained in $M(\sigma )$ because both normals lie there, hence [F5] gives $sa{\le }_T\sigma$. The rank-two statement [F10] applied to $sa$ shows that ${\tau }_s$ and ${\tau }_a$ are the ordered endpoints of the simple system of $P_{sa}$. Put ${\tau }_b:=R({\tau }_a){\tau }_s={\tau }_s-2B({\tau }_s,{\tau }_a){\tau }_a$. The endpoint pairing in [F10] makes this a nonzero nonnegative combination of the endpoints; [F9] says it is a root, and [F15] makes it positive because its simple-root coordinates are nonnegative. The reflection $R({\tau }_a)$ preserves $M(sa)$, so ${\tau }_b\in P_{sa}$. The endpoints are the least and greatest roots of $P_{sa}$, hence ${\tau }_s\le {\tau }_b\le {\tau }_a$; equality ${\tau }_b={\tau }_a$ would imply ${\tau }_s=-{\tau }_a$, so ${\tau }_b<{\tau }_a$. Thus ${\tau }_b\in P_{\sigma }$ as $sa{\le }_T\sigma$. The pair $({\tau }_b,{\tau }_a)$ has reverse product $R({\tau }_a)R({\tau }_b)=sa{\le }_{T}c$ of length $2$, so [F7] gives $B(\mu ({\tau }_a),{\tau }_b)=0$. Also $B(\mu ({\tau }_s),{\tau }_b)=B(\mu ({\tau }_s),{\tau }_s-2B({\tau }_s,{\tau }_a){\tau }_a)=1>0$.

The linear map and finite facet test. Regard $C=\rho (c)$ as an orthogonal operator. Since $C-I$ is invertible, $\mu =2(I-C{)}^{-1}$ and $\mu +{\mu }^{\ast }=2(I-C{)}^{-1}+2(I-C^{-1}{)}^{-1}=2I$, because $(I-C^{-1}{)}^{-1}=-(I-C{)}^{-1}C$. Thus for every unit root $x$, $B(\mu (x),x)=1$. We will use the following finite polyhedral observation at each induction stage: if a full-dimensional cone in a finite-dimensional space is given by finitely many homogeneous linear inequalities, delete the redundant inequalities. For each remaining inequality $g\ge 0$, nonredundancy gives a point satisfying the other inequalities but with $g<0$; join it to an interior point where every remaining inequality is strict. The segment meets $g=0$ while all other inequalities remain strict, so $g=0$ cuts out a facet. Conversely each facet has a relative-interior point where at least one defining inequality is active, and that active hyperplane contains the facet. Hence the cone is the intersection of its active facet halfspaces. This proves the finite facet test without treating a redundant constraint as a facet.

The inclusions and rank base. The root-reflection dictionary and the definition of $W_{\sigma }$ give $P_{\sigma }={\mathrm{\Phi }}_{+}\cap M(\sigma )$. For $n\ge 2$, the wall statement (4)(iii) of item 18 and $B(\mu ({ϵ}_j),{ϵ}_j)=1$ from [F2] show that $\mu ({ϵ}_j)\cdot {\delta }_l=1$ for $l=j$ and $0$ otherwise: the wall makes the off-diagonal pairings zero, and ${ϵ}_j-{\delta }_j$ is a combination of earlier simple roots. Thus the restrictions $B(\mu ({ϵ}_j),-){\mathrm{\mid }}_{M(\sigma )}$ form the basis dual to $\mathrm{\Delta }$. Since the ${\theta }_j$ are a reordering of the ${ϵ}_j$, the restricted pairing functionals $B(\mu ({\theta }_j),-){\mathrm{\mid }}_{M(\sigma )}$ are this same dual basis in a different order. Therefore [F3] gives $B(\mu ({\theta }_j),\tau )\ge 0$ for every $\tau \in P_{\sigma }$. For $n=1$ the same inequalities follow directly from $P_{\sigma }=\{{\theta }_1\}$. If $\tau \le {\tau }_i$ and $j>i$, then $\tau <{\tau }_j$, so [F2] gives $B(\mu ({\tau }_j),\tau )\le 0$. Consequently $Y(\sigma ,{\tau }_i)\subseteq Z(\sigma ,{\tau }_i)$; by definition $c[X(\sigma ,{\tau }_i)]\subseteq Y(\sigma ,{\tau }_i)$. If $k=1$, then $P_{\sigma }=\{{\theta }_1\}$: it is the positive root set on the one-dimensional space $M(\sigma )$, and unit normalization leaves one positive root. The only eligible prefix is the singleton, $c[X(\sigma ,{\theta }_1)]={\mathbb{R}}_{\ge 0}{\theta }_1=M(\sigma )\cap \mu ({\theta }_1{)}^{+}$, whose sole facet is the origin in $\mu ({\theta }_1{)}^{\perp }$; this includes the empty base $X(1)=\{\mathrm{\varnothing }\}$ with cone $\{0\}$. Suppose henceforth $k\ge 2$, and let $i_0$ be the unique index with ${\tau }_{i_0}={\theta }_k$.

The opposite separator. Set ${\tau }_c:={\sigma }^{-1}{\tau }_s$. By [F1], ${\tau }_s\in P_{\sigma }$; the hypothesis excludes the inversion roots in [F3], so [F4] and step 1.1 imply ${\tau }_c\in P_{\sigma }$. Put $t:=R({\tau }_s)$ and $u:=t\sigma$. Write $\sigma =t{u}_0$ with additive reflection lengths, so $u=u_0$ and $u_0^{-1}\sigma =u_0^{-1}t{u}_0$ has length $1$; hence $u{\le }_T\sigma$. If $c=\sigma v$ is reduced, then $tc=u_{0}v$ and ${\mathrm{\ell }}_T(tc)=n-1={\mathrm{\ell }}_T(u_0)+{\mathrm{\ell }}_T(v)$ because $t{\le }_T\sigma {\le }_{T}c$, so also $u{\le }_{T}tc$. The vector $\mu ({\tau }_s)$ is fixed by $tc$ by [F2], hence by $u$ using [F5]-[F6]. Let $p$ be the orthogonal projection of $\mu ({\tau }_s)$ onto $M(\sigma )$. Its residual lies in $F(\sigma )\subseteq F(u)$, so $p\in F(u)$ as well; projection preserves its pairing with ${\tau }_s\in M(\sigma )$, giving $B(p,{\tau }_s)=1$. Therefore $\sigma p=tp=p-2{\tau }_s$. Since $\sigma {\tau }_c={\tau }_s$ and $\sigma$ is an isometry, $B(\mu ({\tau }_s),{\tau }_c)=B(p,{\tau }_c)=B(\sigma p,{\tau }_s)=B(p-2{\tau }_s,{\tau }_s)=-1$. By [F2], if ${\tau }_s<{\tau }_c$ then this pairing is nonnegative, and equality of the roots would give $1$; thus ${\tau }_c<{\tau }_s<{\tau }_a$. Since $s\sigma =\sigma R({\tau }_c)$ and $sa{\le }_T\sigma$, one has $a{\le }_{T}s\sigma =\sigma R({\tau }_c)$. Write $s\sigma =az$ with ${\mathrm{\ell }}_T(z)=k-2$. Then $\sigma =azR({\tau }_c)$ and $(aR({\tau }_c){)}^{-1}\sigma =R({\tau }_c)zR({\tau }_c)$ has length $k-2$ by conjugation invariance. The distinct reflections $a$ and $R({\tau }_c)$ have product of determinant $+1$ and this product is nonidentity, so its reflection length is $2$; the length equality therefore gives $aR({\tau }_c){\le }_T\sigma {\le }_{T}c$. Now [F7] gives $B(\mu ({\tau }_a),{\tau }_c)=0$. Together with step 1.2 this proves (1).

Base of the root-index induction. Put ${\sigma }_0:=R({\theta }_k)\sigma =R({\theta }_{k-1})\cdots R({\theta }_1)$. The prefix $\{{\theta }_1,\dots ,{\theta }_{k-1}\}$ is a face of the canonical $k$-simplex by [F7], so ${\sigma }_0{\le }_{T}c$ and ${\mathrm{\ell }}_T({\sigma }_0)=k-1$. The tuple ${\theta }_1<\cdots <{\theta }_{k-1}$ is eligible for ${\sigma }_0$, so [F3]'s componentwise minimality makes its canonical tuple ${\theta }_1^{\mathrm{\prime }}<\cdots <{\theta }_{k-1}^{\mathrm{\prime }}$ satisfy ${\theta }_j^{\mathrm{\prime }}\le {\theta }_j$ for every $j$. In particular ${\theta }_{k-1}^{\mathrm{\prime }}<{\theta }_k$, and appending ${\theta }_k$ to this tuple gives an increasing reduced tuple for $\sigma$; componentwise minimality for $\sigma$ gives ${\theta }_j\le {\theta }_j^{\mathrm{\prime }}$ for $j<k$. Thus ${\theta }_j^{\mathrm{\prime }}={\theta }_j$ for every $j<k$. Also $M({\sigma }_0)=\mathrm{span}({\theta }_1,\dots ,{\theta }_{k-1})$. The dual-basis result of step 1.4 makes $B(\mu ({\theta }_k),\tau )\ge 0$ for every $\tau \in P_{\sigma }$, while root order makes this pairing nonpositive when $\tau <{\theta }_k$ by [F2]; hence every such $\tau$ lies in $M(\sigma )\cap \mu ({\theta }_k{)}^{\perp }$. This hyperplane has dimension $k-1$ and contains the independent roots ${\theta }_1,\dots ,{\theta }_{k-1}$, so $M({\sigma }_0)=M(\sigma )\cap \mu ({\theta }_k{)}^{\perp }$. Since ${\theta }_{k-1}<{\theta }_k={\tau }_{i_0}$, the prefix ending at ${\tau }_{i_0-1}$ is eligible for ${\sigma }_0$. Every ${\tau }_j<{\theta }_k$ has $B(\mu ({\theta }_k),{\tau }_j)\ge 0$ by the dual-basis result above and $\le 0$ by the global order, so these earlier roots lie in $M({\sigma }_0)=M(\sigma )\cap \mu ({\theta }_k{)}^{\perp }$. Conversely $P_{{\sigma }_0}\subseteq P_{\sigma }$ by [F3]. Thus the two prefix vertex sets, and hence their full subcomplexes, agree: $F_0:=X(\sigma ,{\tau }_{i_0-1})=X({\sigma }_0,{\tau }_{i_0-1})$. The lower-rank induction gives $c[F_0]=Z({\sigma }_0,{\tau }_{i_0-1})$, a full-dimensional convex cone in $L_0:=M({\sigma }_0)$ with facet supports restricted from $\mu (b{)}^{\perp }$ for roots $b\in P_{{\sigma }_0}$.

Transporting the base facets through an apex. The following calculation applies both to the base apex $a={\theta }_k$ and to an inductive apex $a={\tau }_{i+1}$. Let $L=M(\sigma )\cap \mu (a{)}^{\perp }=M(R(a)\sigma )$, let $F$ be the already established full-dimensional base cone in $L$, and let a facet of $F$ have support the restriction of $\mu (b{)}^{\perp }$ for some $b\in P_{R(a)\sigma }\subseteq L$. Put $E:=M(\sigma )$ and $V_a:=F+{\mathbb{R}}_{\ge 0}a$. For $x\in E$, the decomposition $x=y+ta$, with $t=B(x,\mu (a))$ and $y\in L$, is unique. Thus $x\in V_a$ exactly when $t\ge 0$ and $y\in F$. If a facet of $F$ is given by $\epsilon B(y,\mu (b))\ge 0$ with $\epsilon \in \{1,-1\}$, its transported inequality is $\epsilon B(x,\nu )\ge 0$, where $\nu :=\mu (b)-B(\mu (b),a)\mu (a)$; it vanishes at $a$ and agrees with $\mu (b)$ on $L$. Since $B(\mu (a),b)=0$ and $\mu +{\mu }^{\ast }=2I$, $B(\mu (b),a)=2B(b,a)$, so $\nu =\mu (b-2B(b,a)a)=\mu (R(a)b)$. The equality of $F$ with the intersection of its active facet halfspaces therefore gives a finite halfspace presentation of $V_a$ in $E$ by $B(x,\mu (a))\ge 0$ and the transported inequalities; step 1.3 identifies its nonredundant inequalities with its facets. The vector $R(a)b$ is a signed root in $M(\sigma )$, so its positive representative $r$ belongs to $P_{\sigma }$ by [F3]. Thus every non-base facet of $V_a$ is a root-wall facet.

Inductive root-prefix step. Suppose $i\ge i_0$ and $K_i:=c[X(\sigma ,{\tau }_i)]=Z(\sigma ,{\tau }_i)$. Put $a:={\tau }_{i+1}$ and ${\sigma }^{\mathrm{\prime }}:=R(a)\sigma$. Since $R(a){\le }_T\sigma {\le }_{T}c$, write $c=\sigma v$ with ${\mathrm{\ell }}_T(v)=n-k$ and $\sigma =R(a){\sigma }^{\mathrm{\prime }}$. Then $R(a)c={\sigma }^{\mathrm{\prime }}v$; also ${\mathrm{\ell }}_T(R(a)c)=n-1$, since $R(a){\le }_{T}c$, so ${\sigma }^{\mathrm{\prime }}{\le }_{T}R(a)c{\le }_{T}c$ and ${\mathrm{\ell }}_T({\sigma }^{\mathrm{\prime }})=k-1$. The subspace $M({\sigma }^{\mathrm{\prime }})$ lies in $M(\sigma )$ because $\sigma$ and $R(a)$ preserve $M(\sigma )$, and it lies in $M(R(a)c)=\mu (a{)}^{\perp }$ by absolute-order monotonicity. Both $M({\sigma }^{\mathrm{\prime }})$ and $M(\sigma )\cap \mu (a{)}^{\perp }$ have dimension $k-1$: the latter is the kernel of the nonzero functional $x\mapsto B(x,\mu (a))$ on $M(\sigma )$, which is nonzero on $a\in M(\sigma )$ since $B(a,\mu (a))=1$. Hence $M({\sigma }^{\mathrm{\prime }})=M(\sigma )\cap \mu (a{)}^{\perp }$ and $P_{{\sigma }^{\mathrm{\prime }}}=P_{\sigma }\cap \mu (a{)}^{\perp }$. The link base $F$ on the old vertices orthogonal to $\mu (a)$ satisfies $c[F]=K_i\cap \mu (a{)}^{\perp }$: all old vertices have nonpositive pairing with $\mu (a)$, so a nonnegative combination pairs to zero exactly when it uses only zero-pairing vertices. Thus $F=X({\sigma }^{\mathrm{\prime }},{\tau }_i)$. Let ${ϵ}_1^{\mathrm{\prime }},\dots ,{ϵ}_{k-1}^{\mathrm{\prime }}$ be the prefix roots for the canonical simple system of ${\sigma }^{\mathrm{\prime }}$. They lie in $M({\sigma }^{\mathrm{\prime }})$, so $B(\mu (a),{ϵ}_j^{\mathrm{\prime }})=0$. If ${ϵ}_j^{\mathrm{\prime }}>a$, the distinct reflections $R(a)$ and $R({ϵ}_j^{\mathrm{\prime }})$ have product length $2$ by the determinant argument in [F9]. Since $R({ϵ}_j^{\mathrm{\prime }}){\le }_{T}R(a)c$, write $R(a)c=R({ϵ}_j^{\mathrm{\prime }})v$ with ${\mathrm{\ell }}_T(v)=n-2$; then $c=R(a)R({ϵ}_j^{\mathrm{\prime }})v$ is reduced, so $R(a)R({ϵ}_j^{\mathrm{\prime }}){\le }_{T}c$. By [F10] and the increasing order $a<{ϵ}_j^{\mathrm{\prime }}$, this is the endpoint factorization of the rank-two element $w:=R(a)R({ϵ}_j^{\mathrm{\prime }})$, so $B(a,{ϵ}_j^{\mathrm{\prime }})\le 0$. The root $d:=R(a){ϵ}_j^{\mathrm{\prime }}={ϵ}_j^{\mathrm{\prime }}-2B({ϵ}_j^{\mathrm{\prime }},a)a$ is a nonzero nonnegative combination of the endpoints; hence has nonnegative simple-root coordinates and is positive by [F15]. Since it lies in $M(w)$, [F3] puts it in $P_w$; it cannot equal $a$, since that would imply ${ϵ}_j^{\mathrm{\prime }}=R(a)a=-a$. Thus $a<d$ in the global order. Since $a,{ϵ}_j^{\mathrm{\prime }}\in M(\sigma )$ and $R(a)$ preserves $M(\sigma )$, this positive root lies in $P_{\sigma }={\mathrm{\Phi }}_{+}\cap M(\sigma )$. Now ${\sigma }^{\mathrm{\prime }-1}{ϵ}_j^{\mathrm{\prime }}={\sigma }^{-1}d$ is negative by step 1.1 applied to ${\sigma }^{\mathrm{\prime }}$, so step 1.1 applied to $\sigma$ gives $d\in \{{\theta }_1,\dots ,{\theta }_k\}$, contradicting $d>a\ge {\theta }_k$. Hence every ${ϵ}_j^{\mathrm{\prime }}<a$, and therefore ${\theta }_{k-1}^{\mathrm{\prime }}\le {\tau }_i$. Let $b$ be the last root of $P_{{\sigma }^{\mathrm{\prime }}}$ at or below ${\tau }_i$; it exists since ${\theta }_{k-1}^{\mathrm{\prime }}$ is such a root, and $b\ge {\theta }_{k-1}^{\mathrm{\prime }}$. Then $F=X({\sigma }^{\mathrm{\prime }},{\tau }_i)=X({\sigma }^{\mathrm{\prime }},b)$, so lower-rank induction gives $c[F]=Z({\sigma }^{\mathrm{\prime }},b)$, full-dimensional and convex in $L=M({\sigma }^{\mathrm{\prime }})$.

Initial cone and its facets. Let $K_{i_0}:=c[X(\sigma ,{\theta }_k)]$. By [F7], $K_{i_0}=c[F_0]+{\mathbb{R}}_{\ge 0}{\theta }_k$, so it is a full-dimensional convex cone. The base support is $\mu ({\theta }_k{)}^{\perp }$; each other facet has support $\mu (r{)}^{\perp }$ for a positive root $r\in P_{\sigma }$ by step 2.3. It contains the apex, so $B(\mu (r),{\theta }_k)=0$. If $r<{\theta }_k$ and $r\mathrm{\notin }\{{\theta }_1,\dots ,{\theta }_k\}$, step 2.1 gives two roots of $F_0$ on opposite sides of $\mu (r{)}^{\perp }$, contradicting that it supports the cone. Hence every side facet is labelled by a ${\theta }_j$ or a root $r>{\theta }_k$. The ${\theta }_j$ inequalities have positive sign on $K_{i_0}$ by [F3], the base apex inequality is positive on ${\theta }_k$ and zero on $F_0$, and each later-root inequality is nonpositive on all vertices of the prefix. The finite facet test of step 1.3 therefore gives $Z(\sigma ,{\theta }_k)\subseteq K_{i_0}$. With the reverse inclusion from step 1.4, equality holds at $i_0$; the same facet argument records that any other listed halfspace not defining one of these facets is redundant.

The new prefix is $X(\sigma ,{\tau }_{i+1})=X(\sigma ,{\tau }_i)\cup (a\ast F)$ by [F7], so its cone is $K_{i+1}=K_i\cup V_a$ with $V_a=c[F]+{\mathbb{R}}_{\ge 0}a$. Apply step 2.3 to each facet of $F$; every facet of $V_a$ is supported by $\mu (a{)}^{\perp }$ or by $\mu (r{)}^{\perp }$ for $r\in P_{\sigma }$. Each side facet contains $a$, so $B(\mu (r),a)=0$. If $r<a$ and $r$ is not a $\theta$-root, step 2.1 produces two vertices of $F$ on opposite sides of $\mu (r{)}^{\perp }$, contradicting support. Thus every facet label is a ${\theta }_j$, $a$, or a root $r>a$. Its containing halfspace is respectively $\mu ({\theta }_j{)}^{+}$, $\mu (a{)}^{+}$, or $\mu (r{)}^{-}$, by the sign inequalities in [F2]-[F3]. The cone $Z(\sigma ,{\tau }_{i+1})\cap \mu (a{)}^{+}$ satisfies all these facet halfspaces; step 1.3 therefore puts it in $V_a$. Its other half $Z(\sigma ,{\tau }_{i+1})\cap \mu (a{)}^{-}$ equals $Z(\sigma ,{\tau }_i)=K_i$. Consequently $Z(\sigma ,{\tau }_{i+1})\subseteq K_{i+1}$. The reverse containment follows from step 1.4, proving $K_{i+1}=Z(\sigma ,{\tau }_{i+1})$. The active-facet list is a subset of the defining inequalities; any omitted or repeated inequality is recorded as redundant.

Endpoint. The induction ends at $i=t$, where $Y(\sigma ,{\tau }_t)=c[P_{\sigma }]$. Thus the endpoint equality gives both the full positive-root cone and the claimed intersection with $M(\sigma )$ and the $\mu ({\theta }_j{)}^{+}$ halfspaces.

Spherical convexity. The cone $Z(\sigma ,{\tau }_t)$ is convex, and every nonzero vector in it lies in the common open halfspace of the positive roots by [F7]. For unit vectors $x,y$ in its sphere section, write $\varphi =\arccos B(x,y)<\pi$. If $\varphi =0$ the arc is constant. Otherwise put $e=(y-\cos \varphi x)\mathrm{/}\sin \varphi$, so $B(e,x)=0$ and $B(e,e)=1$. The shorter great-circle arc is $\gamma (s)=\cos (s)x+\sin (s)e=\frac{\sin (\varphi -s)}{\sin \varphi }x+\frac{\sin s}{\sin \varphi }y$ for $0\le s\le \varphi$. Its coefficients are nonnegative, so $\gamma (s)$ lies in the convex cone and has unit norm. This proves spherical convexity.

Since $X(\alpha )$ and $X(\beta )$ are full subcomplexes of the finite complex $X(c)$, every face cone of their intersection is a common face. If a point belongs to both $c[X(\alpha )]$ and $c[X(\beta )]$, it lies in cones $c[F]$ and $c[F^{\mathrm{\prime }}]$ for faces in the respective subcomplexes; [F11] identifies their intersection with $c[F\cap F^{\mathrm{\prime }}]$, which lies in the cone of the common subcomplex. Intersecting the resulting cone equality with $S^{n-1}$ proves the realization identity in (3). All inductions are finite and use no Choice. The theorem does not assert a meet of moved spaces or the lattice property of $[1,c]$.