ExampleConstruction: Literature-sourcedVerification: 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.

Reduced words and lengths in a finite dihedral group

Example

Let $m \geq 2$ , $S = {s, t}$ and $m (s, t) = m$ , and put $W = ⟨ s, t ∣ s^{2} = t^{2} = (s t)^{m} = 1 ⟩$ . The exact order of $s t$ is $m$ by The rank-two block computation, exact dihedral orders, the signed reflection action, and ambient reducedness (4); the normal-form computation below verifies that $W$ is dihedral of order $2 m$ .

The $2 m$ elements $(s t)^{k}$ and $(s t)^{k} s$ with $0 \leq k < m$ are pairwise distinct and exhaust $W$ .
For $1 \leq q \leq m$ the two alternating words of length $q$ are reduced. Their values are distinct when $q < m$ and equal when $q = m$ ; explicitly, each has length $q$ , so values belonging to different lengths are distinct.
For $0 \leq k \leq m$ one has $ℓ ((s t)^{k}) = \min (2 k, 2 (m - k)),$ and for $0 \leq k \leq m - 1$ one has $(s t)^{k} s = (t s)^{m - k} s = (t s)^{m - k - 1} t$ and $ℓ ((s t)^{k} s) = \min (2 k + 1, 2 (m - k) - 1);$ in particular $ℓ (s) = 1$ and $ℓ ((s t)^{m - 1} s) = 1$ .
The element $(s t)^{k}$ with $2 k = m$ (only for even $m$ ) is the unique longest element $w_{0}$ of $W$ , of length $m$ ; its two reduced expressions are the two alternating words of length $m$ , and they are related by the braid move $s t s t \dots \mapsto t s t s \dots$ .

Facts & Assumptions

Given: A group $W$ presented by the Coxeter matrix on $S = {s, t}$ with $m (s, t) = m \geq 2$ , with the length function $ℓ$ of Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups; the exact order of $s t$ and the ambient reducedness of alternating words from The rank-two block computation, exact dihedral orders, the signed reflection action, and ambient reducedness; the deletion statement of Length parity, exchange, two-letter deletion, and faithfulness of the signed reflection action; and the vocabulary of powers and orders.

[F1]

Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups: $W = F (S) / N$ is presented by the relators $s^{2}$ , $t^{2}$ and $(s t)^{m}$ (the set $R = {s^{2} : s \in S} \cup {(s t)^{m (s, t)} : s \neq t, m (s, t) < \infty}$ ); the length $ℓ (w)$ is the least $k$ such that $w = s_{1} \dots s_{k}$ for some $s_{1}, \dots, s_{k} \in S$ , and $ℓ (1) = 0$ .

[F2]

The rank-two block computation, exact dihedral orders, the signed reflection action, and ambient reducedness (1),(4): " $σ_{s}^{2} = {i d}_{E}$ for every $s \in S$ ; each $σ_{s}$ is invertible, and $ℓ (s) = 1$ "; and "Consequently, for any distinct $s, t \in S$ , one has $s \neq t$ in $W$ and $s t$ has order exactly $m (s, t)$ in $W$ (infinite when $m (s, t) = \infty$ ).".

[F3]

The rank-two block computation, exact dihedral orders, the signed reflection action, and ambient reducedness (7): "Let $s \neq t$ , $m : = m (s, t)$ , and for $q \geq 1$ let $w_{q}$ be the value of the alternating word of length $q$ beginning with $s$ . If $m < \infty$ and $q \leq m$ , or if $m = \infty$ and $q \geq 1$ , then $ℓ (w_{q}) = q$ , every word in $S$ representing $w_{q}$ has length at least $q$ , and $w_{1}, \dots, w_{q}$ are pairwise distinct."

[F4]

Length parity, exchange, two-letter deletion, and faithfulness of the signed reflection action (3): "If the word $(s_{1}, \dots, s_{k})$ in $S$ is not reduced, then there are $i < j$ with $s_{1} \dots \hat{s_{i}} \dots \hat{s_{j}} \dots s_{k} = s_{1} \dots s_{k}$ . Hence repeated deletion of two letters transforms every word into a reduced expression for the same element".

[F5]

Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ , The order $∣ G ∣$ of a finite group and the order $ord (g)$ of an element, with $ord (g) = \infty$ when no positive power of $g$ is the identity: $g^{k}$ for $k \geq 0$ is the $k$ -fold product of $g$ with $g^{0} = 1$ , $g^{- k} = (g^{- 1})^{k}$ , and the order of $g$ is the least $k \geq 1$ with $g^{k} = 1$ when such $k$ exist, with $g^{ord (g)} = 1$ .

Verification

technique · direct computation with the normal forms of the dihedral group, using the exact order of $st$ and the ambient reducedness of alternating words

1.1F1F5

Exhaustion. Every element of $W$ is the value of a word in $s, t$ whose inverse letters are again letters ( $s^{- 1} = s$ , $t^{- 1} = t$ in $W$ because $s^{2}, t^{2} \in R$ [F1]), so it suffices to treat words in $s, t$ . Cancelling all consecutive equal letters using $s^{2} = t^{2} = 1$ turns any such word into an alternating word $(u_{1}, \dots, u_{q})$ with $u_{i + 1} \neq u_{i}$ . If $q$ is even, the value of the alternating word beginning with $s$ is $(s t)^{q / 2}$ and that of the one beginning with $t$ is $(t s)^{q / 2} = (s t)^{- q / 2}$ [F5]; if $q$ is odd, the corresponding values are $(s t)^{(q - 1) / 2} s$ and $(t s)^{(q - 1) / 2} t = (s t)^{- (q - 1) / 2} t = (s t)^{- (q + 1) / 2} s$ , because $t = (s t)^{- 1} s$ . Since $(s t)^{m} = 1$ [F1], an integer power $(s t)^{j}$ equals $(s t)^{k}$ for the unique $k \in {0, \dots, m - 1}$ with $j \equiv k (m o d m)$ , and $(s t)^{j} s = (s t)^{k} s$ ; hence every element of $W$ is one of the $2 m$ listed elements $(s t)^{k}, (s t)^{k} s$ with $0 \leq k < m$ .

1.2F1F2F3

Reducedness of alternating words. Let $1 \leq q \leq m$ and let $w_{q}$ be the value of the alternating word of length $q$ beginning with $s$ ; by [F3], $ℓ (w_{q}) = q$ and every word in $S$ representing $w_{q}$ has length at least $q$ , so that alternating word is reduced, and $w_{1}, \dots, w_{q}$ are pairwise distinct. The same length and reducedness statements hold for alternating words beginning with $t$ : interchanging the roles of $s$ and $t$ preserves every hypothesis, since $m (t, s) = m (s, t) = m$ and the presentation is symmetric in $s, t$ [F1]. To compare the two words of the same length, put $r = s t$ , so $t = r^{- 1} s$ . For $q = 2 h$ their values are $r^{h}$ and $r^{- h}$ ; for $q = 2 h + 1$ they are $r^{h} s$ and $r^{- h - 1} s$ . In either case equality is equivalent to $r^{q} = 1$ , which for $1 \leq q \leq m$ holds exactly at $q = m$ by [F2].

2.1F2F5step 1.1

Distinctness. If $(s t)^{k} = (s t)^{l}$ with $0 \leq k < l < m$ , then $(s t)^{l - k} = 1$ with $0 < l - k < m$ , contradicting the exact order $m$ of $s t$ [F2, F5]. If $(s t)^{k} s = (s t)^{l} s$ with $0 \leq k < l < m$ , then multiplying on the right by $s$ gives $(s t)^{k} = (s t)^{l}$ , the previous case. If finally $(s t)^{k} = (s t)^{l} s$ , then $(s t)^{k - l} = s$ , so $s \in ⟨ s t ⟩$ and also $t = s \cdot s t \in ⟨ s t ⟩$ , whence $W = ⟨ s t ⟩$ is cyclic and therefore abelian; then $s t = t s$ , so $(s t)^{2} = s t s t = s (t s) t = s (s t) t = (s s) (t t) = 1$ , and the order of $s t$ divides $2$ . Since that order is $m \geq 2$ by [F2], this forces $m = 2$ , in which case $⟨ s t ⟩ = {1, s t}$ while $s \in {1, s t}$ gives $s = 1$ or $t = 1$ ; both are impossible because $ℓ (s) = ℓ (t) = 1$ [F2]. Hence no rotation equals a reflection and the $2 m$ elements of step 1.1 are pairwise distinct, so they exhaust $W$ and $∣ W ∣ = 2 m$ . The identity $s (s t) s = (s t)^{- 1}$ , together with these distinct normal forms, identifies $W$ as the dihedral group.

2.2F1F5step 1.2

The rotation lengths. For $0 \leq k \leq m$ the element $(s t)^{k}$ also equals $(t s)^{m - k}$ : indeed $(t s) = (s t)^{- 1}$ [F5], so $(t s)^{m - k} = (s t)^{- (m - k)} = (s t)^{k - m} = (s t)^{k}$ , using $(s t)^{m} = 1$ [F1]. The two expressions $(s t)^{k}$ and $(t s)^{m - k}$ are alternating words of lengths $2 k$ and $2 (m - k)$ , whose minimum $q_{0} : = \min (2 k, 2 (m - k))$ satisfies $q_{0} \leq m$ because the two lengths sum to $2 m$ . The shorter of the two words has length $q_{0}$ ; if $q_{0} = 0$ it is the empty word with value $1$ , so $ℓ ((s t)^{k}) = 0 = q_{0}$ , and if $q_{0} \geq 1$ it is an alternating word of length $q_{0} \leq m$ whose value is $(s t)^{k}$ , so step 1.2 gives $ℓ ((s t)^{k}) = q_{0}$ and shows that no word represents $(s t)^{k}$ with fewer than $q_{0}$ letters. Hence $ℓ ((s t)^{k}) = \min (2 k, 2 (m - k))$ .

3.1F5step 1.2step 2.2

The reflection lengths. For $0 \leq k \leq m - 1$ one has $(s t)^{k} s = (t s)^{m - k} s = (t s)^{m - k - 1} (t s) s = (t s)^{m - k - 1} t$ , because $(t s)^{m - k} = (s t)^{k - m} = (s t)^{k}$ as in step 2.2; these are alternating words of lengths $2 k + 1$ and $2 (m - k) - 1$ , whose minimum $q_{1} : = \min (2 k + 1, 2 (m - k) - 1)$ is at most $m$ : indeed $q_{1} \leq 2 k + 1$ and $q_{1} \leq 2 (m - k) - 1$ , so $2 q_{1} \leq 2 m$ , that is $q_{1} \leq m$ . The shorter word is nonempty because $q_{1} \geq 1$ for $0 \leq k \leq m - 1$ , and step 1.2 applied to it (with the roles of $s$ and $t$ interchanged if it begins with $t$ ) gives that it is reduced, that its value $(s t)^{k} s$ has length exactly $q_{1}$ , and that no word for $(s t)^{k} s$ is shorter. Hence $ℓ ((s t)^{k} s) = \min (2 k + 1, 2 (m - k) - 1)$ ; the endpoint $k = 0$ gives $ℓ (s) = \min (1, 2 m - 1) = 1$ and the endpoint $k = m - 1$ gives $ℓ ((s t)^{m - 1} s) = \min (2 m - 1, 1) = 1$ .

4.1F4F5step 1.1step 2.1step 1.2step 2.2step 3.1∎

The longest element. Suppose $m$ is even and put $w_{0} : = (s t)^{m / 2}$ . By step 2.2, $ℓ (w_{0}) = \min (m, m) = m$ . Every rotation $(s t)^{k}$ with $k \neq m / 2$ has $ℓ = \min (2 k, 2 m - 2 k) < m$ : their minimum is at most $m$ , and equality would require both terms to equal $m$ because their sum is $2 m$ , forcing $k = m / 2$ . Every reflection $(s t)^{k} s$ with $0 \leq k \leq m - 1$ has $ℓ = \min (2 k + 1, 2 m - 2 k - 1) \leq m$ by step 3.1, and both entries of that minimum are odd while $m$ is even, so $ℓ \leq m - 1 < m$ . Together with steps 1.1 and 2.1 this shows that $w_{0}$ is the unique element of length $m$ , hence the unique longest element. A reduced word for $w_{0}$ of length $m$ cannot contain two consecutive equal letters, since deleting that pair would exhibit a shorter word for $w_{0}$ [F4] in contradiction to $ℓ (w_{0}) = m$ ; hence it is alternating. The two alternating words of length $m$ are $(s t)^{m / 2}$ and $(t s)^{m / 2}$ , both of which have value $w_{0}$ because $(t s)^{m / 2} = (s t)^{- m / 2} = (s t)^{m / 2}$ [F5], and they are reduced by step 1.2; so they are exactly the two reduced expressions of $w_{0}$ . They differ by the single replacement of the alternating block of length $m$ by the other alternating word of the same length, the braid move.

Depends on

Used by

Dependency tree · two levels

55 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

George Lusztig, Hecke Algebras with Unequal Parameters (revised 2014 book text, arXiv:math/0208154v2) (standard reference, not scraped)
Michael W. Davis, The Geometry and Topology of Coxeter Groups (Princeton University Press 2008; author's complete PDF) (standard reference, not scraped)