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.

Type-A reduced words and inversion numbers in $S_{3}$

Example

Let $n = 3$ , so $S = {s_{1}, s_{2}}$ with $m (s_{1}, s_{2}) = 3$ , and let $W ≅ S_{3}$ be the identification of Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (4) sending $s_{1} \mapsto (1 2)$ and $s_{2} \mapsto (2 3)$ . As on the published examples pages, permutations are displayed on the letters ${1, 2, 3}$ , identified with the library's ${0, 1, 2}$ by the order-preserving letter shift $j \mapsto j - 1$ (The finite symmetric group $S_{n}$ , one-line notation, and cycle notation); the shift preserves the order, hence preserves inversion numbers and lengths (Inversions, inversion number, the sign $sgn (σ) = (- 1)^{inv (σ)}$ , and even and odd permutations). Then $ℓ (w) = inv (φ (w))$ for all $w \in W$ , and the six elements of $W$ and their data are:

$w$	permutation	length $ℓ (w)$	inversion number
$1$	$i d$	$0$	$0$
$s_{1}$	$(1 2)$	$1$	$1$
$s_{2}$	$(2 3)$	$1$	$1$
$s_{1} s_{2}$	$(1 2 3)$	$2$	$2$
$s_{2} s_{1}$	$(1 3 2)$	$2$	$2$
$s_{1} s_{2} s_{1} = s_{2} s_{1} s_{2}$	$(1 3)$	$3$	$3$

Consequently: the words $(s_{1}, s_{2})$ , $(s_{2}, s_{1})$ and $(s_{1}, s_{2}, s_{1})$ are reduced, the two reduced expressions $s_{1} s_{2} s_{1}$ and $s_{2} s_{1} s_{2}$ of the longest element are related by the braid move, and the word $(s_{1}, s_{2}, s_{1}, s_{2})$ of length $4$ is nonreduced: it represents $s_{2} s_{1}$ (inversion number $2$ ) and deleting its first and last letters gives the reduced word $(s_{2}, s_{1})$ .

Facts & Assumptions

Given: The type-A Coxeter matrix on $S = {s_{1}, s_{2}}$ with $m (s_{1}, s_{2}) = 3$ ; the presented group $W$ with its length $ℓ$ of Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups; the isomorphism $W \to S_{3}$ with $ℓ = inv$ and the relators of the presentation from Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (4); the rank-two length formula of the dihedral specialisation Reduced words and lengths in a finite dihedral group (3); and the deletion statement of Length parity, exchange, two-letter deletion, and faithfulness of the signed reflection action.

[F1]

Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (4): for the type-A matrix, " $s_{i} \mapsto (i i + 1)$ extends to an isomorphism $W \to S_{n}$ , and for every $w \in W$ , $ℓ (w) = inv (φ (w))$ "; and "a word in the $s_{i}$ is reduced if and only if its length equals the inversion number of its value".

[F2]

The finite symmetric group $S_{n}$ , one-line notation, and cycle notation: $S_{n} = Sym ({0, 1, \dots, n - 1})$ with composition $(σ τ) (i) = σ (τ (i))$ , so the right factor acts first, and "An element of $S_{n}$ is named by either of the two notations below", one-line notation $[σ (0), \dots, σ (n - 1)]$ and cycle notation.

[F3]

Inversions, inversion number, the sign $sgn (σ) = (- 1)^{inv (σ)}$ , and even and odd permutations: "An inversion of $σ$ is a pair $(i, j)$ with $i < j < n$ and $σ (i) > σ (j)$ ", and $inv (σ) : = ∣ Inv (σ) ∣$ .

[F4]

Reduced words and lengths in a finite dihedral group (3): with $m = 3$ the formulae " $ℓ ((s t)^{k}) = \min (2 k, 2 (m - k))$ " and " $ℓ ((s t)^{k} s) = \min (2 k + 1, 2 (m - k) - 1)$ " give, for the rotation values $k = 0, 1, 2, 3$ and the reflection values $k = 0, 1, 2$ , the lengths $0, 2, 2, 0$ and $1, 3, 1$ ; the maximum is $3$ , attained only by $(s t)^{1} s$ , and the same values hold after interchanging the roles of $s$ and $t$ . In particular $ℓ (s_{1}) = ℓ (s_{2}) = 1$ , $ℓ (s_{1} s_{2}) = ℓ (s_{2} s_{1}) = 2$ and $ℓ (s_{1} s_{2} s_{1}) = 3$ , and the element $s_{1} s_{2} s_{1}$ , which also equals the alternating word $s_{2} s_{1} s_{2}$ of length $3$ , is the unique longest element of $W$ .

[F5]

Length parity, exchange, two-letter deletion, and faithfulness of the signed reflection action (3): "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."

Verification

technique · direct multiplication in $S_3$, with the lengths read off from the inversion-number identification of the type-A theorem

1.1F2

The six products. Multiplying in $S_{3}$ with the right factor acting first [F2]: $s_{1} s_{2} = (1 2) (2 3) = (1 2 3)$ , since the right factor $(2 3)$ sends $2 \mapsto 3$ and $3 \mapsto 2$ and the left factor $(1 2)$ then sends $1 \mapsto 2$ , giving $1 \mapsto 2 \mapsto 3 \mapsto 1$ ; and symmetrically $s_{2} s_{1} = (2 3) (1 2) = (1 3 2)$ . Further $s_{1} s_{2} s_{1} = (1 2) (2 3) (1 2) = (1 3)$ and $s_{2} s_{1} s_{2} = (2 3) (1 2) (2 3) = (1 3)$ , so the two length-three words have the same value. The six values $i d$ , $(1 2)$ , $(2 3)$ , $(1 2 3)$ , $(1 3 2)$ , $(1 3)$ are exactly the six elements of $S_{3}$ , so the images of the six words of the table are correct.

2.1F1F3step 1.1

The inversion numbers. Read the inversions of each value off its one-line form on the letters $1 < 2 < 3$ [F3]: $i d = [1, 2, 3]$ and $(1 2) = [2, 1, 3]$ , $(2 3) = [1, 3, 2]$ have inversion numbers $0, 1, 1$ ; the $3$ -cycles $(1 2 3) = [2, 3, 1]$ and $(1 3 2) = [3, 1, 2]$ have inversion numbers $2$ and $2$ ; and $(1 3) = [3, 2, 1]$ has all three pairs inverted, so its inversion number is $3$ . Hence the inversion-number column of the table is $(0, 1, 1, 2, 2, 3)$ , and the length column is the same by [F1].

3.1F1F4step 1.1step 2.1

Reducedness of the short words and the braid move. By step 2.1, $ℓ (s_{1} s_{2}) = 2$ and $ℓ (s_{2} s_{1}) = 2$ equal the lengths of the words $(s_{1}, s_{2})$ and $(s_{2}, s_{1})$ , so both are reduced; likewise $ℓ (s_{1} s_{2} s_{1}) = ℓ (s_{2} s_{1} s_{2}) = 3$ equals the length of the words $(s_{1}, s_{2}, s_{1})$ and $(s_{2}, s_{1}, s_{2})$ , so both are reduced expressions of the common element $s_{1} s_{2} s_{1} = s_{2} s_{1} s_{2} = (1 3)$ of step 1.1. By [F4] the maximum of $ℓ$ on $W$ is $3$ , attained only by the two equal alternating words of length $3$ , so this common element is the unique longest element of $W$ and its two reduced expressions are the two alternating words; the replacement of $(s_{1}, s_{2}, s_{1})$ by $(s_{2}, s_{1}, s_{2})$ is the single braid move exchanging the two alternating words of length $m (s_{1}, s_{2}) = 3$ .

4.1F5step 2.1step 3.1

The nonreduced word and its deletion. For the word $(s_{1}, s_{2}, s_{1}, s_{2})$ one computes in $W$ , using $s_{2}^{2} = 1$ , that $s_{1} s_{2} s_{1} s_{2} = (s_{1} s_{2} s_{1}) s_{2} = (s_{2} s_{1} s_{2}) s_{2} = s_{2} s_{1}$ , by the relation $s_{1} s_{2} s_{1} = s_{2} s_{1} s_{2}$ of the type-A presentation; the value $s_{2} s_{1}$ has inversion number $2 < 4$ by step 2.1, so the word is not reduced. Its first and last letters are $s_{1}$ and $s_{2}$ , and deleting them leaves the word $(s_{2}, s_{1})$ , which represents $s_{2} s_{1}$ and is reduced by step 3.1; this is the two-letter deletion asserted in [F5], here deleting the two letters at positions $1$ and $4$ .

5.1step 1.1step 2.1step 3.1step 4.1∎

Collected. The table and the length identification (steps 1.1, 2.1) verify $ℓ = inv$ on all six elements of the type-A group and exhibit the two reduced expressions of the longest element (step 3.1) together with a nonreduced word whose first and last letters may be deleted (step 4.1).

Depends on

Used by

Minimal coset representatives of S₂ in S₃ Example

Dependency tree · two levels

54 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, Springer GTM 231 (2005) (complete author/class-hosted PDF) (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)

Type-A reduced words and inversion numbers in S3S3​