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 in rank one

Example

Let $S = {s}$ and $m (s, s) = 1$ , so that the relator set of the presentation of Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups is $R = {s^{2}}$ and $W = F ({s}) / ⟨ ⁣ ⟨ s^{2} ⟩ ⁣ ⟩$ . Then:

Every element of $W$ is $1$ or $s$ , with $s^{2} = 1$ and $s \neq 1$ ; hence $W ≅ Z / 2$ .
$ℓ (1) = 0$ and $ℓ (s) = 1$ .
A word $(s, \dots, s)$ of length $k$ has value $s^{k}$ , which is $1$ for even $k$ and $s$ for odd $k$ . Hence the only reduced words are the empty word $()$ for $1$ and the word $(s)$ for $s$ , and every word of length $k \geq 2$ is nonreduced and reduces to a reduced word by repeated deletion of two letters.
The reflection set is $T = {s}$ , the root set is $Φ = {α_{s}, - α_{s}}$ (because $σ_{s} (α_{s}) = - α_{s}$ ), and the signed action on ${\pm 1} \times {s}$ is $(ε, s) \cdot s = (- ε, s)$ , which is faithful.

Facts & Assumptions

Given: The Coxeter matrix on $S = {s}$ with $m (s, s) = 1$ ; the presented group $W$ with its length $ℓ$ of Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups; the field $K$ of characteristic $0$ , the space $E$ with basis $(α_{s})$ and the involution $σ_{s}$ of The geometric representation on the simple-root basis over a common splitting field, and the root set; the reflection set $T$ with the right action of $W$ on ${\pm 1} \times T$ of The rank-two block computation, exact dihedral orders, the signed reflection action, and ambient reducedness; and the deletion and faithfulness statements of Length parity, exchange, two-letter deletion, and faithfulness of the signed reflection action.

[F1]

Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups: the relator set is " $R : = {s^{2} : s \in S} \cup {(s t)^{m (s, t)} : s, t \in S, m (s, t) < \infty}$ " with " $N : = ⟨ ⁣ ⟨ R ⟩ ⁣ ⟩_{F (S)}$ " its normal closure, and "Define $W : = F (S) / N,$ and write $s$ (as well as $s N$ ) for the image of $s \in S$ in $W$ "; the length is " $ℓ (w) : = \min {k \in N : there exist s_{1}, \dots, s_{k} \in S with w = s_{1} \dots s_{k}}$ ", and "the empty word $()$ is a word in $S$ of length $0$ , and $ℓ (1) = 0$ ; it is the reduced expression of $1$ ".

[F2]

The geometric representation on the simple-root basis over a common splitting field, and the root set: "The prime subfield of $K$ is $Q$ " and " $char K = 0$ "; the maps satisfy " $σ_{s} (α_{s}) = - α_{s}, σ_{s} (α_{t}) = α_{t} + c_{s t} α_{s} (t \neq s)$ ", and the root set is " $Φ : = {σ_{s_{1}} σ_{s_{2}} \dots σ_{s_{k}} (α_{t}) : k \geq 0, s_{1}, \dots, s_{k}, t \in S} \subseteq E$ ".

[F3]

The rank-two block computation, exact dihedral orders, the signed reflection action, and ambient reducedness: " $σ_{s}^{2} = {i d}_{E}$ for every $s \in S$ ; each $σ_{s}$ is invertible, and $ℓ (s) = 1$ ."; the reflection set is " $T : = {w s w^{- 1} : w \in W, s \in S} \subseteq W$ "; and "Then $U_{s}^{2} = i d$ for every $s$ , and the assignment $(ε, r) \cdot s : = U_{s} (ε, r)$ extends to a well-defined right action of $W$ on ${\pm 1} \times T$ ".

[F4]

Length parity, exchange, two-letter deletion, and faithfulness of the signed reflection action: "Hence repeated deletion of two letters transforms every word into a reduced expression for the same element, and a word is reduced if and only if it cannot be shortened by deleting two letters."; and "The right action of $W$ on ${\pm 1} \times T$ is faithful".

Verification

technique · direct computation in the rank-one presentation, with the general deletion and faithfulness statements applied to it

1.1F1F3

The group and its two elements. The relation $s^{2} = 1$ holds in $W$ because $s^{2} \in R \subseteq N$ [F1]. Every element of $W$ is the image of a product of the generator $s$ and its inverse, and $s^{- 1} = s$ in $W$ , so every element is a power $s^{k}$ with $k \geq 0$ ; since $s^{k}$ is $1$ for even $k$ and $s$ for odd $k$ , one has $W = {1, s}$ . By [F1] $ℓ (1) = 0$ and by [F3] $ℓ (s) = 1$ , so $s \neq 1$ , and the bijection $W \to Z / 2$ with $1 \mapsto 0$ , $s \mapsto 1$ is a homomorphism; hence $W ≅ Z / 2$ .

2.1F1F3F4step 1.1

Word values and reduced words. A word $(s, \dots, s)$ of length $k$ has value $s^{k}$ , which is $1$ for even $k$ and $s$ for odd $k$ by step 1.1; in particular $()$ has value $1$ and $(s)$ has value $s$ with lengths $0 = ℓ (1)$ and $1 = ℓ (s)$ [F1, F3], so both are reduced. If $k \geq 2$ , the word of length $k$ has value of length at most $1 < k$ , so it is not reduced; by [F4] it admits a deletion of two letters with the same value, and iterating this deletion, the length drops by two each time until the word has length $ℓ (1)$ or $ℓ (s)$ , namely until it is $()$ or $(s)$ . Hence the only reduced words are $()$ and $(s)$ .

3.1F2F3F4∎

Reflections, roots and the signed action. Since $W$ is abelian and $T = {w s w^{- 1} : w \in W, s \in S}$ , the reflection set is $T = {s}$ [F3, step 1.1]. By [F3] the group generated by $σ_{s}$ is ${1, σ_{s}}$ , so the root set of [F2] is $Φ = {α_{s}, σ_{s} (α_{s})} = {α_{s}, - α_{s}}$ , and these two vectors are distinct: $α_{s} = - α_{s}$ would give $2 α_{s} = 0$ , while the basis vector $α_{s}$ is nonzero and $char K = 0$ [F2]. For $r = s$ the formula of [F3] gives $(ε, s) \cdot s = U_{s} (ε, s) = (ε (- 1)^{δ (s, s)}, s s s) = (- ε, s)$ , and this action is faithful by [F4].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

56 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)