TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08

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.

Carter's reflection-length formula, the absolute order on a finite Coxeter group, and moved-space rigidity under a common upper bound

Statement

Let $(W, S)$ be a Coxeter system of finite type with $S$ finite, with $V = R^{S}$ , positive definite Coxeter form $B$ , canonical reflection representation $ρ$ , root system $Φ$ , reflection set $T$ and length function $ℓ$ (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups, The real Coxeter form, its radical, reflections, and form-preserving maps, The canonical reflection homomorphism, roots, reflections, and the positive cone, Finiteness criterion: W is finite exactly when the Coxeter form is positive definite), and let $ℓ_{T}$ , $M$ , $F$ and $\leq_{T}$ be as in Reflection length, the absolute order on a finite Coxeter group, and the moved and fixed spaces of an orthogonal operator. Then:

(1) Carter's formula. For every $w \in W$ ,

$ℓ_{T} (w) = \dim M (w) = \dim V - \dim F (w) .$

(2) The absolute order. $\leq_{T}$ is a partial order on $W$ (Partial order and partially ordered set), and:

(i) $u \leq_{T} v$ holds if and only if there are reflections $t_{1}, \dots, t_{m} \in T$ and an index $k \leq m$ such that $u = t_{1} \dots t_{k}$ and $v = t_{1} \dots t_{m}$ are shortest reflection factorizations, that is, $k = ℓ_{T} (u)$ and $m = ℓ_{T} (v)$ (a shortest reflection factorization of $u$ is a prefix of one of $v$ );

(ii) $ℓ_{T} (1) = 0$ , $u <_{T} v$ implies $ℓ_{T} (u) < ℓ_{T} (v)$ , and $ℓ_{T} (y) = ℓ_{T} (x) + 1$ whenever $y$ covers $x$ ; hence $ℓ_{T}$ is a rank function and every interval $[u, v]_{T} = {x \in W : u \leq_{T} x \leq_{T} v}$ is finite (Graded poset, rank function, and rank levels);

(iii) $∣ ℓ_{T} (u) - ℓ_{T} (v) ∣ \leq ℓ_{T} (u^{- 1} v)$ , $ℓ_{T} (u^{- 1}) = ℓ_{T} (u)$ and $ℓ_{T} (v u v^{- 1}) = ℓ_{T} (u)$ for all $u, v \in W$ ;

(iv) $u \leq_{T} v$ implies $M (u) \subseteq M (v)$ and $F (v) \subseteq F (u)$ .

(3) Moved-space rigidity under a common upper bound. Let $α, β, δ \in W$ with $α \leq_{T} δ$ and $β \leq_{T} δ$ . Then

$α \leq_{T} β ⟺ M (α) \subseteq M (β);$

in particular $M (α) = M (β)$ implies $α = β$ , and $u \mapsto M (u)$ is an order isomorphism from $[1, δ]_{T}$ onto its image ordered by inclusion. The proof of the converse uses the common upper bound $δ$ , through the restriction of $δ$ to the subspace $M (α)$ ; the converse is claimed only under this hypothesis (see the companion example of the $I_{2} (4)$ rotation, where the hypothesis fails).

Facts & Assumptions

Given: The finite-type Coxeter datum $W, S, V, B, ρ, Φ, T$ and the elements $α, β, δ \in W$ above; $ℓ_{T}$ , $M$ , $F$ and $\leq_{T}$ are as in Reflection length, the absolute order on a finite Coxeter group, and the moved and fixed spaces of an orthogonal operator.

[F1]

Every $w \in W$ is a product of $k = \dim M (w)$ elements of $T$ , no product of fewer elements of $T$ represents $w$ , and $ℓ_{T} (w) = \dim M (w)$ . Root normals inside the moved space, factorizations into reflections, and independent normals

[F2]

The Wall form lemma holds on the positive definite space $(V, B)$ : (1) $M (A) = F (A)^{⊥}$ and $V = M (A) \oplus F (A)$ for $A \in O (V)$ ; (4) for $B \leq_{O} A$ one has $M (B) \subseteq M (A)$ and $B = A_{M (B)}$ , the assignment $U \mapsto A_{U}$ is a bijection from subspaces of $M (A)$ onto ${B \in O (V) : B \leq_{O} A}$ , and it is an order isomorphism for inclusion and $\leq_{O}$ , with $(A_{U^{'}})_{U} = A_{U}$ and $A_{U} \leq_{O} A_{U^{'}}$ for $U \subseteq U^{'}$ ; (5) an element of $O (V)$ is a product of exactly $\dim M$ reflections, and $B \leq_{O} A$ holds exactly when $B$ is a prefix of a shortest factorization of $A$ . The Wall form of an orthogonal operator, subspace restriction, and the interval structure of the orthogonal reflection-length order

[F3]

$u \leq_{T} v$ means $ℓ_{T} (v) = ℓ_{T} (u) + ℓ_{T} (u^{- 1} v)$ , $B \leq_{O} A$ means $\dim M (A) = \dim M (B) + \dim M (B^{- 1} A)$ , and $T = {w s w^{- 1} : w \in W, s \in S}$ is closed under inversion; for $u \in W$ one has $M (u) = M (ρ (u))$ and $F (u) = F (ρ (u))$ . Reflection length, the absolute order on a finite Coxeter group, and the moved and fixed spaces of an orthogonal operator

[F4]

$\leq_{T}$ is a relation on the finite set $W$ ; $\leq_{T}$ is a partial order exactly when it is reflexive, antisymmetric and transitive, and a rank function on a finite poset is a map $ρ$ with $ρ (minimal) = 0$ and $ρ (y) = ρ (x) + 1$ across covers. Partial order and partially ordered set Graded poset, rank function, and rank levels

[F5]

The canonical reflection homomorphism, roots, reflections, and the positive cone (1): $ρ : W \to G L (V)$ is a group homomorphism into the group of invertible linear maps, so $ρ (v)^{- 1} = ρ (v^{- 1})$ and $ρ (v)^{- 1} (V) = V$ .

Proof

technique · direct

1.1F1F2

For every $w \in W$ the factorization lemma gives $ℓ_{T} (w) = \dim M (w)$ [F1], and the Wall form lemma gives $V = M (w) \oplus F (w)$ F2, so $\dim M (w) = \dim V - \dim F (w)$ ; this is Carter's formula (1).

1.2F1

For $x, y \in W$ one has $ℓ_{T} (x y) \leq ℓ_{T} (x) + ℓ_{T} (y)$ : shortest factorizations $x = t_{1} \dots t_{k}$ and $y = s_{1} \dots s_{l}$ with $k = ℓ_{T} (x)$ , $l = ℓ_{T} (y)$ exist by [F1] and concatenate to $x y = t_{1} \dots t_{k} s_{1} \dots s_{l}$ , a product of $k + l$ elements of $T$ . Also $ℓ_{T} (x^{- 1}) = ℓ_{T} (x)$ , because if $x = t_{1} \dots t_{k}$ then $x^{- 1} = t_{k} \dots t_{1}$ , giving $ℓ_{T} (x^{- 1}) \leq ℓ_{T} (x)$ , and applying this to $x^{- 1}$ gives equality.

1.3F1

$ℓ_{T} (x) = 0$ if and only if $x = 1$ : by [F1] an element of reflection length $0$ is a product of $0$ elements of $T$ , which is the identity, and conversely the empty product represents $1$ ; in particular $1$ is the only element of reflection length $0$ .

2.1step 1.1F3

For $u, v \in W$ one has $u \leq_{T} v$ if and only if $ρ (u) \leq_{O} ρ (v)$ : by [F3] the two relations read $ℓ_{T} (v) = ℓ_{T} (u) + ℓ_{T} (u^{- 1} v)$ and $\dim M (v) = \dim M (u) + \dim M (u^{- 1} v)$ , and $ℓ_{T} = \dim M$ is step 1.1.

2.2step 1.1F3F5algebra

Conjugation invariance: for $u, v \in W$ , [F5] gives $ρ (v u v^{- 1}) - i d = ρ (v) (ρ (u) - i d) ρ (v)^{- 1}$ . Since $ρ (v)^{- 1} (V) = V$ , taking images and using [F3] yields $M (v u v^{- 1}) = ρ (v) M (u)$ . The invertible map $ρ (v)$ preserves the dimension of this subspace, so $\dim M (v u v^{- 1}) = \dim M (u)$ and hence $ℓ_{T} (v u v^{- 1}) = ℓ_{T} (u)$ by step 1.1.

2.3step 1.2step 1.3

The relation $\leq_{T}$ is reflexive, antisymmetric and transitive, and the triangle inequality holds. Reflexive: $ℓ_{T} (u) = ℓ_{T} (u) + ℓ_{T} (u^{- 1} u)$ by step 1.3. Antisymmetric: if $u \leq_{T} v$ and $v \leq_{T} u$ , then $ℓ_{T} (u^{- 1} v) = ℓ_{T} (v) - ℓ_{T} (u)$ and $ℓ_{T} (v^{- 1} u) = ℓ_{T} (u) - ℓ_{T} (v)$ , while $ℓ_{T} (v^{- 1} u) = ℓ_{T} ((u^{- 1} v)^{- 1}) = ℓ_{T} (u^{- 1} v)$ by step 1.2, so $ℓ_{T} (u^{- 1} v) = 0$ and $u^{- 1} v = 1$ , that is $u = v$ , by step 1.3. Transitive: if $u \leq_{T} v \leq_{T} w$ , then $ℓ_{T} (w) = ℓ_{T} (u) + ℓ_{T} (u^{- 1} v) + ℓ_{T} (v^{- 1} w)$ , while $ℓ_{T} (u^{- 1} w) \leq ℓ_{T} (u^{- 1} v) + ℓ_{T} (v^{- 1} w)$ and $ℓ_{T} (w) \leq ℓ_{T} (u) + ℓ_{T} (u^{- 1} w)$ by step 1.2; all inequalities are therefore equalities and $ℓ_{T} (w) = ℓ_{T} (u) + ℓ_{T} (u^{- 1} w)$ , that is $u \leq_{T} w$ . Triangle inequality: $ℓ_{T} (v) \leq ℓ_{T} (u) + ℓ_{T} (u^{- 1} v)$ and $ℓ_{T} (u) \leq ℓ_{T} (v) + ℓ_{T} (v^{- 1} u) = ℓ_{T} (v) + ℓ_{T} (u^{- 1} v)$ by step 1.2, so $∣ ℓ_{T} (u) - ℓ_{T} (v) ∣ \leq ℓ_{T} (u^{- 1} v)$ .

2.4step 1.2F1

Prefix form: $u \leq_{T} v$ holds if and only if there are reflections $t_{1}, \dots, t_{m} \in T$ and an index $k \leq m$ such that $u = t_{1} \dots t_{k}$ and $v = t_{1} \dots t_{m}$ are shortest factorizations, that is $k = ℓ_{T} (u)$ and $m = ℓ_{T} (v)$ . If $u \leq_{T} v$ , then [F1] supplies shortest factorizations $u = t_{1} \dots t_{k}$ and $u^{- 1} v = s_{1} \dots s_{l}$ with $l = ℓ_{T} (u^{- 1} v)$ , and $v = u \cdot (u^{- 1} v) = t_{1} \dots t_{k} s_{1} \dots s_{l}$ has length $k + l = ℓ_{T} (v)$ , so it is shortest and exhibits the required prefix. Conversely, given such factorizations, $u^{- 1} v = (t_{1} \dots t_{k})^{- 1} t_{1} \dots t_{m} = t_{k} \dots t_{1} t_{1} \dots t_{m} = t_{k + 1} \dots t_{m}$ , so $ℓ_{T} (u^{- 1} v) \leq m - k$ and hence $ℓ_{T} (u) + ℓ_{T} (u^{- 1} v) \leq k + (m - k) = m = ℓ_{T} (v)$ , while $ℓ_{T} (v) \leq ℓ_{T} (u) + ℓ_{T} (u^{- 1} v)$ by step 1.2; thus equality holds and $u \leq_{T} v$ .

3.1step 1.3step 2.3step 2.4F4

Part (ii). First $ℓ_{T} (1) = 0$ by step 1.3. If $u <_{T} v$ , then $ℓ_{T} (v) = ℓ_{T} (u) + ℓ_{T} (u^{- 1} v)$ with $u^{- 1} v \neq 1$ , so $ℓ_{T} (u^{- 1} v) \geq 1$ by step 1.3 and $ℓ_{T} (u) < ℓ_{T} (v)$ . Suppose now that $y$ covers $x$ , so $x <_{T} y$ , and put $d : = ℓ_{T} (y) - ℓ_{T} (x) = ℓ_{T} (x^{- 1} y) \geq 1$ ; by step 2.4 there are $t_{1}, \dots, t_{m} \in T$ with $y = t_{1} \dots t_{m}$ and $x = t_{1} \dots t_{k}$ shortest, so $d = m - k$ . If $d \geq 2$ , put $z : = t_{1} \dots t_{k + 1}$ ; then $z^{- 1} y = t_{k + 2} \dots t_{m}$ is a product of $m - k - 1$ elements of $T$ , so $ℓ_{T} (z^{- 1} y) \leq m - k - 1$ and, by the triangle inequality of step 2.3, $ℓ_{T} (z) \geq ℓ_{T} (y) - ℓ_{T} (z^{- 1} y) \geq m - (m - k - 1) = k + 1$ , while $ℓ_{T} (z) \leq k + 1$ ; hence $ℓ_{T} (z) = k + 1$ and step 2.4 applied to the shortest factorizations $x = t_{1} \dots t_{k}$ and $z = t_{1} \dots t_{k + 1}$ gives $x <_{T} z$ , and applied to $z = t_{1} \dots t_{k + 1}$ and $y = t_{1} \dots t_{m}$ gives $z <_{T} y$ — contradicting that $y$ covers $x$ . Hence $d = 1$ . Every minimal element is $1$ : if $x$ is minimal and $x \neq 1$ , then $1 <_{T} x$ because $ℓ_{T} (x) = ℓ_{T} (1) + ℓ_{T} (x)$ by steps 1.3, a contradiction; and $ℓ_{T} (1) = 0$ . Consequently $ℓ_{T}$ is a rank function on the finite poset $(W, \leq_{T})$ [F4], and every interval $[u, v]_{T}$ is contained in the finite set $W$ .

3.2step 2.1F2F3

Part (iv): if $u \leq_{T} v$ , then $ρ (u) \leq_{O} ρ (v)$ by step 2.1, so F2 gives $M (u) \subseteq M (v)$ , and then $F (v) = M (v)^{⊥} \subseteq M (u)^{⊥} = F (u)$ by F2 and [F3].

4.1step 2.1step 2.3step 3.2F2∎

Let $α \leq_{T} δ$ and $β \leq_{T} δ$ . If $α \leq_{T} β$ , then $M (α) \subseteq M (β)$ by step 3.2. Conversely assume $M (α) \subseteq M (β)$ ; by step 2.1 one has $ρ (α) \leq_{O} ρ (δ)$ and $ρ (β) \leq_{O} ρ (δ)$ , so F2 gives $ρ (α) = (ρ (δ))_{M (α)}$ , $ρ (β) = (ρ (δ))_{M (β)}$ , and $M (β) \subseteq M (δ)$ ; since the restriction assignment of F2 is an order isomorphism and $M (α) \subseteq M (β)$ , one has $ρ (α) = ((ρ (δ))_{M (β)})_{M (α)} = (ρ (β))_{M (α)} \leq_{O} ρ (β)$ , and step 2.1 gives $α \leq_{T} β$ . Hence $α \leq_{T} β$ if and only if $M (α) \subseteq M (β)$ ; in particular $M (α) = M (β)$ yields both $α \leq_{T} β$ and $β \leq_{T} α$ , so $α = β$ by antisymmetry in step 2.3, and the map $u \mapsto M (u)$ is an order isomorphism from $[1, δ]_{T}$ onto its image ordered by inclusion, being order-preserving and order-reflecting by the equivalence just proved and injective by the equality statement. This proves (1), (2) and (3).

Depends on

Used by

Cited to discharge well-definedness by Reflection length, the absolute order on a finite Coxeter group, and the moved and fixed spaces of an orthogonal operator.

Dependency tree · two levels

120 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

R. W. Carter, Conjugacy classes in the Weyl group, Compositio Mathematica 25 (1972) 1-59 (Numdam full text) (standard reference, not scraped)
T. Brady and C. Watt, Lattices in finite real reflection groups (arXiv:math/0501502) (standard reference, not scraped)