Alphabeta Math
Pipeline-generated
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 4 results · all verified · 4 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs; all 4 also cleared it.

Bipartite Coxeter Elements and Ordered Root Complexes

1 · Prerequisites

2 · Summary

This page constructs the ordered positive-root model for an irreducible finite Coxeter group and proves the geometry of its root complex. The companion bipartite-coxeter-elements-and-ordered-root-complexes-examples gives explicit rank-two and type-A3 calculations.

Bipartite data and root order

The tree Coxeter diagram splits into two commuting color classes. The page's first item defines their Coxeter element, cyclic simple-root and dual-vector recursions, and the conditional map μ(v)=−2(CV−I)−1v, with CV=ρ(c). The Coxeter plane, ordered-root enumeration, and invertibility of rho(c) - id proves the Coxeter-plane angle, the positive-root enumeration Φ+=(ρ1,…,ρnh/2), and invertibility of CV−I. The mu-dot-root identities, the cone separation, and the canonical simple systems of the subintervals [1, sigma] proves the μ-root sign and vanishing rules and constructs the canonical simple systems and increasing reduced tuples for every σ≤Tc.

The ordered root complex

The Brady-Watt ordered root complex X(c), its subcomplexes X(sigma) and X(sigma,rho), and their positive-cone realizations defines X(c) from its ordered two-root compatibility relation, then defines the full subcomplexes X(σ), their inclusive root prefixes, and positive-cone realizations. It makes no geometric claim. The factorization criterion, linear independence of the faces, and the geometric simplicial structure of X(sigma) proves the exact factorization and zero-pairing criterion, independence of simplex roots, the prefix link rule, and common-face intersections of geometric cones.

The separating-root lemma, the exact facet halfspaces of the added cones, and the spherical convexity of |X(sigma)| proves the separating-root lemma and the rank-and-prefix facet induction. Each transported facet normal is computed from μ(b)−B(μ(b),a)μ(a)=μ(R(a)b); the proof identifies its sign and excludes unsupported earlier roots. At the endpoint, c[X(σ)] is the positive-root cone cut out by the canonical μ(θj)+ halfspaces, so its unit-sphere section is spherically convex. The theorem also records the exact realization intersection identity and explicitly abstains from asserting that arbitrary moved-space intersections are meets or that [1,c] is a lattice.

Prerequisites

The reading path places finite-reflection-length-and-orthogonal-moved-spaces, finite-lattice-projections-and-coxeter-chain-labels and spherical-simplex-metrics-angular-links-and-cones before this page. The first supplies the reflection-length and orthogonal moved-space framework; the second is the earlier lattice and chain-label context; the third supplies the spherical Gram-simplex result used to identify each face-cone section in step 4.1 of item 20. Item-level inputs are recorded in the authored items and their batch manifest.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

The bipartite Coxeter element, its ordered prefix roots, and the conditional vector map mu(a) = -2(c-1)^{-1}a

Definition

For the irreducible case, let (W,S) be a finite-type Coxeter system with S finite of cardinality n≥1, length function ℓ, Coxeter diagram Γ and standard parabolics WT=⟨s:s∈T⟩ (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups, Coxeter diagrams: edges, labels, components and finite type, The subgroup ⟨S⟩ generated by a subset, the cyclic subgroup ⟨g⟩, and cyclic groups); let V=RS, let B be the Coxeter form with B(es,es)=1 (The real Coxeter form, its radical, reflections, and form-preserving maps, Descent of the reflection representation, unit root norms, and conjugation of reflections (3)), and let ρ:W→GL(V), Φ={ρ(w)es} and T={wsw−1} be the canonical reflection representation, the root system and the reflection set (The canonical reflection homomorphism, roots, reflections, and the positive cone); assume Γ is connected, equivalently (W,S) is irreducible (Coxeter diagrams: edges, labels, components and finite type). The form B is positive definite (Finiteness criterion: W is finite exactly when the Coxeter form is positive definite). Write αs:=es for the simple roots and ra for the reflection with normal a. Clause (5) separately specifies the componentwise extension to reducible finite-type systems.

(1) The bipartition. Γ is connected and has no cycle, hence is a tree (Exclusions for positive definite diagrams: trees, valency, labels, chains and arms (2)); a tree has a bipartition, i.e. there is a partition S=J⊔K with m(s,t)=2 for all distinct s,t in the same part (A bipartite graph and a proper two-colouring of its vertices, A finite graph is bipartite if and only if it has no odd cycle). Concretely, fix s0∈S, let J be the set of vertices at even distance from s0 in Γ and K the set at odd distance, and note that the pair {J,K} is determined up to interchanging the two classes. Choose such a bipartition and order the simple reflections and their simple roots as α1,…,αn, with corresponding simple reflections s1,…,sn and reflections Ri:=rαi, so that J={s1,…,sr} and K={sr+1,…,sn} for r:=∣J∣. For distinct si,sj in either class, m(si,sj)=2; the Coxeter relators si2=sj2=(sisj)2=1 therefore imply sisj=sjsi (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups). Thus the products a:=∏i=1rsi and b:=∏i=r+1nsi do not depend on the order of their factors, and

c:=ab=s1s2⋯sn∈W,h:=ord⁡(c)∈N

are well defined (W is finite, so h≥1). For n=1 one has J={s1}, K=∅, a=s1, b=1, c=s1 and h=2; empty products are 1. For n≥2 both classes are nonempty because Γ is connected.

(2) Cyclic indexing. Read subscripts i of si, αi, Ri and βi cyclically modulo n: si+n:=si, αi+n:=αi, Ri+n:=Ri, and βi+n:=βi for the dual family below. The cyclic indexing of the βi is part of the convention: it is what makes the vector μi below well defined for every i≥1 (see (3)).

(3) Prefix roots and dual vertices. Let G=(B(αj,αk))j,k=1n be the Gram matrix. It is invertible: for x≠0, the basis property gives ∑jxjαj≠0, so xTGx=B(∑jxjαj,∑jxjαj)>0. Set βi:=∑k=1n(G−1)kiαk; symmetry of G gives B(βi,αj)=∑kGjk(G−1)ki=δji. These vectors are unique, since a vector orthogonal to every basis vector is orthogonal to itself and hence is zero by positive definiteness. Thus (β1,…,βn) is the B-dual family of (α1,…,αn). Define, for every integer i≥1,

ρi:=R1R2⋯Ri−1 αi,μi:=R1R2⋯Ri−1 βi,

the empty product for i=1 being the identity. Put cV:=ρ(c)∈GL(V). The recursions ρi+n=cVρi and μi+n=cVμi (valid for all i≥1) follow by separating the first n factors and using cyclic indexing; they are also recorded in The Coxeter plane, ordered-root enumeration, and invertibility of rho(c) - id ↗.

(4) The conditional vector map μ. For v∈V put

μ(v):=−2 (cV−idV)−1v,

defined only if the linear map cV−idV∈GL(V) is invertible (Invertible linear maps, linear isomorphisms, and inverse linear maps). This definition asserts neither the invertibility of cV−idV nor the identity μ(ρi)=μi; both are proved in The Coxeter plane, ordered-root enumeration, and invertibility of rho(c) - id ↗, the recorded justifier of this definition. Once defined, μ is a linear map on all of V, with μ(ρi)=μi for every i≥1 and μ(cVkv)=cVkμ(v) for all k∈Z and v∈V, since cV commutes with cV−idV.

(5) Reducible and empty systems. For a finite-type system with connected components S1,…,Sm, apply (1)--(4) to each irreducible factor (Wi,Si), where Wi=WSi (Disconnected diagrams, direct products, and comparison of invariant forms). With component bipartitions Si=Ji⊔Ki, let ai,bi,ci be the resulting group elements and hi=ord⁡(ci). The product c=c1⋯cm is a product of the simple reflections in every component. Under the direct-product decomposition, ck=1 exactly when cik=1 for every i, so its order is h=lcm⁡(h1,…,hm). Choose a block order of the components and list the root and dual-vector families in that order. The operator cV=ρ(c) is the direct sum of cVi=ρ(ci); as in (4), the map μ is defined exactly when every cVi−idVi is invertible, and then is their direct sum. For S=∅ one has m=0, W={1}, c=1, h=1 (the empty lcm is 1), V={0} and empty root and dual-vector families; the unique endomorphism of V is invertible, so μ is that unique map. No single number nh/2 is claimed for reducible systems whose components have unequal Coxeter numbers.

(6) Abstentions. Each ρi is a root by definition, since R1⋯Ri−1=ρ(s1⋯si−1) and αi=esi. This item does not assert that the first nh/2 roots enumerate the positive roots, any sign pattern for (B(μi,ρj)), or a spherical realization of the ordered root complex; those are proved by later items in this pair. No Choice is used.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

The Coxeter plane, ordered-root enumeration, and invertibility of rho(c) - id

Statement

Let (W,S) be an irreducible finite-type Coxeter system with ∣S∣=n≥2, with bipartition J⊔K=S and data α1,…,αn, s1,…,sn, a,b,c=ab, h=ord⁡(c), βi,ρi,μi and conditional map μ as in The bipartite Coxeter element, its ordered prefix roots, and the conditional vector map mu(a) = -2(c-1)^{-1}a. Put r:=∣J∣, so J={s1,…,sr} and K={sr+1,…,sn}. Let CV:=ρ(c)∈GL(V) denote the linear action of c, let C be the primal chamber in V and C∘ its interior, and let Hα={x∈V:B(x,α)=0} be the root hyperplanes (The real Coxeter form, its radical, reflections, and form-preserving maps, The canonical reflection homomorphism, roots, reflections, and the positive cone, The finite reflection arrangement, its chambers, the spherical chamber complex, and the coset face poset). Write w0 for the longest element (The longest element as the opposition of the chamber, and longest elements of finite parabolics). Then:

(1) The Coxeter-plane eigenvector. The matrix A=(2(δst−B(es,et)))s,t∈S has nonnegative entries, zero diagonal, and connected nonzero off-diagonal pattern. There are p∈R>0S and λ∈(0,2) with Ap=λp, and λ=2cos⁡(π/h).

(2) The invariant plane and chamber sector. Put u:=∑s∈Jpsαs, v:=∑t∈Kptαt, d:=∑s∈Jps2 and P:=span(u,v). Then d>0, B(u,u)=B(v,v)=d, B(u,v)=−λd/2, the plane P is invariant under ρ(a), ρ(b) and CV, and

ρ(a)u=−u,ρ(a)v=v+λu,ρ(b)v=−v,ρ(b)u=u+λv.

Thus CV∣P is a rotation through 2θ, where θ:=arccos⁡(λ/2)=π/h. The intersection C∩P is a sector of angle θ whose relative interior lies in C∘; it contains a point with trivial W-stabiliser. The restrictions of ρ(a) and ρ(b) generate a dihedral group of order 2h on P. Its 2h translates of C∩P are exactly the full-dimensional chamber sections wC∩P: they are the sectors cut out by the h root-hyperplane traces, with pairwise disjoint relative interiors. The set of traces {Hα∩P:α∈Φ} is exactly the set of h reflection lines of this dihedral action.

(3) Enumeration of the roots. Every ρi is a root, ρi+n=CVρi for all i≥1, and

Φ+={ρ1,…,ρnh/2},Φ−=−Φ+={ρnh/2+1,…,ρnh},

with all nh listed roots pairwise distinct; hence the sequence has exact period nh. Moreover ∣Φ+∣=∣T∣=nh/2=ℓ(w0). If h is even then w0=ch/2. If h is odd then n is even, r=∣J∣=∣K∣=n/2, and w0=c(h−1)/2a. Accordingly, the word

(s1⋯sn)h/2or(s1⋯sn)(h−1)/2s1⋯sr

is a reduced expression of w0 of length nh/2, with prefix roots exactly ρ1,…,ρnh/2 in this order.

(4) Invertibility of the linear action minus the identity. The operator CV−idV is invertible. Consequently the conditional map from the preceding definition is defined on all of V and satisfies μ(ρi)=μi for every i≥1.

For n=1 the conclusions are direct: Φ+={α1}={ρ1}, c=s1 and h=2. Reducible systems are handled componentwise using the preceding definition's clause (5), and no uniform nh/2 count is asserted for unequal component Coxeter numbers. No Choice is used.

Facts & Assumptions

Given: An irreducible finite-type Coxeter system (W,S) with ∣S∣=n≥2, the bipartite data αi,si,Ri,a,b,c,h,βi,ρi,μi of The bipartite Coxeter element, its ordered prefix roots, and the conditional vector map mu(a) = -2(c-1)^{-1}a, the operator CV=ρ(c), the positive definite space (V,B) with root system Φ=Φ+⊔Φ− and reflection set T, and the transferred primal chamber C and root hyperplanes Hα.

[F1]

The defining data have Γ connected, J={s1,…,sr}, K={sr+1,…,sn}, pairwise orthogonal simple roots within each class, and ρi+n=CVρi, μi+n=CVμi for every i≥1. The vectors βi satisfy B(βi,αj)=δij. The bipartite Coxeter element, its ordered prefix roots, and the conditional vector map mu(a) = -2(c-1)^{-1}a (1)-(3)

[F2]

B is positive definite, ρ is faithful and preserves B, and every root satisfies B(α,α)=1; for each s, Rs=ρ(s) is the reflection x↦x−2B(x,αs)αs. Finiteness criterion: W is finite exactly when the Coxeter form is positive definite, Descent of the reflection representation, unit root norms, and conjugation of reflections (1)-(3), The root-length criterion and faithfulness of the canonical reflection representation (3)

[F3]

The roots split as Φ=Φ+⊔Φ− with Φ−=−Φ+ and Φ+ consists exactly of the roots with nonnegative simple-root coordinates; each Rs sends αs to −αs and permutes Φ+∖{αs}. Root sign coherence and the action of simple reflections on positive roots (1)-(3)

[F4]

The transferred chamber is C={x∈V:B(x,αs)≥0 ∀s} with interior defined by strict inequalities; the chambers wC tile V with disjoint interiors, and a point in wCI has stabiliser wWIw−1. In particular a point of C∘ has trivial stabiliser, and a point in the relative interior of CJ has stabiliser WJ. The interior of every chamber is disjoint from every root hyperplane, and Hρ(w)α=ρ(w)Hα. The finite reflection arrangement, its chambers, the spherical chamber complex, and the coset face poset, The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere (1),(3)

[F5]

For every w∈W and s∈S, ℓ(ws)>ℓ(w) if and only if ρ(w)αs∈Φ+. The root-length criterion and faithfulness of the canonical reflection representation (1)

[F6]

The longest element satisfies ρ(w0)Φ+=Φ−, ℓ(w0)=∣Φ+∣=∣T∣, w02=1, and it is the unique element of length ℓ(w0). The longest element as the opposition of the chamber, and longest elements of finite parabolics (1)(ii)-(iv)

[F7]

The map Φ+→T, α↦tα, is a bijection, ρ(tα)=rα, and tα=tβ exactly when α=±β. Thus root hyperplanes are in bijection with T. The inversion formula ∣N(w)∣=ℓ(w), the root-reflection dictionary and strong exchange (1)(i)-(iv)

[F8]

The coordinate norm ∥⋅∥0 and inner product ⟨⋅,⋅⟩0 are the standard Euclidean ones on RS. For n≥1 the coordinate unit sphere is nonempty (it contains each simple basis vector αs) and compact. The identity map is continuous, and a linear map L is continuous because ∥Lx−Ly∥0≤K∥x−y∥0 for some K≥0. The inner product of continuous vector-valued maps is continuous, so q(x)=⟨x,Ax⟩0 is continuous; every continuous real-valued function on a nonempty compact subset of Rn attains a maximum. The real Coxeter form, its radical, reflections, and form-preserving maps, The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn, Every Euclidean linear map has a unique matrix and satisfies ∥Lh∥2≤K∥h∥2 for some K≥0, A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions (3), For n≥1, every Euclidean closed ball and every Euclidean sphere of positive radius is compact, For a nonempty subset of Rn with n≥1, compactness, closedness and boundedness, pseudocompactness, and attainment of extrema by every continuous real-valued function are equivalent (4)

[F9]

For a reducible diagram with components Si, W is the direct product of the WSi and V is their orthogonal direct sum; the root, reflection and bipartite constructions are componentwise. Disconnected diagrams, direct products, and comparison of invariant forms, Coxeter diagrams: edges, labels, components and finite type

Proof

technique · maximize the nonnegative adjacency quadratic form, build the invariant plane, and use the chamber tiling to determine its angle and the roots crossing its walls
1.1F1F2algebra

Write ∥x∥02:=∑s∈Sxs2 for the standard coordinate norm and set q(x):=xTAx. If m(s,t)=∞ for distinct s,t, then B(es+et,es+et)=0, contradicting positive definiteness; hence every off-diagonal Coxeter exponent is finite. Therefore Ass=0 and Ast=−2B(es,et)=2cos⁡(π/m(s,t))≥0 for s≠t, with Ast>0 exactly on the edges of the connected diagram. Also q(x)=2∥x∥02−2B(x,x)<2∥x∥02 for every nonzero x.

1.2F1F2algebra

For 1≤i≤n, the first n prefix vectors satisfy ρi=αi for i≤r and ρi=ρ(a)αi=αi+∑s∈JAsiαs for i>r: the earlier reflections in the same color class fix αi, while each reflection in the other class adds its Asiαs and fixes the other roots of that class. Hence the coordinate matrix of (ρ1,…,ρn) relative to the ordered basis (α1,…,αn) is block upper triangular with identity diagonal blocks, so these vectors form a basis. The cyclic definitions give ρi+n=CVρi and μi+n=CVμi for every i≥1, because each block of n reflections has product c. Each ρi is a root, being the image of a simple root by an element of W.

2.1F2F8step 1.1algebra

The unit sphere for ∥⋅∥0 is compact, so q attains a maximum λ there; normalizing es+et for an edge {s,t} gives a positive value of q, so λ>0, and step 1.1 at a maximizer gives λ<2. Let p be a unit maximizer. For y with ⟨p,y⟩0=0, maximality at (p+ty)/(1+t2∥y∥02)1/2 gives 2t⟨Ap,y⟩0+t2(q(y)−λ∥y∥02)≤0 for every real t. If ⟨Ap,y⟩0≠0, a sufficiently small t of the same sign makes the linear term dominate the quadratic term, a contradiction. Thus Ap is orthogonal to every y⊥p, so it is a multiple of p; pairing with p gives Ap=λp.

2.2F1F2step 1.2algebra

For 1≤i≤n, duality gives B(βi,αj)=0 for every j≠i, so Rjβi=βi for every j≠i and in particular μi=R1⋯Ri−1βi=βi. Also Riβi=βi−2αi. Thus CVβi=R1⋯Rnβi=R1⋯Ri−1(βi−2αi)=μi−2ρi=βi−2ρi, so (CV−idV)βi=−2ρi.

3.1F1step 2.1algebra

Since every entry of A is nonnegative, q(∣p∣)≥q(p)=λ, while ∥∣p∣∥0=1, so ∣p∣ is also a maximizer and satisfies A∣p∣=λ∣p∣ by step 2.1. Put r:=∣p∣. If rs>0 and Ast>0, then λrt=∑uAturu≥Atsrs>0; since λ>0 and the edge graph of A is connected, positivity propagates to every coordinate. Thus we may take p∈R>0S, proving the existence claim in (1).

3.2F1step 1.2step 2.2algebra

The vectors β1,…,βn form a basis by the construction in the preceding definition, and ρ1,…,ρn form a basis by 1.2; thus 2.2 shows that CV−idV maps one basis to the other up to the nonzero scalar −2, so it is invertible. If i=mn+j with m≥0 and 1≤j≤n, then the cyclic recursions in F1 and the identity in 2.2 give (CV−idV)μi=CVm(CV−idV)μj=−2CVmρj=−2ρi. Applying the conditional map of the preceding definition now yields μ(ρi)=μi for all i≥1, proving (4) and the definition's well-definedness justification.

4.1F1F2step 3.1algebra

Put d′:=∑t∈Kpt2. Since distinct simple roots in either color class are orthogonal, B(u,u)=d and B(v,v)=d′. Multiplying the eigenvector equations ∑t∈KAstpt=λps by ps and summing over s∈J gives ∑s∈J,t∈KpsAstpt=λd; summing the equations indexed by K gives the same left side equal to λd′, hence d=d′>0. Finally B(u,v)=−12∑s∈J,t∈KpsAstpt=−λd/2. The Gram matrix on (u,v) is d(1−λ/2−λ/21) with determinant d2(1−λ2/4)>0, so u,v are independent and P is a plane.

5.1F1F2step 4.1algebra

For s∈J, Rs fixes αs′ for s′∈J∖{s} and negates αs; the corresponding statement holds in K. For t∈K, the commuting reflections in a give ρ(a)αt=αt+∑s∈JAstαs, and for s∈J, ρ(b)αs=αs+∑t∈KAtsαt. Summing with coefficients pt and ps and using Ap=λp yields ρ(a)u=−u, ρ(a)v=v+λu, ρ(b)v=−v, and ρ(b)u=u+λv. Thus P is invariant under ρ(a),ρ(b) and CV=ρ(a)ρ(b).

6.1F2step 5.1algebra

In the basis (u,v), ρ(a)=(−1λ01), ρ(b)=(10λ−1), and CV∣P=(λ2−1−λλ−1). The vectors f1:=u/d and f2:=(v+λ2u)/d(1−λ2/4) are B-orthonormal, and direct substitution gives CVf1=(λ2/2−1)f1+λ1−λ2/4 f2. With θ:=arccos⁡(λ/2)∈(0,π/2) these coefficients are cos⁡(2θ) and sin⁡(2θ); since CV preserves B and has determinant 1 on P, it is the rotation through 2θ.

7.1F1F2step 4.1step 5.1step 6.1algebra

For x=ξu+ηv∈P, one has B(x,αs)=ps(ξ−λ2η) for s∈J and B(x,αt)=pt(η−λ2ξ) for t∈K. Thus C∩P is given by ξ≥λ2η and η≥λ2ξ; because 0<λ/2<1, these inequalities imply ξ,η≥0, and their strict versions place the relative interior in C∘. Its boundary rays are xJ:=λu+2v (the J simple-root hyperplanes) and xK:=2u+λv (the K simple-root hyperplanes). Their squared B-norms are both d(4−λ2) and B(xJ,xK)=λd(2−λ2/2), so the sector angle has cosine λ/2 and equals θ. The restrictions of ρ(a) and ρ(b) are reflections in the lines RxJ and RxK: they fix those lines, are involutions, and are nonidentity on P by 4.1.

8.1F1F2F4step 6.1step 7.1algebra

Let m0 be the order of CV∣P. Since it rotates through 2θ∈(0,π), m0≥3 and 2θ=2πj/m0 for an integer j with 1≤j<m0/2 and gcd⁡(j,m0)=1. The subgroup D:=⟨ρ(a)∣P,ρ(b)∣P⟩ consists of the m0 distinct rotations (CV∣P)k and the m0 distinct reflections ρ(a)∣P(CV∣P)k, so ∣D∣=2m0. Distinct elements of D have lifts g~∈⟨a,b⟩ with distinct restrictions to P, hence are distinct elements of W; by F4 their chamber interiors are distinct and disjoint. Thus the orbit of S0:=C∩P consists of 2m0 distinct sectors of angle θ, each of the form ρ(g~)C∩P, with pairwise disjoint relative interiors. Hence 2m0θ≤2π, so j=1 and θ=π/m0; equality shows the sectors cover P. As m0∣h by F1, the element cm0 fixes every point of P, in particular a point of C∘∩P; its stabiliser is trivial, so cm0=1 and h∣m0. Thus m0=h and λ=2cos⁡(π/h), completing (1) and the angle claims of (2).

9.1F2F4step 7.1step 8.1algebra

For every root α, the trace Hα∩P is a line: if P⊆Hα, the nonidentity reflection tα fixes a point of C∘∩P, contradicting its trivial stabiliser; otherwise the nonzero linear functional x↦B(x,α) restricts to a nonzero functional on the two-plane P, whose kernel is a line. Each such line is a root-hyperplane trace and cannot meet the relative interior of any sector ρ(g~)S0, because that relative interior lies in the chamber interior ρ(g~)C∘, which is disjoint from the arrangement. Conversely the two boundary lines of S0 are traces of simple-root hyperplanes by 7.1, and their images under D are root-hyperplane traces because ρ(W) permutes roots. These images are all the sector boundary lines: the 2h sectors from 8.1 tile P and have 2h distinct boundary rays, while every root trace must be one of those lines because it cannot meet a sector interior. Opposite rays define the same line, so the traces are exactly h distinct lines. The connected components of the complement of these lines are the sector interiors. Each component is connected and the ambient chamber interiors form a disjoint open cover of it, so it lies in one chamber interior. Conversely, if a full-dimensional chamber section contained points from two components, choose them in its relative interior; their segment lies in that relative interior by convexity and crosses a root trace, contradicting disjointness of chamber interiors from the arrangement. Hence the full-dimensional chamber sections are exactly the 2h sectors.

10.1F1F2F4F7step 6.1step 7.1step 8.1step 9.1algebra

The ray R>0xJ lies in the relative interior of the face CJ, so its stabiliser is WJ; similarly the stabiliser of R>0xK is WK. Every element of WJ reduces to a product of a subset I⊆J because its simple generators are commuting involutions; the subset products are distinct because their ρ-images have different signs on the independent simple roots and ρ is faithful by [F2]. The image of the product for I acts by −1 on span⁡{αs:s∈I} and by +1 on its B-orthogonal complement, so its (−1)-eigenspace has dimension ∣I∣; therefore it is a reflection exactly when ∣I∣=1, and the reflections in WJ are precisely its ∣J∣=r simple generators. The same reasoning gives exactly ∣K∣=n−r reflections in WK. The 2h distinct boundary rays from 8.1 alternate between the two types, so there are h of each; conjugating the stabiliser count around them gives hr+h(n−r)=hn incidences between rays and ambient root hyperplanes. Each hyperplane contributes exactly two incidences because its trace is a line. Hence the arrangement has hn/2 hyperplanes, so ∣T∣=hn/2 by the root-reflection correspondence of [F7].

11.1step 9.1step 10.1algebra

If h is odd, a semicircle from a point of C∘∩P to its antipode crosses each trace line once; since every root-hyperplane trace is one of these lines, it meets each ambient root hyperplane exactly once. The boundary-ray types alternate, so one type occurs (h+1)/2 times and the other (h−1)/2 times. Counting the hyperplanes met using 10.1 gives hn/2=((h+1)/2)r+((h−1)/2)(n−r) if the more frequent rays have type J, and the same equation with r and n−r interchanged if they have type K. Either equation gives r=n/2. Thus n is even and ∣J∣=∣K∣=n/2.

12.1F1step 9.1step 10.1step 11.1algebra

Choose the direction around the circle so that the first boundary ray of S0 is xJ. The rays then occur in the cyclic order p2k=CVkR>0xJ and p2k+1=CVkρ(a)R>0xK for k=0,…,h−1: ρ(a) reflects across the J boundary, while CV advances by two sector angles. The hyperplanes through p2k are exactly HCVkαs for s=s1,…,sr, and those through p2k+1 are exactly HCVkρ(a)αt for t=sr+1,…,sn, by the stabiliser counts and the description of the reflections in WJ,WK from 10.1. These are precisely the blocks Hρkn+1,…,Hρkn+r and Hρkn+r+1,…,Hρ(k+1)n by the cyclic prefix definition in 1.2. The first h rays carry hn/2 hyperplanes: this is hn/2 from h/2 complete color pairs when h is even, and n(h−1)/2+r=hn/2 when h is odd by 11.1. The opposite semicircle carries the other hn/2 hyperplanes. Each half-turn list is pairwise distinct because every trace line meets that semicircle only once, and the listed hyperplanes in each boundary block are distinct simple-root images.

13.1F3step 1.2step 12.1algebra

Fix k≤hn/2. The first half-turn list of hyperplanes in 12.1 is pairwise distinct, so ρk≠±ρj for every j<k. For 1≤j≤k, put yj:=Rj−1⋯R1ρk, with y1=ρk and yk=αk; for j<k, yj≠±αj, since otherwise applying R1⋯Rj−1 would give ρk=±ρj. Each Rj preserves the sign of every root other than ±αj by [F3], so yj and yj+1=Rjyj have the same sign. Since yk=αk∈Φ+, descending induction gives ρk∈Φ+ for every k≤hn/2.

14.1F5F6step 11.1step 13.1algebra

Let q:=hn/2. The word w=ch/2 for even h, or w=c(h−1)/2a for odd h, has exactly q letters; in the odd case this uses r=n/2 from 11.1. Its prefix roots are ρ1,…,ρq by the cyclic definition, and these are positive by 13.1. At each step the root-length criterion therefore increases the prefix length by one, so the word is reduced and ℓ(w)=q=ℓ(w0). By uniqueness of the longest element, w=w0, proving the formulas for w0 in (3).

15.1F3F5F6step 10.1step 12.1step 13.1step 14.1algebra

The full word (s1⋯sn)h represents 1 and splits after its first q letters, whose product is w0 by 14.1. Its remaining q-letter suffix also represents w0−1=w0, so it is reduced. Every prefix of a reduced word is reduced; applying the root-length criterion at each next letter shows that every prefix root of this suffix is positive. Its corresponding global prefix root is obtained by applying ρ(w0) and is therefore negative by [F6]. The second half in 12.1 has pairwise distinct hyperplanes, so these negative roots are pairwise distinct as well. Hence the first q roots are all of Φ+ because ∣Φ+∣=∣T∣=q by [F6] and 10.1, and the second q are all of Φ−=−Φ+. The first and second lists are disjoint by sign, giving pairwise distinctness of all nh roots; CVh=idV gives period nh, and that distinctness makes it exact. This proves (3).

16.1F9given∎

In rank one, B(α1,α1)=1, CV=−id, ρ1=α1, ρ2=−α1, and μ=idV, so the stated conclusions hold. For a reducible finite-type system, V, B, ρ, the root systems and CV split over the components by [F9]; each rank-one or irreducible component satisfies the result just proved, so CV−idV is a direct sum of invertible operators and the map μ and root enumeration hold componentwise. The total number of positive roots is ∑inihi/2, with no common nh/2 formula asserted when the component orders differ. No Choice is used.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

The mu-dot-root identities, the cone separation, and the canonical simple systems of the subintervals [1, sigma]

Statement

Let (W,S) be an irreducible Coxeter system of finite type with S finite of cardinality n≥2, with the data αi, βi, si, Ri, a, b, c, h, (ρi), (μi) and the linear map μ of The bipartite Coxeter element, its ordered prefix roots, and the conditional vector map mu(a) = -2(c-1)^{-1}a, and assume the conclusions of The Coxeter plane, ordered-root enumeration, and invertibility of rho(c) - id (so that Φ+={ρ1,…,ρnh/2} and μ(ρi)=μi). Let ℓT, ≤T, M, F be reflection length, absolute order and the moved and fixed spaces, and let Pσ:={α∈Φ+:tα≤Tσ} for σ≤Tc, where tα∈T is the reflection with normal α (The inversion formula ∣N(w)∣=ℓ(w), the root-reflection dictionary and strong exchange (1), Reflection length, the absolute order on a finite Coxeter group, and the moved and fixed spaces of an orthogonal operator, Carter's reflection-length formula, the absolute order on a finite Coxeter group, and moved-space rigidity under a common upper bound). Then:

(1) The basic identities. For every i≥1: (c−id)μi=−2ρi, μi⋅ρi=1, and μi∈F(R(ρi)c), i.e. R(ρi)c μi=μi; moreover F(R(ρi)c) is one dimensional and μi is its unique vector satisfying μi⋅ρi=1.

(2) Sign and vanishing identities. (a) μi⋅ρj=−μj+n⋅ρi for all i,j≥1; (b) μi⋅ρj≥0 whenever 1≤i≤j≤nh/2; (c) μi+t⋅ρi=0 for 1≤t≤n−1 and all i≥1; (d) μj⋅ρi≤0 whenever 1≤i<j≤nh/2.

(3) Separation from earlier cones. If 1≤i1<i2<⋯<im<k≤nh/2, then ρk is not a nonnegative linear combination of ρi1,…,ρim.

(4) Canonical simple systems of the subintervals. Fix σ≤Tc with σ≠1, put k:=ℓT(σ)=dim⁡M(σ) and write Pσ={τ1<τ2<⋯<τt} in the global ρ-order. Then:

(i) Pσ is the set of positive roots of the reflection subgroup Wσ:={w∈W:M(w)⊆M(σ)}, and it contains a simple system Δ={δ1,…,δk}: every root of Pσ is a nonnegative linear combination of the δ's and δ1,…,δk are linearly independent; moreover δk=τt and, recursively, δi is the last root of Pσ lying in M(σR(δk)R(δk−1)⋯R(δi+1)); equivalently δi is the first root of Pσ in M(R(δi−1)⋯R(δ1)σ), with the product empty for i=1, so in particular δ1=τ1.

(ii) εi:=R(δ1)R(δ2)⋯R(δi−1)δi is a positive root for each i, and

σ=R(εk)R(εk−1)⋯R(ε1),σ=R(εi) R(δ1)⋯R(δi−1)R(δi+1)⋯R(δk).

(iii) Let Sσ:=cone⁡{δ1,…,δk}∩S(M(σ)) be the spherical simplex, where S(M(σ))={x∈M(σ):B(x,x)=1}. Its closed spherical wall opposite δi is cone⁡{δj:j≠i}∩S(M(σ))=Sσ∩μ(εi)⊥, and its supporting hyperplane in M(σ) is M(σ)∩μ(εi)⊥.

(iv) If i<j and εi>εj in the global order, then εi⋅εj=0, so R(εi) and R(εj) commute; the reordering θ1<θ2<⋯<θk of ε1,…,εk in the global order satisfies σ=R(θk)R(θk−1)⋯R(θ1) and is lexicographically first among all increasing k-tuples η1<⋯<ηk in Pσ for which R(ηk)⋯R(η1)≤Tc and ℓT(R(ηk)⋯R(η1))=k.

(v) If ℓT(σ)=2 then {τ1,τt} is a simple system of Pσ, the only factorizations of σ as a product of two reflections in W are σ=R(τ1)R(τt)=R(τ2)R(τ1)=⋯=R(τt)R(τt−1), and τ1⋅τt≤0 while τi⋅τi+1≥0 for 1≤i<t; dually, for distinct positive roots ρi,ρj with R(ρi)R(ρj)≤Tc one has: if i<j then ρi⋅ρj≤0, and if i>j then ρi⋅ρj≥0.

(vi) Whenever τi1<⋯<τik is an increasing tuple of roots of Pσ for which R(τik)⋯R(τi1)≤Tc and ℓT(R(τik)⋯R(τi1))=k, one has τij≥θj for every j=1,…,k.

No Choice is used.

Facts & Assumptions

Given: The finite-type irreducible datum with ∣S∣=n≥2 and the bipartite data αi,si,Ri,βi,ρi,μi,a,b,c,h of The bipartite Coxeter element, its ordered prefix roots, and the conditional vector map mu(a) = -2(c-1)^{-1}a, the enumeration of The Coxeter plane, ordered-root enumeration, and invertibility of rho(c) - id, and an element σ≤Tc.

[F1]

Φ+={ρ1,…,ρnh/2} with the ρi pairwise distinct and ρi+n=Cρi, μi+n=Cμi for all i≥1, where C:=ρ(c); C−id is invertible, μ(ρi)=μi, and M(c)=V. Hence ℓT(c)=n. The Coxeter plane, ordered-root enumeration, and invertibility of rho(c) - id (1)-(4) Carter's reflection-length formula, the absolute order on a finite Coxeter group, and moved-space rigidity under a common upper bound (1)

[F2]

(C−id)μi=−2ρi for all i≥1, and μ is C-equivariant. For 1≤i≤n, μi=βi: each preceding reflection fixes βi by duality. The pairing and fixed-line assertions of (1) are derived in step 1.1 below. The Coxeter plane, ordered-root enumeration, and invertibility of rho(c) - id (4) The bipartite Coxeter element, its ordered prefix roots, and the conditional vector map mu(a) = -2(c-1)^{-1}a (3)-(4)

[F3]

B is positive definite, every root has B-norm 1, reflections act by rα(x)=x−2B(x,α)α, and B(Cx,Cy)=B(x,y). For each positive root α there is a unique reflection tα with ρ(tα)=rα; its moved space is Rα. The real Coxeter form, its radical, reflections, and form-preserving maps (3) Descent of the reflection representation, unit root norms, and conjugation of reflections (2),(3) The inversion formula ∣N(w)∣=ℓ(w), the root-reflection dictionary and strong exchange (1) Reflections: involutivity, form invariance, fixed hyperplane, and exact rank-two order (2)

[F4]

Positive roots have nonnegative simple-root coefficients, and B(f,α)>0 for every f∈C∘ and α∈Φ+. Root sign coherence and the action of simple reflections on positive roots (1),(2)

[F5]

Carter's formula gives ℓT(w)=dim⁡M(w); u≤Tv iff ℓT(v)=ℓT(u)+ℓT(u−1v); u≤Tv implies M(u)⊆M(v); if u,v≤Tc, then u≤Tv iff M(u)⊆M(v); and ℓT is invariant under conjugation and satisfies the triangle inequality. Carter's reflection-length formula, the absolute order on a finite Coxeter group, and moved-space rigidity under a common upper bound (1)-(3)

[F6]

On the positive-definite space (V,B), M(A)=F(A)⊥ for orthogonal A. For U⊆M(A) there is a unique orthogonal restriction AU≤OA with moved space U, and every line L is the moved space of the unique orthogonal reflection id−2ΠL. For group elements, orthogonal order and reflection order agree by Carter's formula. The Wall form of an orthogonal operator, subspace restriction, and the interval structure of the orthogonal reflection-length order (1),(3)-(5) Carter's reflection-length formula, the absolute order on a finite Coxeter group, and moved-space rigidity under a common upper bound (1),(2)

[F7]

In a reduced reflection factorization w=t1⋯tm, the prefix-conjugated root normals form a basis of M(w). Root normals inside the moved space, factorizations into reflections, and independent normals (3)

[F8]

Every nonidentity w has a reduced reflection factorization of length dim⁡M(w); the factorization lemma also supplies a root normal in M(w) for its induction step. Root normals inside the moved space, factorizations into reflections, and independent normals (1)-(3)

[F10]

For every nonzero point x∈gCI, its stabilizer is gWIg−1. In a finite Coxeter system the chambers are translates of the simplicial fundamental chamber, whose inward unit normals are its simple roots. The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere (1)-(3)

[F11]

For a canonical rank-two system with finite exponent m≥2, the simple-root Gram entry is −cos⁡(π/m) and the product of its two reflections is a rotation of exact order m, through an angle of magnitude 2π/m. Reflections: involutivity, form invariance, fixed hyperplane, and exact rank-two order (3)

[F12]

No finite family of proper linear subspaces of a finite-dimensional real vector space covers the whole space. A finite-dimensional vector space over an infinite field is not a finite union of proper subspaces

[F13]

For a reduced simple-generator expression w=s1⋯sm, every prefix-conjugated normal ρ(s1⋯si−1)esi is a positive root. The inversion formula ∣N(w)∣=ℓ(w), the root-reflection dictionary and strong exchange (2)

[F14]

(WI,I) is the Coxeter system of the restricted matrix, with intrinsic length equal to ambient length; every element of WI has a reduced expression using only letters of I. If t∈T and ℓ(tw)<ℓ(w), strong exchange expresses t as a prefix-conjugate of one letter of any reduced expression of w. Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (1)-(2) The inversion formula ∣N(w)∣=ℓ(w), the root-reflection dictionary and strong exchange (3)

Proof

technique · direct
1.1F1F2F3F5algebra

For every i≥1, [F2] gives (C−id)μi=−2ρi. Since C is an isometry and B(ρi,ρi)=1, B(μi,ρi)=1 follows by expanding B(Cμi,Cμi)=B(μi−2ρi,μi−2ρi). The same identity gives Cμi=μi−2ρi, so rρiCμi=μi and μi∈F(rρiC). For 1≤i≤n, the reflection word rρiC cancels to R1⋯Ri−1Ri+1⋯Rn, so its reflection length is at most n−1; the triangle inequality and ℓT(c)=n give the lower bound n−1. Thus its fixed space is one-dimensional. Since rρi+nC=C(rρiC)C−1, the same dimension holds for all i. The vector μi is nonzero because μi⋅ρi=1, and it is the unique vector in that line with this pairing. This proves (1).

1.2F1F2algebra

For all i,j≥1, μi⋅ρj=−μj+n⋅ρi. Indeed, ρi=12(μi−Cμi) by [F2], so −μj+n⋅ρi=−Cμj⋅12(μi−Cμi)=12(μj−Cμj)⋅μi=ρj⋅μi, using the isometry of C and [F1]-[F2]. This is (2)(a).

1.3F1F2F4algebra

Suppose 1≤i≤j≤nh/2. If i>n, then j>n and C-equivariance gives μi⋅ρj=μi−n⋅ρj−n. Repeating reduces to a first index at most n while keeping both indices positive and ordered. For i≤n, μi=βi, and βi⋅ρj is the coefficient of αi in the positive root ρj; this is nonnegative by [F4]. Thus (2)(b) holds.

1.4F1F3F5F6

Every reflection lies below c. Indeed, M(c)=V by [F1]. For a positive root α, the orthogonal reflection with moved line Rα is uniquely rα=ρ(tα) by [F3],[F6]; the Wall restriction for this line is below C=ρ(c) and has moved space Rα. The Wall dimension identity and Carter's formula therefore give tα≤Tc.

1.5F3F5algebra

We use two elementary consequences of absolute order. First, if w=r1⋯rm is a reduced reflection factorization and p<q, then rprq≤Tw: distinct root-reflections have product moved space the two-plane spanned by their distinct normal lines, so their product has reflection length 2 by Carter's formula. Write w=xrpyrqz; then (rprq)−1w=rqrpxrpyrqz=(rq(rpxrp)yrq)z, a product of m−2 reflections because conjugation preserves reflections. The triangle inequality forces this complement to have length m−2. Second, if u≤Tv≤Tw, then v−1w≤Tu−1w: write v=ux, w=vy with additive reflection lengths; then u−1w=xy, while y−1xy has the same length as x, so y≤Txy. These facts will be used below.

1.6F3F5F9F10F12

Put E=M(σ) and F=E⊥. Then Wσ={w:M(w)⊆E} is the pointwise stabilizer of F, because M(w)=F(w)⊥. If F≠0, choose x∈F outside {0} and every proper subspace F∩Hα; this is possible by [F9] and [F12]. By [F10], Stab⁡W(x)=gWIg−1 for some g,I. Each conjugate simple generator has a root hyperplane containing x, hence, by the choice of x, containing all of F; therefore every generator of this stabilizer fixes F pointwise. Conversely every element fixing F fixes x, so Wσ=gWIg−1. If F=0, take g=1 and I=S.

2.1F1F2F4step 1.3algebra

To prove (2)(c), first reduce i modulo n using C-equivariance, which preserves μi+t⋅ρi, and assume 1≤i≤n. If i+t≤n, then μi+t=βi+t and ρi=R1⋯Ri−1αi has no αi+t coefficient, so the pairing is zero. If i+t>n, put j=i+t−n, so 1≤j<i. By (2)(a), μi+t⋅ρi=μj+n⋅ρi=−μi⋅ρj=−βi⋅ρj=0, since ρj is supported on α1,…,αj. Now if 1≤i<j≤nh/2 and j<i+n, (2)(d) is (2)(c) with t=j−i; if j≥i+n, (2)(a) and (2)(b) give μj⋅ρi=−μi+n⋅ρj≤0. This proves (2)(c)-(d).

2.2F3F5F7F8step 1.4

For every σ≤Tc, one has Pσ=Φ+∩M(σ). If α∈Pσ, then M(tα)=Rα⊆M(σ) by [F5]. Conversely, if α∈Φ+∩M(σ), then tα≤Tc by step 1.4 and σ≤Tc, so moved-space rigidity in [F5] gives tα≤Tσ. Also Pσ spans M(σ): choose a reduced reflection factorization of σ; its prefix-conjugated normals are a basis of M(σ) by [F7], and the reflections with those normals have moved lines in M(σ), hence lie below σ by the same common-upper-bound argument. Taking the positive sign of each normal puts a spanning set in Pσ.

2.3F1F2F3F5F6step 1.1step 1.4step 1.5algebra

For any increasing tuple a1<⋯<am of positive roots, one has ℓT(R(a1)⋯R(am)c)=n−m if and only if μ(ai)⋅aj=0 for all i>j. If m=0, the left side is ℓT(c)=n by [F1], and the zero-pairing condition is vacuous; hence assume m≥1. Put ri=R(ai). The length equality is equivalent to the reverse product q=rm⋯r1 being a reduced element below c: its complement is q−1c=r1⋯rmc. In fact, if ℓT(q−1c)=n−m, then ℓT(q)≤m and n=ℓT(c)≤ℓT(q)+ℓT(q−1c)≤n, so both inequalities are equalities; the converse is the defining absolute-order equality. For the forward implication, the pair-product fact in step 1.5 gives rirj≤Tc whenever i>j. Since ℓT(ric)=n−1, this gives rj≤Tric from ℓT(rjric)=n−2; hence M(rj)⊆M(ric)=F(ric)⊥. The vector μ(ai) is a nonzero member of the one-dimensional fixed space F(ric), so μ(ai)⋅aj=0. Conversely, suppose all these pairings vanish. The matrix [μ(ai)⋅aj] is upper triangular with diagonal 1 by (1), so both the ai and the μ(ai) are linearly independent; in particular m≤n. Induct downward on i to prove qi:=rm⋯ri≤Tc with length m−i+1. The base qm=rm is step 1.4. If qi+1≤Tc, then each factor rj with j>i satisfies rj≤Tqi+1: writing a reduced factorization qi+1=xrjy, the product rjqi+1=(rjxrj)y uses one fewer reflections, and the triangle inequality makes that expression reduced. Put v=qi+1−1c. Complement order reversal from step 1.5 gives v≤Trjc, so μ(aj)∈F(rjc)⊆F(v) for every j>i. These m−i independent vectors form a basis of F(v), whose dimension is m−i by Carter's formula. The assumed zero pairings give ai∈F(v)⊥=M(v). The Wall restriction for the line Rai gives ri≤Tv; writing v=riz then gives c=qi+1riz, with lengths adding, so qi=qi+1ri≤Tc and ℓT(qi)=m−i+1. At i=1 this proves the claimed equivalence. The same argument applies to every subtuple because the vanishing conditions are inherited.

3.1step 1.1step 2.1algebra

If ρk=∑r=1marρir with ar≥0 and i1<⋯<im<k, then (2)(d) gives μk⋅ρir≤0 for every r, so 1=μk⋅ρk=∑rar(μk⋅ρir)≤0, a contradiction. This proves (3).

3.2F3F14step 2.2step 1.6

Let ΦI={ρ(u)αs:u∈WI,s∈I} be the intrinsic root system from [F14]; its representation is the restriction to VI=span⁡{αs:s∈I}, since the reflection formulas agree. An ambient reflection t∈T∩WI has a reduced I-expression by [F14]. Apply strong exchange to tt=1: it expresses t as a prefix-conjugate of a letter of that expression, so its root normal belongs to ±ΦI by [F3]. Conversely every intrinsic root gives an ambient reflection in WI. Conjugating by g, the root-reflection dictionary therefore identifies the roots of gWIg−1 with precisely the ambient roots whose reflections fix F pointwise, namely Φ∩E=±Pσ by step 2.2. Their span is both ρ(g)VI and E, since Pσ spans E.

4.1F3F4F10F14step 3.2

Choose f∈C∘ and project it orthogonally to E. Its pairing with every root of Pσ is positive by [F4], so it avoids the subsystem arrangement. Apply [F10] to the finite Coxeter system (WI,I) and transfer its chambers to E by ρ(g). The chamber containing the projection has inward unit normals Δ={ρ(gu)αs:s∈I} for some u∈WI. These are a basis of E, their reflections are the conjugates of the simple generators of WI, and their Gram matrix is the restricted Coxeter Gram matrix. In particular distinct normals have nonpositive pairings. By the root-sign theorem [F4] applied to this conjugate Coxeter system, its positive roots are exactly the roots positive on the projection, hence Pσ, and every such root is a nonnegative combination of Δ. This supplies the simple system and the Coxeter presentation used below.

4.2F1step 1.1step 2.1step 3.1algebra

In any such positive root subsystem with simple system Γ, its first root in the global order is a member of Γ. For if the first root η were not simple, write η=∑γ∈Γbγγ with bγ≥0; each γ is later than η, so (2)(d) gives μ(γ)⋅η≤0. Linearity of μ and (1) would give 1=μ(η)⋅η=∑bγ(μ(γ)⋅η)≤0, impossible. Also the last root of Pσ belongs to Δ: otherwise it is a nonnegative combination of the earlier simple roots, contrary to step 3.1.

5.1F5step 1.4step 1.6step 4.1step 4.2

We prove the recursive selection and the factorization σ=R(δ1)⋯R(δk) by induction on k. For k=1, Wσ has rank one, Pσ has its single positive root δ1, and σ=R(δ1). For k>1, order the simple roots increasingly; step 4.2 makes the last one δk=τt. Put r=R(δk). Since r≤Tσ, write σ=ru with ℓT(u)=k−1; then σ′:=σr=rur has length k−1. Write c=σv with ℓT(v)=n−k. The identity c=σ′(rv) and the bounds ℓT(rv)≤n−k+1 and n=ℓT(c)≤ℓT(σ′)+ℓT(rv) force ℓT(rv)=n−k+1, so σ′≤Tc. Also σ′ fixes F pointwise, hence M(σ′)⊆E.

6.1F1F2F4F5step 1.1step 1.3step 2.2step 5.1algebra

Let q be the global index with δk=ρq and put ν=Cμq=μq+n. For every ρj∈Pσ one has j≤q and, by (2)(a) and C-equivariance, ν⋅ρj=μq+n⋅ρj=−μj+n⋅ρq+n=−μj⋅ρq≤0 by (2)(b); at j=q this is −1. Since μq∈F(rc), conjugating by C gives ν∈F(cr); and ℓT(cr)=n−1, so F(cr)=Rν and M(cr)=ν⊥. Moreover σ′≤Tcr: its complement is σ′−1cr=rvr, of length n−k, while ℓT(cr)=n−1; the lengths add to n−1. Hence U:=M(σ′) is contained in E∩ν⊥, and both have dimension k−1 because ν⋅δk=−1. Thus U=E∩ν⊥. The roots Pσ′=Φ+∩U span U by step 2.2. Each is a nonnegative combination of Δ and is orthogonal to ν; since ν⋅δk=−1 and ν⋅δj≤0 for every j, every root in Pσ′ is a combination only of the δj for which ν⋅δj=0. Those zero-pairing simple roots must span the (k−1)-space U, so they are exactly δ1,…,δk−1. They form a simple system for Pσ′. Induction gives σ′=R(δ1)⋯R(δk−1) and proves the reverse selection at each rank. Therefore σ=R(δ1)⋯R(δk). For each i, its prefix pi:=R(δ1)⋯R(δi) and complementary suffix R(δi+1)⋯R(δk) multiply to σ and have at most i and k−i reflections, so both lengths attain these bounds. Thus M(pi), contained in span⁡(δ1,…,δi), has dimension i and equals that span. Since σR(δk)⋯R(δi+1)=pi, the induction shows that δi is the last root of Pσ in this subspace.

7.1F5step 4.2step 6.1algebra

The other recursive description follows by considering the suffix qi:=R(δi)⋯R(δk). The factorization in step 6.1 gives ℓT(qi)=k−i+1: its prefix and suffix factors together multiply to σ of length k, and their lengths are bounded by their numbers of reflections, whose sum is k. Writing pi:=R(δ1)⋯R(δi−1), the same length equality forces ℓT(pi)=i−1, so qi−1σ=qi−1piqi has length i−1 and qi≤Tσ. If c=σv as above, then qi−1c=qi−1(R(δ1)⋯R(δi−1))qiv has length at most (i−1)+(n−k)=n−ℓT(qi); the triangle inequality forces equality, so qi≤Tc. Its moved space is span⁡(δi,…,δk), since its factors fix the orthogonal complement of that span and its moved dimension is k−i+1. Thus Pqi=Pσ∩M(qi), and {δi,…,δk} is a simple system for this subsystem: a root in the tail span has zero coefficients on δ1,…,δi−1 in its nonnegative Δ-expansion. By step 4.2 the first root of Pqi is a simple root of this tail system; its first simple root is δi. Finally R(δi−1)⋯R(δ1)σ=qi by cancellation, so δi is the first root of Pσ in the moved space in (4)(i), and δ1=τ1. This proves (4)(i).

7.2F3F5F13step 4.1step 6.1algebra

Put Di:=R(δ1)⋯R(δi−1) and εi:=Diδi. The prefix R(δ1)⋯R(δi) has reflection length i by the factorization of σ and the triangle inequality, so this simple-generator word in the Coxeter system of Wσ is reduced. The root-inversion formula [F13], applied to that parabolic system, gives εi∈Pσ, hence it is a positive root. Conjugation gives R(εi)=DiR(δi)Di−1; multiplying these identities and cancelling adjacent inverse prefixes yields σ=R(εk)⋯R(ε1). Also R(εi)DiR(δi+1)⋯R(δk)=DiR(δi)R(δi+1)⋯R(δk)=σ. This proves (4)(ii).

8.1F3F5F11step 2.2step 3.1step 4.1step 6.1step 7.1algebra

Suppose ℓT(σ)=2 and Pσ={τ1<⋯<τt}. By (4)(i), Δ={τ1,τt} and σ=R(τ1)R(τt). Step 4.1 realizes this as a canonical rank-two system. If its exponent is m, [F11] gives simple-root angle π−π/m and a rotation of magnitude 2π/m. Write its generators as r,s and q=rs. The identities rqr=q−1 and s=rq reduce every word to qj or qjr, 0≤j<m; their distinct actions are the m rotations and m reflections in lines spaced by π/m. Every reflection is a conjugate of r or s: the conjugates give respectively q2jr and q2j−1r. The root-reflection dictionary thus gives t=m positive roots, equally spaced between the simple-root rays. The global order agrees with angular order: a decrease after τr would put τr+1 in the cone on earlier roots τ1,τr, contrary to step 3.1. A product of reflections has rotation angle twice the difference of its normal angles, modulo 2π; hence the two-reflection factorizations of σ are exactly R(τ1)R(τt)=R(τ2)R(τ1)=⋯=R(τt)R(τt−1). These exhaust factorizations in W: if σ=R(α)R(β), then M(σ)⊆span⁡(α,β), and both spaces have dimension 2, so the positive representatives of α,β lie in Pσ by step 2.2. The endpoint angle gives τ1⋅τt=−cos⁡(π/t)≤0, while each adjacent angle gives τi⋅τi+1=cos⁡(π/t)≥0.

8.2F2F3F5step 1.1step 7.2algebra

Fix i. The second factorization in (4)(ii) writes σ=R(εi)qi′ where qi′ is the product of the other k−1 simple reflections in Δ. Thus ℓT(qi′)=k−1, R(εi)≤Tσ, and qi′=R(εi)σ. Since c=σv with ℓT(v)=n−k, R(εi)c=qi′v is reduced, so qi′≤TR(εi)c. It follows that μ(εi)∈F(qi′). The moved space M(qi′) is exactly span⁡{δj:j≠i}: it is contained there because those are its reflection normals, and both dimensions are k−1. Hence μ(εi)⋅δj=0 for j≠i. Since εi−δi is a linear combination of δ1,…,δi−1, (1) gives 1=μ(εi)⋅εi=μ(εi)⋅δi. Thus the restrictions to E of the functionals B(μ(εi),−) form the dual basis to Δ. For x=∑jajδj with aj≥0, μ(εi)⋅x=ai; intersecting the cone with this zero hyperplane and with the unit sphere proves the wall equality, and the supporting hyperplane in E is E∩μ(εi)⊥. This proves (4)(iii).

9.1F3F5step 8.1

If distinct positive roots ρi,ρj satisfy R(ρi)R(ρj)≤Tc, their product has reflection length 2 and belongs to the rank-two case of step 8.1. Both roots lie in the corresponding Pσ by moved-space rigidity. If i<j, the only increasing-order two-factorization in step 8.1 is the endpoint factorization, so ρi⋅ρj≤0. If i>j, the factorization is one of the adjacent descending pairs, so ρi⋅ρj≥0. This proves (4)(v).

10.1F3step 4.1step 7.2step 1.5step 9.1algebra

If i<j and εi>εj, the factorization σ=R(εk)⋯R(ε1) is reduced, and the pair-product fact of step 1.5 gives R(εj)R(εi)≤Tσ≤Tc. The rank-two sign result of step 9.1 gives εi⋅εj≤0. On the other hand, since distinct simple roots have nonpositive pairings by step 4.1, applying R(δj−1),…,R(δi+1) successively to δj yields a nonnegative combination of δi+1,…,δj, and εi⋅εj=−δi⋅(R(δi+1)⋯R(δj−1)δj)≥0. Thus the pairing is zero, and the two reflections commute. Sorting the εi into global order uses only swaps of such inverted commuting pairs, so the product is unchanged and σ=R(θk)⋯R(θ1).

11.1F4F5step 8.2step 2.3step 2.1step 10.1∎

The tuple θ1<⋯<θk has reverse product σ≤Tc of length k, so it is among the tuples in (4)(iv). Let η1<⋯<ηk be any other such tuple. By step 2.3 every prefix η1<⋯<ηr also has reverse product below c of length r, so its r roots are linearly independent. For each s≥r, every root τ∈Pσ with τ<θr has μ(θs)⋅τ=0: its pairing is nonnegative because τ is a nonnegative combination of Δ and the restricted pairing functionals B(μ(εi),−)∣E are dual to Δ by step 8.2, while it is nonpositive by (2)(d). The restrictions to E of the k−r+1 functionals μ(θr),…,μ(θk) are independent, again by the dual-basis property. Their common kernel in E therefore has dimension r−1. If ηr<θr, the r independent roots η1,…,ηr all lie in that kernel, a contradiction. Hence ηr≥θr for every r, which proves componentwise domination (4)(vi) and the lexicographic minimality in (4)(iv). No Choice is used.

DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

The Brady-Watt ordered root complex X(c), its subcomplexes X(sigma) and X(sigma,rho), and their positive-cone realizations

Definition

Let (W,S) be an irreducible Coxeter system of finite type with S finite, n:=∣S∣≥1, and let αi, Ri, c, h, (ρi), (μi), μ, Φ+, ≤T, M and tα be as in The bipartite Coxeter element, its ordered prefix roots, and the conditional vector map mu(a) = -2(c-1)^{-1}a, The Coxeter plane, ordered-root enumeration, and invertibility of rho(c) - id and The mu-dot-root identities, the cone separation, and the canonical simple systems of the subintervals [1, sigma], so Φ+={ρ1<ρ2<⋯<ρnh/2} in the global order. Write R(α) for the reflection with normal α and Sn−1:={x∈V:B(x,x)=1}.

(1) The complex X(c). Its vertex set is Φ+. For 1≤i<j≤nh/2, join ρi to ρj by an edge exactly when R(ρj)R(ρi)≤Tc. Let X(c) contain the empty simplex and every finite nonempty set of vertices whose every two-element subset is an edge. Thus X(c) is the abstract simplicial complex (An abstract simplicial complex) determined by this ordered edge relation.

(2) The subcomplexes X(σ). For σ≤Tc, put Pσ:={α∈Φ+:tα≤Tσ} and let X(σ) be the full subcomplex of X(c) on the vertex set Pσ. For a positive root ρ in the global order, let X(σ,ρ) be the full subcomplex on vertices in Pσ∩M(σ) that are less than or equal to ρ; thus X(σ,τi) has vertex set {τ1,…,τi} when Pσ={τ1<⋯<τt}.

(3) Positive cones and realizations. Every vertex is a unit vector. For a finite set F of vertices define c[F]:={∑v∈Fλvv:λv≥0},c[∅]:={0}. For a subcomplex Y put c[Y]:=⋃F∈Yc[F] and ∣Y∣:=c[Y]∩Sn−1, its positive-cone realization in the unit sphere. For σ≤Tc and a positive root ρ, write Y(σ,ρ):=c[{τ∈Pσ∩M(σ):τ≤ρ}].

(4) Abstentions. This definition does not assert that c[F] is nondegenerate for each simplex F, that ∣F∣ is a spherical simplex, that the cone realization embeds X(c) or any X(σ), or that these realizations are convex or have dimension ℓT(σ)−1. It also does not assert an equivalence between higher simplex membership and a single full-tuple product condition. No Choice is used.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

The factorization criterion, linear independence of the faces, and the geometric simplicial structure of X(sigma)

Statement

With the notation of The Brady-Watt ordered root complex X(c), its subcomplexes X(sigma) and X(sigma,rho), and their positive-cone realizations and the conclusions of The mu-dot-root identities, the cone separation, and the canonical simple systems of the subintervals [1, sigma]:

(1) Factorization criterion. For any strictly increasing tuple a1<a2<⋯<ak of roots in Φ+, including the empty tuple when k=0, ℓT(R(a1)R(a2)⋯R(ak)c)=n−k  ⟺  μ(ai)⋅aj=0for every i>j.

(2) Linear independence and spherical simplices. If F={a1<⋯<ak} is a nonempty simplex of X(c), then a1,…,ak are linearly independent and lie in a common open halfspace, namely {x:B(x,f)>0} for every f∈C∘. Thus c[F] is a pointed simplicial cone and ∣F∣:=c[F]∩Sn−1 is a spherical simplex of dimension k−1. The empty face has c[∅]={0} and ∣∅∣=∅. For any increasing tuple of positive roots, its set is a simplex of X(c) if and only if its reverse product R(ak)⋯R(a1) lies below c in absolute order and has reflection length k.

(3) The complex structure and its dimension. For every σ≤Tc, the full subcomplex X(σ) is a finite simplicial complex of dimension ℓT(σ)−1; in particular X(1)={∅} has dimension −1. Each X(σ,ρ) is a simplicial complex. If Pσ={τ1<⋯<τt}, then X(σ,τi)⊆X(σ,τi+1)(1≤i<t), and the simplices of X(σ,τi+1) not already in X(σ,τi) are exactly the cones B∪{τi+1} over faces B of X(σ,τi) whose vertices all lie in μ(τi+1)⊥. The empty face is allowed as a base, giving the new singleton vertex.

(4) Geometric intersections are common faces. For any two faces F,F′ of X(σ), c[F]∩c[F′]=c[F∩F′]. Consequently, the normalized cone map from the ordinary geometric realization of X(σ) to Sn−1 is an embedding onto ∣X(σ)∣, and this image is a finite union of spherical simplices that pairwise meet in common faces. No Choice is used.

Facts & Assumptions

Given: An irreducible finite-type Coxeter system (W,S) with ∣S∣=n≥1, the bipartite Coxeter element c, its linear action CV=ρ(c), the ordered positive roots Φ+, the vectors μi and map μ of The bipartite Coxeter element, its ordered prefix roots, and the conditional vector map mu(a) = -2(c-1)^{-1}a, The Coxeter plane, ordered-root enumeration, and invertibility of rho(c) - id, and The mu-dot-root identities, the cone separation, and the canonical simple systems of the subintervals [1, sigma]. Let R(a) be the reflection with root normal a, and use the absolute order, moved spaces and positive-cone complexes of The Brady-Watt ordered root complex X(c), its subcomplexes X(sigma) and X(sigma,rho), and their positive-cone realizations.

[F1]

CV−idV is invertible, ρi+n=CVρi, and Φ+={ρ1,…,ρnh/2}. Hence M(c)=V. The Coxeter plane, ordered-root enumeration, and invertibility of rho(c) - id (3)-(4)

[F2]

The map Φ+→T, a↦ta, is a bijection; ρ(ta)=R(a), and distinct positive roots determine distinct reflections. The canonical reflection homomorphism, roots, reflections, and the positive cone (1)-(2) The inversion formula ∣N(w)∣=ℓ(w), the root-reflection dictionary and strong exchange (1)

[F3]

Since W is finite, B is positive definite and every ρ(w) is a B-isometry. Carter's formula gives ℓT(w)=dim⁡M(w)=n−dim⁡F(w) for every w. Absolute order is the partial order defined by reflection-length additivity; it has the triangle inequality and conjugation invariance, and u≤Tv implies M(u)⊆M(v) and F(v)⊆F(u). Reflection length, the absolute order on a finite Coxeter group, and the moved and fixed spaces of an orthogonal operator Carter's reflection-length formula, the absolute order on a finite Coxeter group, and moved-space rigidity under a common upper bound (1)-(2)

[F5]

Every subspace U⊆M(A) has an orthogonal restriction AU≤OA with moved space U, and every line is the moved space of a unique orthogonal reflection. Carter's formula transfers this restriction order to absolute order for group elements. The Wall form of an orthogonal operator, subspace restriction, and the interval structure of the orthogonal reflection-length order (3)-(4) Carter's reflection-length formula, the absolute order on a finite Coxeter group, and moved-space rigidity under a common upper bound (1)

[F6]

Writing a=ρi and using μ(ρi)=μi, one has μ(a)∈F(R(a)c), this fixed space is a line, and μ(a)⋅a=1. Also μi⋅ρj≥0 if i≤j, μi⋅ρj≤0 if i>j within the positive-root range, and μi+t⋅ρi=0 for 1≤t≤n−1. For n=1, CV=−id and μ=id, so R(α1)c=1 has the one-dimensional fixed space V and B(μ(α1),α1)=1; the strict-order sign conditions and the range 1≤t≤n−1 are empty. The Coxeter plane, ordered-root enumeration, and invertibility of rho(c) - id (4) The mu-dot-root identities, the cone separation, and the canonical simple systems of the subintervals [1, sigma] (1)-(2)

[F7]

Every root has B-norm 1; every positive root is a nonzero vector with nonnegative simple-root coordinates; and for every f∈C∘ and a∈Φ+, B(f,a)>0. Root sign coherence and the action of simple reflections on positive roots (1)-(2)

[F8]

For a root normal a of norm 1, R(a)(x)=x−2B(x,a)a; it fixes the codimension-one kernel of B(−,a) and negates a, so its determinant is −1. The real Coxeter form, its radical, reflections, and form-preserving maps (3)

[F9]

For n≥2 and σ≠1, Pσ is the positive-root set of the reflection subgroup Wσ and contains the simple system Δ={δ1,…,δk}. The roots εi=R(δ1)⋯R(δi−1)δi are positive, factor σ=R(εk)⋯R(ε1), and their increasing reordering θ1<⋯<θk has reverse product below c with reflection length k=ℓT(σ). The mu-dot-root identities, the cone separation, and the canonical simple systems of the subintervals [1, sigma] (4)(i)-(ii),(iv)

[F10]

X(c) has the ordered pairwise-edge definition, X(σ) and X(σ,ρ) are full subcomplexes with X(σ,τi) on vertices τ1,…,τi, and c[∅]={0}. The Brady-Watt ordered root complex X(c), its subcomplexes X(sigma) and X(sigma,rho), and their positive-cone realizations (1)-(3)

[F11]

An abstract simplicial complex contains the empty simplex and is closed under taking subsets; its geometric realization has the weak topology determined by its finite simplices. An abstract simplicial complex The geometric realization of an abstract simplicial complex

[F12]

A positive-definite Gram matrix with diagonal 1 defines a spherical simplex; for linearly independent unit vectors its cone section of the sphere is a spherical simplex of dimension one less than the number of vertices, and the radial normalization of the Euclidean simplex onto that section is a homeomorphism. Spherical Gram simplices and angular links of Euclidean faces Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas (i)-(ii)

[F13]

The vectors βs form the B-dual basis to the simple roots αs, so B(∑sβs,αt)=1 for every t∈S. The bipartite Coxeter element, its ordered prefix roots, and the conditional vector map mu(a) = -2(c-1)^{-1}a (3)

[F14]

A list is linearly independent exactly when its only vanishing linear combination has all coefficients zero; the empty set is a basis exactly in the zero space. Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis

[F17]

The chamber interior C∘ is the transfer, under v↦B(v,⋅), of the dual chamber interior. The finite reflection arrangement, its chambers, the spherical chamber complex, and the coset face poset

Proof

technique · derive the ordered-factorization test from absolute order and the fixed-space vectors, then use it to identify the faces, their dimensions, and the intersections of their positive cones
1.1F1F2F3F5F8

By [F1], M(c)=V and ℓT(c)=n. For every a∈Φ+, [F2] gives ta with ρ(ta)=R(a), and [F8] gives its moved line Ra. Apply the subspace-restriction theorem [F5] to this line inside M(c); its orthogonal restriction is the unique reflection with normal a, so Carter's formula gives ta≤Tc. Thus every positive-root reflection lies below c.

1.2F2F3F8

Let q=t1⋯tm be a reduced reflection factorization. Each factor tr lies below q: if q=xtry, then trq=(trxtr)y is a product of m−1 reflections, so the triangle inequality forces ℓT(trq)=m−1. If r<s, the product trts has reflection length 2 when tr≠ts: their canonical images are distinct involutions with distinct moved lines, so ρ(tr)ρ(ts)≠I; its determinant is +1, whereas every reflection has determinant −1. Thus trts is neither the identity nor a reflection, and its reflection length is 2. Write q=xtrytsz. Then (trts)−1q=tstrxtrytsz=(tstrxtrts)(tsyts)z, a product of m−2 reflections. The triangle inequality gives the reverse lower bound m−2, so trts≤Tq.

2.1F1F2F3F4F6F8step 1.1step 1.2

Let q:=R(ak)⋯R(a1). If ℓT(R(a1)⋯R(ak)c)=n−k, then ℓT(q)≤k and [F1], [F3] give n=ℓT(c)≤ℓT(q)+ℓT(q−1c)≤k+(n−k)=n. Thus ℓT(q)=k and q≤Tc, so the factorization of q is reduced. For i>j, step 1.2 gives R(ai)R(aj)≤Tq≤Tc. Since R(ai)≤Tc by step 1.1, ℓT(R(ai)c)=n−1; also ℓT(R(aj)R(ai)c)=n−2. Hence R(aj)≤TR(ai)c. By [F2] and [F8] the moved line of R(aj) is Raj; by [F3] and [F4] it lies in M(R(ai)c)=F(R(ai)c)⊥. The vector μ(ai) spans that fixed line by [F6], so μ(ai)⋅aj=0.

2.2F2F3F4F5F6F14step 1.2

Conversely, suppose μ(ai)⋅aj=0 for all i>j. The matrix D=(μ(ai)⋅aj)i,j=1k is upper triangular with diagonal 1 by [F6]; therefore both the roots ai and the vectors μ(ai) are linearly independent, so k≤n. For k=0 the conclusion is ℓT(c)=n by [F3], so assume k≥1. Define qk+1=1. Descending on i, assume qi+1:=R(ak)⋯R(ai+1)≤Tc with length k−i. Each factor R(aj), j>i, is below qi+1 by the first claim of step 1.2. Complements reverse order: if u≤Tv≤Tw, transitivity gives u≤Tw; writing v=ux and w=vy with additive reflection lengths then gives ℓT(xy)=ℓT(x)+ℓT(y), and conjugation invariance gives ℓT(y−1xy)=ℓT(x), hence y=v−1w≤Tu−1w=xy. Put v:=qi+1−1c. For every j>i, complement reversal gives v≤TR(aj)c, and [F6] puts μ(aj) in F(R(aj)c)⊆F(v). These k−i independent vectors form a basis of F(v): Carter's formula gives dim⁡F(v)=n−ℓT(v)=n−(n−k+i)=k−i. The assumed zero pairings put ai in F(v)⊥=M(v) by [F4]. Restricting ρ(v) to the line Rai gives the orthogonal reflection R(ai)=ρ(tai) by [F2]; the restriction theorem [F5] and Carter's formula therefore give R(ai)≤Tv. Write v=R(ai)z with ℓT(v)=1+ℓT(z). Then c=qi+1R(ai)z, whose displayed k−i+1+ℓT(z)=n reflection factors force the factorization to be reduced; consequently qi:=qi+1R(ai)≤Tc and ℓT(qi)=k−i+1. At i=1 this yields ℓT(q)=k and ℓT(q−1c)=n−k. This proves (1).

3.1F2F3F6F10F14step 1.2step 2.1step 2.2

For i<j, the two-root instance of (1) says R(aj)R(ai)≤Tc⟺μ(aj)⋅ai=0, since the product of two distinct positive-root reflections has length 2 by step 1.2. If F={a1<⋯<ak} is a simplex, every pair is an edge by [F10], so these pairwise equivalences make D=(μ(ai)⋅aj) upper triangular with diagonal 1. Pairing a vanishing combination ∑jλjaj=0 with each μ(ai) gives Dλ=0; hence every λj=0. Thus the vertices of every nonempty face are linearly independent. Conversely, if the reverse product of an increasing tuple lies below c and has length k, step 1.2 applied to its reduced factorization shows each pair product is below c, so the tuple is a simplex. The empty tuple is the empty simplex by [F10].

4.1F3F7F10F12F13F17step 3.1

Let f0:=∑s∈Sβs, with the dual vectors from [F13]. Then B(f0,αs)=1 for every simple root; since each positive root is a nonzero nonnegative combination of simple roots by [F7], every positive root has positive pairing with f0. Also [F7] gives positive pairing with every f∈C∘ by the chamber transfer [F17]. For a nonempty face F, its independent unit roots have a positive-definite Gram matrix with diagonal 1. By [F12], c[F]∩Sn−1 is the associated spherical simplex of dimension ∣F∣−1. The independence of the cone generators makes c[F] pointed and simplicial. For the empty face, [F10] gives c[∅]={0} and its sphere section is empty.

4.2F1F2F3F8F9F10step 3.1

The roots of Pσ lie in M(σ): if a∈Pσ, then ta≤Tσ by definition; [F2] identifies its linear reflection, [F8] gives M(ta)=Ra, and [F3] gives M(ta)⊆M(σ). Thus a face of X(σ) has at most dim⁡M(σ)=ℓT(σ) vertices by step 3.1 and Carter's formula. If σ=1, then Pσ=∅ and X(1)={∅} has dimension −1. If n=1 and σ≠1, the rank-one data give W={1,c}, σ=c, and Pσ={α1}; hence X(σ) has one vertex and dimension 0=ℓT(σ)−1. If n≥2 and σ≠1, [F9] gives Δ={δ1,…,δk}⊆Pσ and εi=R(δ1)⋯R(δi−1)δi. Each R(δj) lies in the reflection subgroup Wσ of [F9], so every εi is a root of that subgroup; its positivity from [F9] puts it in Pσ. Hence the increasing reordering θ1<⋯<θk lies in Pσ. Its reverse product is below c with length k=ℓT(σ) by [F9], so step 3.1 makes it a k-vertex simplex. Therefore dim⁡X(σ)=k−1. Finiteness follows from finiteness of Φ+ in [F1], and the full-subcomplex and X(σ,ρ) claims follow from [F10].

4.3F6F10step 3.1

Let Ki:=X(σ,τi). By [F10], Ki has vertices τ1,…,τi. Any new simplex of Ki+1 must contain the new vertex τi+1. Its other vertices form a face B of Ki, and the two-root criterion of step 3.1 says each such vertex b is joined to τi+1 exactly when μ(τi+1)⋅b=0. Conversely, any face B of Ki with all vertices in this hyperplane gives a simplex B∪{τi+1}. This includes B=∅, proving the cone-over-link description and the nested inclusions.

5.1F6F10step 4.3

Put K0:={∅} and induct on i to prove the cone intersection formula for all faces of Ki. At i=0 both cones equal {0}. Suppose the formula holds at i and consider faces of Ki+1. If both are in Ki, use induction. Otherwise each new face has the form B∪{τi+1} with B∈Ki and every vertex of B orthogonal to μ(τi+1), by step 4.3. For a cone point in such a face, its coefficient on τi+1 is its pairing with μ(τi+1), because μ(τi+1)⋅τi+1=1 by [F6] and its pairings with the base vertices are zero. Every old vertex τj, j≤i, has μ(τi+1)⋅τj≤0 by [F6]. Therefore a cone on an old face intersects a cone with apex τi+1 only where the apex coefficient is zero; there the induction hypothesis identifies the intersection with the cone on the common base face. For two faces both containing the apex, equality of a common cone point gives equality of its apex coefficients after pairing with μ(τi+1), and then equality of the base cone points; induction identifies their base intersection. In each case the intersection is exactly the cone on the common face. Since every face of X(σ) belongs to Kt, this proves the formula in (4).

6.1F1F10F11F12F15F16step 4.1step 4.2step 5.1∎

Define the normalized cone map on a barycentric point of the geometric realization by ι((λv)v∈V(F)):=∑vλvv∥∑vλvv∥B,λv≥0,∑vλv=1. The denominator is nonzero because B(f0,v)>0 for every positive root by step 4.1. Its restriction to each simplex is a homeomorphism onto the corresponding spherical simplex by [F12], and it is continuous globally by the weak-topology definition [F11]. If two such images agree, the two positive combinations lie on the same ray; step 5.1 puts that ray in the cone on the common face, and linear independence of that face plus the barycentric sum-one condition makes the original points equal. Thus ι is a continuous bijection onto ∣X(σ)∣. By [F1] and step 4.2, X(σ) is a finite abstract simplicial complex, so its ordinary realization is compact by [F15]. If A is closed in that realization, [F15] makes A compact; the open-cover argument in [F15] makes ι[A] compact, and it is closed in the Hausdorff sphere by [F15] and [F16]. Thus ι is a closed continuous bijection onto its image and therefore a topological embedding. No Choice is used: the only compactness input is [F15], whose finite-complex proof reduces to finite-dimensional Heine-Borel.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

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

Statement

With the notation of The Brady-Watt ordered root complex X(c), its subcomplexes X(sigma) and X(sigma,rho), and their positive-cone realizations, The Coxeter plane, ordered-root enumeration, and invertibility of rho(c) - id and The mu-dot-root identities, the cone separation, and the canonical simple systems of the subintervals [1, sigma], fix σ≤Tc, σ≠1, put k=ℓT(σ), and write Pσ={τ1<⋯<τt}. If n=1, set Pσ={τ1} and θ1=τ1; if n≥2, write θ1<⋯<θk as in (4)(iv) of The mu-dot-root identities, the cone separation, and the canonical simple systems of the subintervals [1, sigma]. For τ∈Pσ define μ(τ)±:={x∈V: ±B(x,μ(τ))≥0},c[Pσ]:={∑τ∈Pσλττ:λτ≥0}. For θk≤τi≤τt put Z(σ,τi):=M(σ)∩⋂j=1kμ(θj)+∩⋂j=i+1tμ(τj)−. Then:

(1) The separating-root lemma. If τa,τs∈Pσ satisfy τa≥θk, τs<τa, τs∉{θ1,…,θk} and B(τa,μ(τs))=0, there are τb,τc∈Pσ with τb,τc<τa, B(τb,μ(τa))=B(τc,μ(τa))=0, and B(τb,μ(τs))>0>B(τc,μ(τs)).

(2) The facet induction. For every index i with θk≤τi≤τt, c[X(σ,τi)]=Y(σ,τi)=Z(σ,τi). The cone is full-dimensional in M(σ), closed and convex. Every facet is contained in one of the hyperplanes M(σ)∩μ(θj)⊥ (1≤j≤k) or M(σ)∩μ(τj)⊥ (j>i). Some listed halfspaces may be redundant; only nonredundant active inequalities support facets. This includes rank one and the empty base at the start of the rank induction.

(3) Spherical convexity and intersection. ∣X(σ)∣=Sn−1∩c[X(σ)]=Sn−1∩M(σ)∩⋂j=1kμ(θj)+=Sn−1∩c[Pσ]. This set is spherically convex: the shorter great-circle arc between any two of its points lies in it. For α,β≤Tc, ∣X(α)∩X(β)∣=∣X(α)∣∩∣X(β)∣, using the common-face cone intersections of The factorization criterion, linear independence of the faces, and the geometric simplicial structure of X(sigma) (4).

(4) Limits. This theorem asserts nothing about M(α)∩M(β) for arbitrary α,β≤Tc, the lattice property of [1,c], or X(σ) for σ̸≤Tc. No Choice is used.

Facts & Assumptions

Given: The irreducible finite-type Coxeter system and the bipartite data of The bipartite Coxeter element, its ordered prefix roots, and the conditional vector map mu(a) = -2(c-1)^{-1}a, The Coxeter plane, ordered-root enumeration, and invertibility of rho(c) - id and The mu-dot-root identities, the cone separation, and the canonical simple systems of the subintervals [1, sigma], together with σ≤Tc, σ≠1, k=ℓT(σ) and Pσ={τ1<⋯<τt}.

[F1]

The conditional map μ(v)=−2(C−id)−1v=2(id−C)−1v is defined, C=ρ(c) is a B-isometry, ρi enumerate Φ+ in the global order, and μ(ρi)=μi. The bipartite Coxeter element, its ordered prefix roots, and the conditional vector map mu(a) = -2(c-1)^{-1}a The Coxeter plane, ordered-root enumeration, and invertibility of rho(c) - id

[F2]

For each positive root a, μ(a)∈F(R(a)c), B(μ(a),a)=1, and for positive roots a<b in the global order, B(μ(a),b)≥0 while B(μ(b),a)≤0. The Coxeter plane, ordered-root enumeration, and invertibility of rho(c) - id The mu-dot-root identities, the cone separation, and the canonical simple systems of the subintervals [1, sigma]

[F3]

Wσ={w:M(w)⊆M(σ)} is the finite reflection subgroup whose positive roots are Pσ. Since M(tα)=Rα, this gives Pσ=Φ+∩M(σ). For n≥2 it has a simple system Δ={δ1,…,δk}, every root in Pσ is a nonnegative combination of Δ, and the reordered roots θ1<⋯<θk give a reduced factorization σ=R(θk)⋯R(θ1). The prefix roots ϵj=R(δ1)⋯R(δj−1)δj are positive. The mu-dot-root identities, the cone separation, and the canonical simple systems of the subintervals [1, sigma] (4)(i)-(iv) The inversion formula ∣N(w)∣=ℓ(w), the root-reflection dictionary and strong exchange (1)

[F4]

The inversion set is N(w)={α∈Φ+:wα∈Φ−}. For a reduced expression w=s1⋯sm, its prefix roots s1⋯si−1αsi are exactly N(w−1), and are pairwise distinct positive roots. The geometric inversion set N(w) of an element of a Coxeter group The inversion formula ∣N(w)∣=ℓ(w), the root-reflection dictionary and strong exchange (2)

[F5]

ℓT(w)=dim⁡M(w); absolute order is the reflection-length order; it has the triangle inequality and conjugation invariance; and if u,v≤Tc, then u≤Tv exactly when M(u)⊆M(v). Reflection length, the absolute order on a finite Coxeter group, and the moved and fixed spaces of an orthogonal operator Carter's reflection-length formula, the absolute order on a finite Coxeter group, and moved-space rigidity under a common upper bound (1)-(3)

[F6]

For orthogonal A, M(A)=F(A)⊥. Every subspace U⊆M(A) has an orthogonal restriction with moved space U, and for group elements Carter's formula transfers this restriction order to absolute order. The Wall form of an orthogonal operator, subspace restriction, and the interval structure of the orthogonal reflection-length order (1),(3)-(5) Carter's reflection-length formula, the absolute order on a finite Coxeter group, and moved-space rigidity under a common upper bound

[F7]

For an increasing root tuple a1<⋯<am, its set is a simplex of X(c) exactly when the reverse product R(am)⋯R(a1) lies below c and has reflection length m; every face has independent vertices, and all positive-root vertices lie in a common open halfspace. If Pσ={τ1<⋯<τt}, the prefix complexes are nested and each new simplex at τi+1 is a cone over a face in μ(τi+1)⊥. The factorization criterion, linear independence of the faces, and the geometric simplicial structure of X(sigma) (1)-(3)

[F8]

The ordered complex, its full subcomplexes, cones, and inclusive root prefixes have the definitions of The Brady-Watt ordered root complex X(c), its subcomplexes X(sigma) and X(sigma,rho), and their positive-cone realizations (1)-(3). In particular X(σ,τi) contains precisely the vertices τ1,…,τi.

[F9]

The root-reflection map a↦ta is a bijection from positive roots to reflections; distinct positive roots give distinct reflecting involutions; R(a)x=x−2B(x,a)a has determinant −1 and moved line Ra for unit roots; reflections act on roots by their orthogonal root action; and positive roots have norm one. The inversion formula ∣N(w)∣=ℓ(w), the root-reflection dictionary and strong exchange (1) The real Coxeter form, its radical, reflections, and form-preserving maps (3) Root sign coherence and the action of simple reflections on positive roots

[F10]

If ℓT(u)=2 and Pu={τ1<⋯<τt}, then {τ1,τt} is a simple system of Pu (so every root in Pu is a nonnegative combination of these endpoints), u=R(τ1)R(τt)=R(τ2)R(τ1)=⋯=R(τt)R(τt−1), and B(τ1,τt)≤0. The mu-dot-root identities, the cone separation, and the canonical simple systems of the subintervals [1, sigma] (4)(i),(v)

[F11]

A nonempty simplex cone in X(σ) is pointed and its normalized map is an embedding; cones of two faces intersect in the cone on their common face. The factorization criterion, linear independence of the faces, and the geometric simplicial structure of X(sigma) (2),(4)

[F12]

A finite abstract simplicial complex is closed under taking subsets; an empty face is permitted and has dimension −1. An abstract simplicial complex

[F13]

For a linear map between finite-dimensional vector spaces, dim⁡ker⁡f+dim⁡im⁡f=dim⁡V. Rank-nullity: dim⁡FV=nullity⁡T+rank⁡T

[F14]

A finite-dimensional real inner-product space has induced norm ∥v∥=B(v,v). Real and complex inner-product spaces and their induced length

[F15]

The simple roots are a basis, and the positive roots are exactly the roots with nonnegative simple-root coordinates (the negative roots have nonpositive coordinates). Root sign coherence and the action of simple reflections on positive roots (1)-(2)

Proof

technique · first identify the roots inverted by each interval element; then prove the separating-root statement; finally use a nested rank and root-index induction, transporting each facet normal across the new apex
1.1F3F4

Inversion inside a subinterval. If n=1, (1) is vacuous because Pσ has only its single positive root. Assume n≥2. Fix u≤Tc, u≠1, and let Δu={d1,…,dm} be the simple system of Pu given by [F3]. The item-18 factorization, in its second form with index 1, is u=R(d1)⋯R(dm); it is reduced because ℓT(u)=m. Apply the inversion formula [F4] to the finite Coxeter system Wu with simple system Δu. Its positive roots are exactly Pu, so {α∈Pu:u−1α∈−Pu}={ε1,…,εm}={θ1,…,θm}, where the prefix roots are εj=R(d1)⋯R(dj−1)dj. 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 α∈Pu∖{θ1,…,θm}, u−1α∈Pu.

1.2F2F3F5F6F7F9F10F15

The first separator. Write s=R(τs) and a=R(τa). Since B(μ(τs),τa)=0, [F2] and [F6] give τa∈M(sc) and hence a≤Tsc. The distinct reflections s,a have product determinant +1 and nonidentity image, whereas every reflection has determinant −1; hence ℓT(sa)=2. Writing sc=az gives c=saz with 2+ℓT(z)=ℓT(c), so sa≤Tc. Its moved space is contained in M(σ) because both normals lie there, hence [F5] gives sa≤Tσ. The rank-two statement [F10] applied to sa shows that τs and τa are the ordered endpoints of the simple system of Psa. Put τb:=R(τa)τs=τs−2B(τs,τa)τ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(τa) preserves M(sa), so τb∈Psa. The endpoints are the least and greatest roots of Psa, hence τs≤τb≤τa; equality τb=τa would imply τs=−τa, so τb<τa. Thus τb∈Pσ as sa≤Tσ. The pair (τb,τa) has reverse product R(τa)R(τb)=sa≤Tc of length 2, so [F7] gives B(μ(τa),τb)=0. Also B(μ(τs),τb)=B(μ(τs),τs−2B(τs,τa)τa)=1>0.

1.3F1F2F14

The linear map and finite facet test. Regard C=ρ(c) as an orthogonal operator. Since C−I is invertible, μ=2(I−C)−1 and μ+μ∗=2(I−C)−1+2(I−C−1)−1=2I, because (I−C−1)−1=−(I−C)−1C. Thus for every unit root x, B(μ(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≥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.

1.4F1F2F3F7F8F9F12

The inclusions and rank base. The root-reflection dictionary and the definition of Wσ give Pσ=Φ+∩M(σ). For n≥2, the wall statement (4)(iii) of item 18 and B(μ(ϵj),ϵj)=1 from [F2] show that μ(ϵj)⋅δl=1 for l=j and 0 otherwise: the wall makes the off-diagonal pairings zero, and ϵj−δj is a combination of earlier simple roots. Thus the restrictions B(μ(ϵj),−)∣M(σ) form the basis dual to Δ. Since the θj are a reordering of the ϵj, the restricted pairing functionals B(μ(θj),−)∣M(σ) are this same dual basis in a different order. Therefore [F3] gives B(μ(θj),τ)≥0 for every τ∈Pσ. For n=1 the same inequalities follow directly from Pσ={θ1}. If τ≤τi and j>i, then τ<τj, so [F2] gives B(μ(τj),τ)≤0. Consequently Y(σ,τi)⊆Z(σ,τi); by definition c[X(σ,τi)]⊆Y(σ,τi). If k=1, then Pσ={θ1}: it is the positive root set on the one-dimensional space M(σ), and unit normalization leaves one positive root. The only eligible prefix is the singleton, c[X(σ,θ1)]=R≥0θ1=M(σ)∩μ(θ1)+, whose sole facet is the origin in μ(θ1)⊥; this includes the empty base X(1)={∅} with cone {0}. Suppose henceforth k≥2, and let i0 be the unique index with τi0=θk.

2.1F1F2F3F4F5F6F7F9

The opposite separator. Set τc:=σ−1τs. By [F1], τs∈Pσ; the hypothesis excludes the inversion roots in [F3], so [F4] and step 1.1 imply τc∈Pσ. Put t:=R(τs) and u:=tσ. Write σ=tu0 with additive reflection lengths, so u=u0 and u0−1σ=u0−1tu0 has length 1; hence u≤Tσ. If c=σv is reduced, then tc=u0v and ℓT(tc)=n−1=ℓT(u0)+ℓT(v) because t≤Tσ≤Tc, so also u≤Ttc. The vector μ(τs) is fixed by tc by [F2], hence by u using [F5]-[F6]. Let p be the orthogonal projection of μ(τs) onto M(σ). Its residual lies in F(σ)⊆F(u), so p∈F(u) as well; projection preserves its pairing with τs∈M(σ), giving B(p,τs)=1. Therefore σp=tp=p−2τs. Since στc=τs and σ is an isometry, B(μ(τs),τc)=B(p,τc)=B(σp,τs)=B(p−2τs,τs)=−1. By [F2], if τs<τc then this pairing is nonnegative, and equality of the roots would give 1; thus τc<τs<τa. Since sσ=σR(τc) and sa≤Tσ, one has a≤Tsσ=σR(τc). Write sσ=az with ℓT(z)=k−2. Then σ=azR(τc) and (aR(τc))−1σ=R(τc)zR(τc) has length k−2 by conjugation invariance. The distinct reflections a and R(τc) have product of determinant +1 and this product is nonidentity, so its reflection length is 2; the length equality therefore gives aR(τc)≤Tσ≤Tc. Now [F7] gives B(μ(τa),τc)=0. Together with step 1.2 this proves (1).

2.2F2F3F5F7

Base of the root-index induction. Put σ0:=R(θk)σ=R(θk−1)⋯R(θ1). The prefix {θ1,…,θk−1} is a face of the canonical k-simplex by [F7], so σ0≤Tc and ℓT(σ0)=k−1. The tuple θ1<⋯<θk−1 is eligible for σ0, so [F3]'s componentwise minimality makes its canonical tuple θ1′<⋯<θk−1′ satisfy θj′≤θj for every j. In particular θk−1′<θk, and appending θk to this tuple gives an increasing reduced tuple for σ; componentwise minimality for σ gives θj≤θj′ for j<k. Thus θj′=θj for every j<k. Also M(σ0)=span⁡(θ1,…,θk−1). The dual-basis result of step 1.4 makes B(μ(θk),τ)≥0 for every τ∈Pσ, while root order makes this pairing nonpositive when τ<θk by [F2]; hence every such τ lies in M(σ)∩μ(θk)⊥. This hyperplane has dimension k−1 and contains the independent roots θ1,…,θk−1, so M(σ0)=M(σ)∩μ(θk)⊥. Since θk−1<θk=τi0, the prefix ending at τi0−1 is eligible for σ0. Every τj<θk has B(μ(θk),τj)≥0 by the dual-basis result above and ≤0 by the global order, so these earlier roots lie in M(σ0)=M(σ)∩μ(θk)⊥. Conversely Pσ0⊆Pσ by [F3]. Thus the two prefix vertex sets, and hence their full subcomplexes, agree: F0:=X(σ,τi0−1)=X(σ0,τi0−1). The lower-rank induction gives c[F0]=Z(σ0,τi0−1), a full-dimensional convex cone in L0:=M(σ0) with facet supports restricted from μ(b)⊥ for roots b∈Pσ0.

2.3F1F3F5F6F9F14step 1.3

Transporting the base facets through an apex. The following calculation applies both to the base apex a=θk and to an inductive apex a=τi+1. Let L=M(σ)∩μ(a)⊥=M(R(a)σ), let F be the already established full-dimensional base cone in L, and let a facet of F have support the restriction of μ(b)⊥ for some b∈PR(a)σ⊆L. Put E:=M(σ) and Va:=F+R≥0a. For x∈E, the decomposition x=y+ta, with t=B(x,μ(a)) and y∈L, is unique. Thus x∈Va exactly when t≥0 and y∈F. If a facet of F is given by εB(y,μ(b))≥0 with ε∈{1,−1}, its transported inequality is εB(x,ν)≥0, where ν:=μ(b)−B(μ(b),a)μ(a); it vanishes at a and agrees with μ(b) on L. Since B(μ(a),b)=0 and μ+μ∗=2I, B(μ(b),a)=2B(b,a), so ν=μ(b−2B(b,a)a)=μ(R(a)b). The equality of F with the intersection of its active facet halfspaces therefore gives a finite halfspace presentation of Va in E by B(x,μ(a))≥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(σ), so its positive representative r belongs to Pσ by [F3]. Thus every non-base facet of Va is a root-wall facet.

2.4F1F2F3F5F6F7F9F10F13F15step 1.1

Inductive root-prefix step. Suppose i≥i0 and Ki:=c[X(σ,τi)]=Z(σ,τi). Put a:=τi+1 and σ′:=R(a)σ. Since R(a)≤Tσ≤Tc, write c=σv with ℓT(v)=n−k and σ=R(a)σ′. Then R(a)c=σ′v; also ℓT(R(a)c)=n−1, since R(a)≤Tc, so σ′≤TR(a)c≤Tc and ℓT(σ′)=k−1. The subspace M(σ′) lies in M(σ) because σ and R(a) preserve M(σ), and it lies in M(R(a)c)=μ(a)⊥ by absolute-order monotonicity. Both M(σ′) and M(σ)∩μ(a)⊥ have dimension k−1: the latter is the kernel of the nonzero functional x↦B(x,μ(a)) on M(σ), which is nonzero on a∈M(σ) since B(a,μ(a))=1. Hence M(σ′)=M(σ)∩μ(a)⊥ and Pσ′=Pσ∩μ(a)⊥. The link base F on the old vertices orthogonal to μ(a) satisfies c[F]=Ki∩μ(a)⊥: all old vertices have nonpositive pairing with μ(a), so a nonnegative combination pairs to zero exactly when it uses only zero-pairing vertices. Thus F=X(σ′,τi). Let ϵ1′,…,ϵk−1′ be the prefix roots for the canonical simple system of σ′. They lie in M(σ′), so B(μ(a),ϵj′)=0. If ϵj′>a, the distinct reflections R(a) and R(ϵj′) have product length 2 by the determinant argument in [F9]. Since R(ϵj′)≤TR(a)c, write R(a)c=R(ϵj′)v with ℓT(v)=n−2; then c=R(a)R(ϵj′)v is reduced, so R(a)R(ϵj′)≤Tc. By [F10] and the increasing order a<ϵj′, this is the endpoint factorization of the rank-two element w:=R(a)R(ϵj′), so B(a,ϵj′)≤0. The root d:=R(a)ϵj′=ϵj′−2B(ϵj′,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 Pw; it cannot equal a, since that would imply ϵj′=R(a)a=−a. Thus a<d in the global order. Since a,ϵj′∈M(σ) and R(a) preserves M(σ), this positive root lies in Pσ=Φ+∩M(σ). Now σ′−1ϵj′=σ−1d is negative by step 1.1 applied to σ′, so step 1.1 applied to σ gives d∈{θ1,…,θk}, contradicting d>a≥θk. Hence every ϵj′<a, and therefore θk−1′≤τi. Let b be the last root of Pσ′ at or below τi; it exists since θk−1′ is such a root, and b≥θk−1′. Then F=X(σ′,τi)=X(σ′,b), so lower-rank induction gives c[F]=Z(σ′,b), full-dimensional and convex in L=M(σ′).

3.1F2F3F7step 2.1step 1.3step 1.4step 2.3

Initial cone and its facets. Let Ki0:=c[X(σ,θk)]. By [F7], Ki0=c[F0]+R≥0θk, so it is a full-dimensional convex cone. The base support is μ(θk)⊥; each other facet has support μ(r)⊥ for a positive root r∈Pσ by step 2.3. It contains the apex, so B(μ(r),θk)=0. If r<θk and r∉{θ1,…,θk}, step 2.1 gives two roots of F0 on opposite sides of μ(r)⊥, contradicting that it supports the cone. Hence every side facet is labelled by a θj or a root r>θk. The θj inequalities have positive sign on Ki0 by [F3], the base apex inequality is positive on θk and zero on F0, and each later-root inequality is nonpositive on all vertices of the prefix. The finite facet test of step 1.3 therefore gives Z(σ,θk)⊆Ki0. With the reverse inclusion from step 1.4, equality holds at i0; the same facet argument records that any other listed halfspace not defining one of these facets is redundant.

3.2F2F3F6F7step 2.1step 1.3step 1.4step 2.3step 2.4

The new prefix is X(σ,τi+1)=X(σ,τi)∪(a∗F) by [F7], so its cone is Ki+1=Ki∪Va with Va=c[F]+R≥0a. Apply step 2.3 to each facet of F; every facet of Va is supported by μ(a)⊥ or by μ(r)⊥ for r∈Pσ. Each side facet contains a, so B(μ(r),a)=0. If r<a and r is not a θ-root, step 2.1 produces two vertices of F on opposite sides of μ(r)⊥, contradicting support. Thus every facet label is a θj, a, or a root r>a. Its containing halfspace is respectively μ(θj)+, μ(a)+, or μ(r)−, by the sign inequalities in [F2]-[F3]. The cone Z(σ,τi+1)∩μ(a)+ satisfies all these facet halfspaces; step 1.3 therefore puts it in Va. Its other half Z(σ,τi+1)∩μ(a)− equals Z(σ,τi)=Ki. Consequently Z(σ,τi+1)⊆Ki+1. The reverse containment follows from step 1.4, proving Ki+1=Z(σ,τi+1). The active-facet list is a subset of the defining inequalities; any omitted or repeated inequality is recorded as redundant.

4.1F7step 1.4step 3.1step 3.2

Endpoint. The induction ends at i=t, where Y(σ,τt)=c[Pσ]. Thus the endpoint equality gives both the full positive-root cone and the claimed intersection with M(σ) and the μ(θj)+ halfspaces.

5.1F7F14step 4.1

Spherical convexity. The cone Z(σ,τ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 ϕ=arccos⁡B(x,y)<π. If ϕ=0 the arc is constant. Otherwise put e=(y−cos⁡ϕ x)/sin⁡ϕ, so B(e,x)=0 and B(e,e)=1. The shorter great-circle arc is γ(s)=cos⁡(s)x+sin⁡(s)e=sin⁡(ϕ−s)sin⁡ϕx+sin⁡ssin⁡ϕy for 0≤s≤ϕ. Its coefficients are nonnegative, so γ(s) lies in the convex cone and has unit norm. This proves spherical convexity.

6.1F11F12step 4.1∎

Since X(α) and X(β) 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(α)] and c[X(β)], it lies in cones c[F] and c[F′] for faces in the respective subcomplexes; [F11] identifies their intersection with c[F∩F′], which lies in the cone of the common subcomplex. Intersecting the resulting cone equality with Sn−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].

5 · Examples, counterexamples and false statements

None yet.

Sources