LemmaStatement: 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.

The length identity, the prefix property, left translation, and interval translation for weak order

Statement

Let $(S, m)$ be a finite Coxeter matrix, $W$ the presented group with length $ℓ$ , the descent sets $D_{L}, D_{R}$ and the weak orders $\leq_{R}, \leq_{L}$ as in The right and left weak orders, intervals, covers, and meets and joins of subsets. Then:

(1) Length identity. For all $u, v \in W$ ,

$u \leq_{R} v ⟺ ℓ (v) = ℓ (u) + ℓ (u^{- 1} v), u \leq_{L} v ⟺ ℓ (v) = ℓ (u) + ℓ (v u^{- 1}) .$

In particular $u \leq_{R} v$ implies $ℓ (u) \leq ℓ (v)$ , and likewise for $\leq_{L}$ .

(2) Prefix property. $u \leq_{R} v$ if and only if there exist reduced expressions $u = s_{1} \dots s_{k}$ and $v = s_{1} \dots s_{k} s_{1}^{'} \dots s_{q}^{'}$ with $k, q \geq 0$ ; equivalently, some reduced expression of $v$ has a reduced expression of $u$ as its initial segment. Symmetrically, $u \leq_{L} v$ if and only if there exist reduced expressions $u = t_{1} \dots t_{k}$ and $v = t_{1}^{'} \dots t_{q}^{'} t_{1} \dots t_{k}$ .

(3) Left translation. For all $u, v \in W$ and $s \in S$ with $s \in D_{L} (u) \cap D_{L} (v)$ ,

$u \leq_{R} v ⟺ s u \leq_{R} s v .$

(4) Interval translation. If $u \leq_{R} v$ , then $x \mapsto u x$ is a bijection $[1, u^{- 1} v]_{R} \to [u, v]_{R}$ satisfying $ℓ (u x) = ℓ (u) + ℓ (x)$ for every $x \in [1, u^{- 1} v]_{R}$ and preserving and reflecting the relation: for all $x, x^{'}$ in the source interval, $x \leq_{R} x^{'} ⟺ u x \leq_{R} u x^{'}$ . If $u \leq_{L} v$ , then $x \mapsto x u$ is a bijection $[1, v u^{- 1}]_{L} \to [u, v]_{L}$ with the analogous length and relation properties. No Choice is used.

Facts & Assumptions

Given: A finite Coxeter matrix $(S, m)$ with presented group $W$ , length function $ℓ$ , descent sets $D_{L}, D_{R}$ and weak orders $\leq_{R}, \leq_{L}$ as in The right and left weak orders, intervals, covers, and meets and joins of subsets, and elements $u, v, x \in W$ and $s \in S$ as specified in each clause.

[F1]

The right and left weak orders, intervals, covers, and meets and joins of subsets: $u \leq_{R} v$ means that $v = u x$ for some $x \in W$ with $ℓ (v) = ℓ (u) + ℓ (x)$ ; $u \leq_{L} v$ means that $v = x u$ for some $x \in W$ with $ℓ (v) = ℓ (u) + ℓ (x)$ ; and $u \leq_{R} v ⟺ u^{- 1} \leq_{L} v^{- 1}$ . Intervals, covers and bounded subsets are defined there.

[F2]

Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (3): by inversion, $w \mapsto w^{- 1}$ preserves lengths, that is $ℓ (y) = ℓ (y^{- 1})$ for every $y \in W$ .

[F3]

Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups: for $w \in W$ , $ℓ (w) = \min {k \in N : there exist s_{1}, \dots, s_{k} \in S with w = s_{1} \dots s_{k}}$ ; a reduced expression of $w$ is a word $(s_{1}, \dots, s_{k})$ in $S$ with $w = s_{1} \dots s_{k}$ and $k = ℓ (w)$ .

[F4]

Standard parabolic subgroups, descent-free one- and two-sided representatives, parabolic and reflection subgroups (2): $D_{L} (w) = {s \in S : ℓ (s w) < ℓ (w)}$ , $D_{R} (w) = {s \in S : ℓ (w s) < ℓ (w)}$ , and for every $s \in S, w \in W$ , $ℓ (s w) - ℓ (w)$ and $ℓ (w s) - ℓ (w)$ lie in ${- 1, + 1}$ . Thus $s \in D_{L} (w)$ implies $ℓ (s w) = ℓ (w) - 1$ ; also $ℓ (s) = 1$ by taking $w = 1$ and using $ℓ (1) = 0$ from [A1].

[F5]

Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups: every simple generator $s \in S$ satisfies $s^{2} = 1$ in $W$ .

[A1]

For the word length of [F3]: $ℓ (1) = 0$ , since $1$ is the value of the empty word and no shorter length is possible; $ℓ (a) = 0$ forces $a = 1$ ; and $ℓ (a b) \leq ℓ (a) + ℓ (b)$ for all $a, b \in W$ , because concatenating a reduced expression of $a$ with one of $b$ gives a word of length $ℓ (a) + ℓ (b)$ representing $a b$ .

Proof

1.1F1F3A1givenalgebra

For all $u, v \in W$ , $u \leq_{R} v$ if and only if $ℓ (v) = ℓ (u) + ℓ (u^{- 1} v)$ , and then $ℓ (u) \leq ℓ (v)$ . Indeed, if $u \leq_{R} v$ then $v = u x$ with $ℓ (v) = ℓ (u) + ℓ (x)$ for some $x$ , and multiplying $v = u x$ on the left by $u^{- 1}$ gives $x = u^{- 1} v$ , hence $ℓ (v) = ℓ (u) + ℓ (u^{- 1} v)$ ; conversely, if $ℓ (v) = ℓ (u) + ℓ (u^{- 1} v)$ , then $x : = u^{- 1} v$ satisfies $v = u x$ with $ℓ (v) = ℓ (u) + ℓ (x)$ , so $u \leq_{R} v$ . The final inequality follows from $ℓ (u^{- 1} v) \geq 0$ .

1.2F1F3A1givenalgebra

For all $u, v \in W$ , $u \leq_{L} v$ if and only if $ℓ (v) = ℓ (u) + ℓ (v u^{- 1})$ , and then $ℓ (u) \leq ℓ (v)$ . The argument is symmetric: if $u \leq_{L} v$ then $v = x u$ with $ℓ (v) = ℓ (u) + ℓ (x)$ , and multiplying on the right by $u^{- 1}$ gives $x = v u^{- 1}$ ; conversely $x : = v u^{- 1}$ realizes the defining factorization whenever the displayed length identity holds.

2.1F1F3A1step 1.1givenalgebra

If $u \leq_{R} v$ , then $v$ has a reduced expression $s_{1} \dots s_{k} s_{1}^{'} \dots s_{q}^{'}$ whose initial segment $s_{1} \dots s_{k}$ is a reduced expression of $u$ . By step 1.1, $ℓ (v) = ℓ (u) + ℓ (u^{- 1} v)$ ; choose reduced expressions $u = s_{1} \dots s_{k}$ and $u^{- 1} v = s_{1}^{'} \dots s_{q}^{'}$ , so $k = ℓ (u)$ and $q = ℓ (u^{- 1} v)$ . The concatenated word $s_{1} \dots s_{k} s_{1}^{'} \dots s_{q}^{'}$ represents the element $u \cdot u^{- 1} v = v$ and has length $k + q = ℓ (v)$ ; hence it is a reduced expression of $v$ whose initial segment $s_{1} \dots s_{k}$ is the chosen reduced expression of $u$ .

2.2F1A1step 1.1givenalgebra

Conversely, if $v$ has a reduced expression $s_{1} \dots s_{m}$ and $k \leq m$ is such that the initial segment $s_{1} \dots s_{k}$ is a reduced expression of $u$ , then $u \leq_{R} v$ . Indeed the suffix $x : = s_{k + 1} \dots s_{m}$ satisfies $v = u x$ and $ℓ (x) \leq m - k$ , so $ℓ (u) + ℓ (x) \leq k + (m - k) = m = ℓ (v)$ , while subadditivity gives the reverse inequality $ℓ (v) \leq ℓ (u) + ℓ (x)$ ; hence $ℓ (v) = ℓ (u) + ℓ (x)$ , which is the defining condition for $u \leq_{R} v$ by step 1.1.

2.3F1F4F5A1step 1.1givenalgebra

Let $s \in D_{L} (u) \cap D_{L} (v)$ . Then $u \leq_{R} v$ if and only if $s u \leq_{R} s v$ . By [F4], each of $ℓ (s u) - ℓ (u)$ and $ℓ (s v) - ℓ (v)$ lies in ${- 1, + 1}$ ; the strict descent inequalities therefore give $ℓ (s u) = ℓ (u) - 1$ and $ℓ (s v) = ℓ (v) - 1$ . Also $ℓ (s) = 1$ by [F4] and [A1]. For the forward direction assume $u \leq_{R} v$ ; by step 1.1, $v = u x$ with $ℓ (v) = ℓ (u) + ℓ (x)$ . Subadditivity gives $ℓ (s v) = ℓ (s u x) \leq ℓ (s u) + ℓ (x) = ℓ (v) - 1$ , while $v = s (s v)$ by [F5], so $ℓ (v) \leq ℓ (s) + ℓ (s v) = 1 + ℓ (s v)$ and $ℓ (s v) \geq ℓ (v) - 1$ . Therefore $ℓ (s v) = ℓ (s u) + ℓ (x)$ and $s v = s u \cdot x$ , which is $s u \leq_{R} s v$ . For the converse assume $s u \leq_{R} s v$ ; then $s v = s u \cdot x$ with $ℓ (s v) = ℓ (s u) + ℓ (x)$ . Multiplying on the left by $s$ and using [F5] gives $v = u x$ , and the descent identities give $ℓ (v) = ℓ (s v) + 1 = ℓ (s u) + ℓ (x) + 1 = ℓ (u) + ℓ (x)$ , so $u \leq_{R} v$ .

2.4F1A1step 1.1givenalgebra

Assume $u \leq_{R} v$ . Then for every $x \in W$ one has $x \in [1, u^{- 1} v]_{R}$ if and only if $u x \in [u, v]_{R}$ , and in that case $ℓ (u x) = ℓ (u) + ℓ (x)$ . For the forward direction suppose $x \leq_{R} u^{- 1} v$ ; by step 1.1, $ℓ (u^{- 1} v) = ℓ (x) + ℓ (x^{- 1} u^{- 1} v)$ , so $ℓ (v) = ℓ (u) + ℓ (u^{- 1} v) = ℓ (u) + ℓ (x) + ℓ (x^{- 1} u^{- 1} v)$ . Since $ℓ (u x) \leq ℓ (u) + ℓ (x)$ and $ℓ (v) \leq ℓ (u x) + ℓ (x^{- 1} u^{- 1} v)$ both hold by subadditivity, these are equalities, giving $ℓ (u x) = ℓ (u) + ℓ (x)$ and $ℓ (v) = ℓ (u x) + ℓ ((u x)^{- 1} v)$ , that is $u \leq_{R} u x \leq_{R} v$ . For the converse suppose $u \leq_{R} u x \leq_{R} v$ ; then $ℓ (u x) = ℓ (u) + ℓ (x)$ and $ℓ (v) = ℓ (u x) + ℓ (x^{- 1} u^{- 1} v) = ℓ (u) + ℓ (x) + ℓ (x^{- 1} u^{- 1} v)$ , while the hypothesis $u \leq_{R} v$ and step 1.1 give $ℓ (v) = ℓ (u) + ℓ (u^{- 1} v)$ ; cancelling $ℓ (u)$ yields $ℓ (u^{- 1} v) = ℓ (x) + ℓ (x^{- 1} u^{- 1} v)$ , that is $x \leq_{R} u^{- 1} v$ .

3.1F1F2A1step 2.1step 2.2givenalgebra

$u \leq_{L} v$ if and only if there are reduced expressions $u = t_{1} \dots t_{k}$ and $v = t_{1}^{'} \dots t_{q}^{'} t_{1} \dots t_{k}$ . By [F1], $u \leq_{L} v ⟺ u^{- 1} \leq_{R} v^{- 1}$ , and by [F2] inversion preserves lengths; moreover, if $s_{1} \dots s_{m}$ is a reduced expression, then $(s_{1} \dots s_{m})^{- 1} = s_{m} \dots s_{1}$ has length $m = ℓ (s_{1} \dots s_{m}) = ℓ ((s_{1} \dots s_{m})^{- 1})$ , so reversing a reduced expression gives a reduced expression of the inverse. Applying steps 2.1 and 2.2 to the pair $u^{- 1} \leq_{R} v^{- 1}$ and then inverting the two reduced expressions produces exactly the two directions of the claim.

4.1F1F2step 2.4givenalgebra∎

Assume $u \leq_{R} v$ . The map $y \mapsto u y$ on $W$ is a bijection with inverse $y \mapsto u^{- 1} y$ ; by step 2.4 it restricts to a bijection $[1, u^{- 1} v]_{R} \to [u, v]_{R}$ satisfying $ℓ (u x) = ℓ (u) + ℓ (x)$ throughout. For $x, x^{'} \in [1, u^{- 1} v]_{R}$ , if $x \leq_{R} x^{'}$ , then $x^{'} = x y$ with $ℓ (x^{'}) = ℓ (x) + ℓ (y)$ , so $u x^{'} = u x y$ and $ℓ (u x^{'}) = ℓ (u) + ℓ (x^{'}) = ℓ (u) + ℓ (x) + ℓ (y) = ℓ (u x) + ℓ (y)$ , giving $u x \leq_{R} u x^{'}$ ; conversely, if $u x \leq_{R} u x^{'}$ , then $u x^{'} = u x y$ with $ℓ (u x^{'}) = ℓ (u x) + ℓ (y)$ , so cancelling $u$ gives $x^{'} = x y$ , and step 2.4 gives $ℓ (u) + ℓ (x^{'}) = ℓ (u x^{'}) = ℓ (u x) + ℓ (y) = ℓ (u) + ℓ (x) + ℓ (y)$ , hence $ℓ (x^{'}) = ℓ (x) + ℓ (y)$ and $x \leq_{R} x^{'}$ . Thus the bijection preserves and reflects $\leq_{R}$ . If instead $u \leq_{L} v$ , then $u^{- 1} \leq_{R} v^{- 1}$ by [F1]; applying the right-handed result to $u^{- 1} \leq_{R} v^{- 1}$ and inverting gives a bijection $x \mapsto x u$ from $[1, v u^{- 1}]_{L}$ to $[u, v]_{L}$ that preserves and reflects $\leq_{L}$ . Its length identity is $ℓ (x u) = ℓ ((x u)^{- 1}) = ℓ (u^{- 1} x^{- 1}) = ℓ (u^{- 1}) + ℓ (x^{- 1}) = ℓ (u) + ℓ (x)$ by [F2]. No Choice was used anywhere in this proof.

Depends on

Used by

Dependency tree · two levels

35 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

Anders Bjorner and Francesco Brenti, Combinatorics of Coxeter Groups (Graduate Texts in Mathematics 231, Springer 2005; author-hosted complete PDF) (standard reference, not scraped)
John R. Stembridge, On the fully commutative elements of Coxeter groups (author-hosted preprint) (standard reference, not scraped)