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.

A nonreduced word deleted by its repeated prefix reflection, and an exchange step

Example

Let $S = {s, t}$ with $m (s, t) = 3$ , so that $W = I_{2} (3)$ is the dihedral group of order $6$ in which $s t$ has order $3$ (The rank-two block computation, exact dihedral orders, the signed reflection action, and ambient reducedness (4), Reduced words and lengths in a finite dihedral group (1)).

Exchange. The word $(s, t)$ is a reduced expression of $s t$ with $ℓ (s t) = 2$ . Since $s \cdot s t = t$ has length $1 < 2$ , the exchange theorem (Length parity, exchange, two-letter deletion, and faithfulness of the signed reflection action (2)) predicts $s \cdot s t = t = s_{1} \dots \hat{s_{1}} \dots s_{2}$ , the deletion of the first letter; and indeed $s s t = t$ .
A nonreduced word. In the word $(s, t, s, t)$ the prefix reflections are $r_{1} = s$ , $r_{2} = s t s$ , $r_{3} = t$ , $r_{4} = s$ ; thus $r_{1} = r_{4}$ . Deleting the first and the last letter gives the word $(t, s)$ with value $t s$ , and indeed $s t s t = (s t)^{2} = (s t)^{- 1} = t s$ , so the deleted word is an expression of the same element: $s t s t = t s$ .
Consequences. The word $(s, t, s, t)$ is nonreduced: $ℓ (s t s t) = ℓ (t s) = 2 < 4$ , in agreement with the length formula $ℓ ((s t)^{2}) = \min (4, 2) = 2$ of Reduced words and lengths in a finite dihedral group (3). The reflection set of the element is $Φ (s t s t) = {s t s, t}$ , of cardinality $2 = ℓ (s t s t)$ , and $s \notin Φ (s t s t)$ because $s = r_{1} = r_{4}$ occurs an even number of times; deleting a different pair, e.g. the letters $s$ at positions $1$ and $3$ , does not preserve the value: $t \cdot t = 1 \neq t s$ .

Facts & Assumptions

Given: The Coxeter matrix on $S = {s, t}$ with $m (s, t) = 3$ ; the presented group $W$ with its length $ℓ$ of Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups; the reflection set $T$ , the prefix reflections, the sign-change sets $Φ (w)$ and the exact order of $s t$ from The rank-two block computation, exact dihedral orders, the signed reflection action, and ambient reducedness; the exchange and deletion statements of Length parity, exchange, two-letter deletion, and faithfulness of the signed reflection action; and the length table for $I_{2} (3)$ of Reduced words and lengths in a finite dihedral group.

[F1]

The rank-two block computation, exact dihedral orders, the signed reflection action, and ambient reducedness (1),(4),(6): " $σ_{s}^{2} = {i d}_{E}$ for every $s \in S$ ; each $σ_{s}$ is invertible, and $ℓ (s) = 1$ "; "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$ ).", so here $s t$ has order $3$ ; "(a) If $r_{i} = r_{j}$ for some $i < j$ , then $s_{1} \dots \hat{s_{i}} \dots \hat{s_{j}} \dots s_{k} = w$ : the two letters $s_{i}, s_{j}$ can be deleted"; "(b) $(- 1)^{n (r)} = : η (r, w)$ depends only on $w$ and $r$ "; and for a reduced word "(c) ... the set $Φ (w) : = {r_{1}, \dots, r_{k}} = {r \in T : η (r, w) = - 1}$ is independent of the reduced expression chosen, with $# Φ (w) = ℓ (w)$ ", where $r_{i} = s_{1} \dots s_{i - 1} s_{i} s_{i - 1} \dots s_{1}$ are the prefix reflections and $n (r) = # {i : r_{i} = r}$ .

[F2]

Length parity, exchange, two-letter deletion, and faithfulness of the signed reflection action (2): "Let $w = s_{1} \dots s_{k}$ be a reduced expression and let $s \in S$ satisfy $ℓ (s w) = k - 1$ . Then $s w = s_{1} \dots \hat{s_{i}} \dots s_{k}$ for some $i \in {1, \dots, k}$ "; and (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}$ ."

[F3]

Reduced words and lengths in a finite dihedral group (3): for $0 \leq k \leq m$ one has " $ℓ ((s t)^{k}) = \min (2 k, 2 (m - k))$ ", so with $m = 3$ and $k = 2$ this reads $ℓ ((s t)^{2}) = \min (4, 2) = 2$ .

[F4]

Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ : $g^{k}$ is the $k$ -fold product with $g^{0} = 1$ and $g^{- k} = (g^{- 1})^{k}$ , so $g \cdot g^{- 1} = 1$ and $(s t)^{- 1} = t^{- 1} s^{- 1} = t s$ in $W$ , where $s^{- 1} = s$ and $t^{- 1} = t$ because $s^{2}, t^{2}$ are relators of the presentation of Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups.

[F5]

Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups: the relators are $s^{2}$ , $t^{2}$ and $(s t)^{3}$ , and $ℓ (w)$ is the least length of a word in $S$ representing $w$ .

Verification

technique · direct computation in $I_2(3)$, with the prefix reflections read off from the definition and the general exchange and deletion statements applied to this word

1.1F1F2F3

The exchange step. The word $(s, t)$ has value $s t$ and length $2$ , and $ℓ (s t) = 2$ by [F3] (the case $m = 3$ , $k = 1$ gives $\min (2, 4) = 2$ ), so $(s, t)$ is a reduced expression of $s t$ . In $W$ one has $s^{2} = 1$ , so $s \cdot s t = s^{2} t = t$ ; and $ℓ (t) = 1$ by [F1]. Hence $ℓ (s \cdot s t) = 1 = 2 - 1$ and [F2] (2) applies to the reduced word $(s_{1}, s_{2}) = (s, t)$ with the letter $s$ : there is $i \in {1, 2}$ with $s \cdot s t = s_{1} \dots \hat{s_{i}} \dots s_{2}$ . Since $s \cdot s t = t$ and the two deletion words are $\hat{s_{1}} s_{2} = t$ and $s_{1} \hat{s_{2}} = s$ , only $i = 1$ gives the value $t$ , so $s \cdot s t = \hat{s_{1}} s_{2} = t$ : the predicted deletion is the deletion of the first letter.

1.2F1F4F5

The prefix reflections and the repeated one. Compute the prefix reflections of $(s, t, s, t)$ from $r_{i} = w_{i - 1} s_{i} w_{i - 1}^{- 1}$ with $w_{0} = 1$ , $w_{1} = s$ , $w_{2} = s t$ , $w_{3} = s t s$ : $r_{1} = s$ ; $r_{2} = s t s = s t s$ ; $r_{3} = (s t) s (s t)^{- 1} = s t s \cdot t s = s t s t s = (s t)^{2} s = t s \cdot s = t$ , where $(s t)^{- 1} = t s$ and $(s t)^{2} = (s t)^{- 1}$ because $s t$ has order $3$ [F1, F4]; and $r_{4} = (s t s) t (s t s) = s t s t s t s = (s t)^{3} s = s$ , using $(s t)^{3} = 1$ and $s^{2} = t^{2} = 1$ [F5]. Hence $r_{1} = r_{4} = s$ while $r_{2} = s t s$ and $r_{3} = t$ .

1.3F1F4

The deletion and the value identity. Since $r_{1} = r_{4}$ , [F1] (6)(a) with $i = 1$ , $j = 4$ gives $s t s t = \hat{s_{1}} t s \hat{s_{4}} = t s$ . Independently, $(s t)^{2} = (s t)^{- 1}$ because $s t$ has order $3$ [F1], and $(s t)^{- 1} = t^{- 1} s^{- 1} = t s$ [F4]; hence $s t s t = (s t)^{2} = t s$ , confirming that deleting the first and the last letter of $(s, t, s, t)$ preserves the value.

2.1F1F3F5step 1.2

The element and its reflection set. By step 1.3 the word $(s, t, s, t)$ represents $s t s t = t s$ and has length $4$ , while $ℓ (s t s t) = ℓ (t s) = 2$ by [F3] with $m = 3$ , $k = 2$ and $k = 1$ ; hence the word is not reduced. By [F1] (6)(b) the function $η (r, s t s t) = (- 1)^{n (r)}$ is expression-independent, so it may be computed from the word $(s, t, s, t)$ with the prefix reflections of step 1.2: of these $r_{1} = r_{4} = s$ occurs twice and $r_{2} = s t s$ , $r_{3} = t$ occur once each, so $Φ (s t s t) = {r \in T : η (r, s t s t) = - 1} = {s t s, t}$ has cardinality $2 = ℓ (s t s t)$ , in agreement with the cardinality forced for any reduced expression by [F1] (6)(c); in particular $s \notin Φ (s t s t)$ , and the two-letter deletion licensed by [F1] (6)(a) is the one deleting the equal reflections $r_{1} = r_{4}$ , not an arbitrary pair of equal letters. The last point: deleting the letters at positions $1$ and $3$ of $(s, t, s, t)$ leaves the word $(t, t)$ with value $t^{2} = 1$ [F5], and $1 \neq t s$ since $ℓ (1) = 0 \neq 2 = ℓ (t s)$ ; so that deletion does not preserve the value.

3.1step 1.1step 1.2step 1.3step 2.1∎

Collected. The example exhibits the exchange step of [F2] (2) in complete detail (step 1.1), a nonreduced word whose two equal prefix reflections $r_{1} = r_{4}$ license the deletion of its first and last letter (steps 1.2, 1.3), and the resulting expression-independent sign-change set $Φ (s t s t) = {s t s, t}$ together with a failed deletion of an unequal-reflection pair (step 2.1).

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

51 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

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