LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-27

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 adjacent-transposition words have well-defined positive lifts

Statement

Let $n \geq 2$ , let $S_{n}$ be the symmetric group on ${1, \dots, n}$ with the product convention of The symmetric group $Sym (X)$ : the bijections of a set $X$ under composition (the product of permutations acts with the right factor first, and permutations are composed as functions), let $s_{i} : = (i i + 1)$ be the adjacent transpositions. Transport the inversion convention of Inversions, inversion number, the sign $sgn (σ) = (- 1)^{inv (σ)}$ , and even and odd permutations from ${0, \dots, n - 1}$ by the increasing bijection $κ (j) = j - 1$ : for $σ \in S_{n}$ put $σ_{0} : = κ σ κ^{- 1}$ , $Inv (σ) : = {(a, b) : 1 \leq a < b \leq n, σ (a) > σ (b)}$ , and $inv (σ) : = ∣ Inv (σ) ∣$ . The map $(a, b) \mapsto (a - 1, b - 1)$ identifies this set with $Inv (σ_{0})$ of that definition, so the numbers agree. Let $B_{n}^{+}$ be the positive braid monoid of Positive braid monoid with atoms $σ_{i}$ , length $ℓ$ , and half twist $Δ$ of The Garside half twist and simple positive braids, of length $N = n (n - 1) / 2$ . A word $s_{i_{1}} ∣ s_{i_{2}} ∣ \dots ∣ s_{i_{k}}$ in the symbols $s_{1}, \dots, s_{n - 1}$ is reduced if $k$ is minimal among the words representing the permutation $s_{i_{1}} s_{i_{2}} \dots s_{i_{k}}$ .

(a) The type-A relations. $s_{i}^{2} = i d$ for all $i$ , $s_{i} s_{j} = s_{j} s_{i}$ whenever $∣ i - j ∣ > 1$ , and $s_{i} s_{i + 1} s_{i} = s_{i + 1} s_{i} s_{i + 1}$ whenever $1 \leq i \leq n - 2$ .

(b) The homomorphism to the symmetric group. There is a monoid homomorphism $π ⁣ : B_{n}^{+} \to S_{n}$ with $π (σ_{i}) = s_{i}$ , and it is surjective.

(c) The inversion calculus. For every $τ \in S_{n}$ and every $i$ , writing the inversion set as pairs of values, $E (τ) : = {{u, v} : u < v, τ^{- 1} (u) > τ^{- 1} (v)},$ one has $E (τ s_{i}) = E (τ) △ {{τ (i), τ (i + 1)}}$ , so that $inv (τ s_{i}) = inv (τ) + 1$ if $τ (i) < τ (i + 1)$ and $inv (τ s_{i}) = inv (τ) - 1$ otherwise; moreover $∣ E (τ) ∣ = inv (τ)$ and $inv (π (a)) \leq ℓ (a)$ for every $a \in B_{n}^{+}$ .

(d) The prefix invariant. For a word $w = s_{i_{1}} ∣ \dots ∣ s_{i_{k}}$ with prefix products $τ_{t} = s_{i_{1}} \dots s_{i_{t}}$ put $c_{t} : = {τ_{t - 1} (i_{t}), τ_{t - 1} (i_{t} + 1)}$ and $N (w) : = △_{t = 1}^{k} {c_{t}}$ . Then $N (w) = E (σ (w))$ where $σ (w)$ is the permutation represented by $w$ ; consequently $inv (σ (w)) = ∣ N (w) ∣ \leq k$ .

(e) Length equals inversion number. Every $σ \in S_{n}$ has minimal word length $∥ σ ∥ : = \min {k : σ = s_{i_{1}} \dots s_{i_{k}}}$ equal to $inv (σ)$ ; a word is reduced if and only if its length is $inv$ of the permutation it represents.

(f) Exchange. Let $w = s_{i_{1}} ∣ \dots ∣ s_{i_{k}}$ be reduced for $σ$ and let $j$ satisfy $σ (j) > σ (j + 1)$ . Then ${σ (j), σ (j + 1)}$ equals exactly one of the transpositions $c_{1}, \dots, c_{k}$ of (d), say $c_{r}$ , and deleting the $r$ -th letter gives a reduced word $s_{i_{1}} ∣ \dots ∣ \hat{s_{i_{r}}} ∣ \dots ∣ s_{i_{k}}$ for $σ s_{j}$ .

(g) Well-defined positive lifts. Any two reduced words for the same $σ \in S_{n}$ are connected by braid moves, that is, by replacements of a subword $s_{i} s_{i + 1} s_{i}$ by $s_{i + 1} s_{i} s_{i + 1}$ , and of a subword $s_{i} s_{j}$ by $s_{j} s_{i}$ for $∣ i - j ∣ > 1$ . Hence all reduced words for $σ$ represent one and the same element of $B_{n}^{+}$ , denoted $\hat{σ}$ ; the map $σ \mapsto \hat{σ}$ is injective, satisfies $π (\hat{σ}) = σ$ and $ℓ (\hat{σ}) = inv (σ) = ∥ σ ∥$ , and is a section of $π$ . In particular $\hat{s_{i}} = σ_{i}$ for every $i$ .

(h) The half twist. With $w_{0} : = σ \mapsto n + 1 - σ$ the longest element of $S_{n}$ , one has $π (Δ) = w_{0}$ , $inv (w_{0}) = N$ , and $Δ = \hat{w_{0}}$ .

For $n = 0, 1$ the group $S_{n}$ and the monoid $B_{n}^{+}$ are trivial, no generator occurs, and the statements are vacuous. No choice principle is used; the only imported statement is (g)'s braid-connectivity theorem, stated in [F4] below with its hypotheses checked.

Facts & Assumptions

Given: A natural number $n \geq 2$ , the symmetric group $S_{n}$ with its adjacent transpositions $s_{i}$ , the monoid $B_{n}^{+}$ with atoms $σ_{i}$ , length $ℓ$ and half twist $Δ$ , and the words over the alphabets ${s_{1}, \dots, s_{n - 1}}$ and ${σ_{1}, \dots, σ_{n - 1}}$ .

[F1]

$B_{n}^{+}$ is generated by the atoms $σ_{i}$ , with product $[u] [v] = [u v]$ , homogeneous length $ℓ ([w]) = ∣ w ∣$ , and the universal property: a monoid homomorphism out of $B_{n}^{+}$ is the same as a choice of elements satisfying the braid and commutation relations (Positive braid monoid, Positive artin relations preserve homogeneous length). The half twist is $Δ = [T_{1} T_{2} \dots T_{n - 1}]$ with $T_{k} = σ_{k} σ_{k - 1} \dots σ_{1}$ and $ℓ (Δ) = N = n (n - 1) / 2$ (The Garside half twist and simple positive braids).

[F2]

Permutations are composed as functions with the right factor first, $s_{i}$ is the transposition of $i$ and $i + 1$ , and $Inv (σ) = {(a, b) : a < b, σ (a) > σ (b)}$ with $inv (σ) = ∣ Inv (σ) ∣$ on the labels $1, \dots, n$ , transported along $κ$ as specified in the Statement (The symmetric group $Sym (X)$ : the bijections of a set $X$ under composition, Inversions, inversion number, the sign $sgn (σ) = (- 1)^{inv (σ)}$ , and even and odd permutations). The adjacent transpositions generate $S_{n}$ (The adjacent transpositions $(1 2), (2 3), \dots, (n - 1 n)$ generate $S_{n}$ ).

[F3]

The congruence $\equiv^{+}$ of $B_{n}^{+}$ contains every pair of words related by a braid move, that is, by replacing a subword $σ_{i} σ_{i + 1} σ_{i}$ with $σ_{i + 1} σ_{i} σ_{i + 1}$ , or a subword $σ_{i} σ_{j}$ with $σ_{j} σ_{i}$ for $∣ i - j ∣ > 1$ ; this is the definition of the defining pairs $R_{n}$ and of the congruence they generate (Positive braid monoid).

[F4]

Imported induction, with its inputs exposed. Dehornoy et al., Foundations of Garside Theory, Corollary IX.1.11(ii), printed p. 435, proves braid-connectivity of reduced expressions by induction from the exchange property in Proposition IX.1.10, printed p. 434. The extracted induction uses: (i) a length function for which all reduced expressions of one element have that length; (ii) exchange for a length-decreasing multiplication by a generator, on either side; and (iii) finite rank-two orders $m_{s, t}$ , so that the alternating words of length $m_{s, t}$ are related by a braid move. These inputs hold here: (i) is step 2.3; (ii) is step 3.2 on the right and its left-hand version follows by applying 3.2 to inverse permutations and reversed words; and (iii) is the direct permutation calculation of step 1.1, giving $m_{s_{i}, s_{j}} = 2$ when $∣ i - j ∣ > 1$ and $3$ when $∣ i - j ∣ = 1$ . We import only this exchange-to-connectivity induction, not a Coxeter presentation of $S_{n}$ ; the published thm-the-symmetric-group-has-the-coxeter-presentation is not used.

Proof

technique · direct

1.1

The type-A relations (a). The permutation $s_{i}$ swaps $i$ and $i + 1$ and fixes all other symbols, so $s_{i}^{2} = i d$ ; if $∣ i - j ∣ > 1$ the two transpositions move disjoint pairs of symbols, so $s_{i} s_{j} = s_{j} s_{i}$ ; and for $1 \leq i \leq n - 2$ both $s_{i} s_{i + 1} s_{i}$ and $s_{i + 1} s_{i} s_{i + 1}$ fix every $x \notin {i, i + 1, i + 2}$ and map $i \mapsto i + 2$ , $i + 1 \mapsto i + 1$ , $i + 2 \mapsto i$ , as one checks by applying the three transpositions in turn; hence they are equal. Moreover, for $∣ i - j ∣ > 1$ the product $s_{i} s_{j}$ is the product of two disjoint transpositions and has order $2$ , while $s_{i} s_{i + 1}$ is a three-cycle on ${i, i + 1, i + 2}$ and has order $3$ . These are the rank-two orders needed below.

F2algebra

1.2

The inversion calculus (c). Define $E (τ)$ as in the statement and let $p_{τ} : = τ^{- 1}$ be the position function, so that $(i, j) \in Inv (τ)$ if and only if ${τ (i), τ (j)} \in E (τ)$ , because $i = p_{τ} (τ (i))$ and $j = p_{τ} (τ (j))$ ; the map $(i, j) \mapsto {τ (i), τ (j)}$ is therefore a bijection $Inv (τ) \to E (τ)$ and $∣ E (τ) ∣ = inv (τ)$ . Right multiplication by $s_{i}$ exchanges the values at the positions $i$ and $i + 1$ and leaves all other values in place, so $p_{τ s_{i}}$ agrees with $p_{τ}$ except that the positions of the two values $u : = τ (i)$ , $v : = τ (i + 1)$ are interchanged; hence for a two-element set ${a, b} \neq {u, v}$ the comparison of $p (a)$ and $p (b)$ is unchanged, while the set ${u, v}$ itself is in $E (τ s_{i})$ if and only if it is not in $E (τ)$ , which gives $E (τ s_{i}) = E (τ) △ {{u, v}}$ . Consequently $inv (τ s_{i}) = inv (τ) \pm 1$ , and the sign is $+ 1$ exactly when ${u, v} \notin E (τ)$ , that is, when $τ (i) < τ (i + 1)$ .

F2algebra

2.1

The prefix invariant (d). For the empty word $N (ε) = \emptyset = E (i d)$ . If $w^{'} = w ∣ s_{i}$ and $N (w) = E (σ (w))$ by induction, then $σ (w^{'}) = σ (w) s_{i}$ and the definition gives $N (w^{'}) = N (w) △ {c}$ with $c = {σ (w) (i), σ (w) (i + 1)}$ , which equals $E (σ (w) s_{i}) = E (σ (w^{'}))$ by step 1.2. Hence $N (w) = E (σ (w))$ for every word, and $inv (σ (w)) = ∣ N (w) ∣ \leq k$ because $N (w)$ is a symmetric difference of $k$ two-element sets. Also every element $a \in B_{n}^{+}$ is $[w]$ for some word $w$ , so $inv (π (a)) \leq ℓ (a)$ once $π$ is available.

F2step 1.2

2.2

The homomorphism (b). By step 1.1 the elements $s_{1}, \dots, s_{n - 1} \in S_{n}$ satisfy the relations of the defining pairs $R_{n}$ of $B_{n}^{+}$ , so the universal property [F1] gives a monoid homomorphism $π ⁣ : B_{n}^{+} \to S_{n}$ with $π (σ_{i}) = s_{i}$ . It is surjective because the $s_{i}$ generate $S_{n}$ [F2] and each $s_{i} = π (σ_{i})$ .

F1F2step 1.1

2.3

Minimal length equals inversion number (e). Let $σ \in S_{n}$ and let $∥ σ ∥$ be its minimal word length. Every word of length $k$ representing $σ$ satisfies $inv (σ) \leq k$ by step 1.2 applied along the prefixes (each right multiplication by a generator changes the inversion number by exactly one, so it can increase it by at most one), whence $inv (σ) \leq ∥ σ ∥$ . Conversely we show $∥ σ ∥ \leq inv (σ)$ by induction on $inv (σ)$ : if $inv (σ) = 0$ then $σ (1) < σ (2) < \dots < σ (n)$ , so $σ = i d$ and $∥ σ ∥ = 0$ ; otherwise there is $j$ with $σ (j) > σ (j + 1)$ , step 1.2 gives $inv (σ s_{j}) = inv (σ) - 1$ , the induction hypothesis gives an expression of $σ s_{j}$ of length $inv (σ) - 1$ , and appending $s_{j}$ expresses $σ$ with $inv (σ)$ letters. Hence $∥ σ ∥ = inv (σ)$ , and a word is reduced exactly when its length equals the inversion number of the permutation it represents.

F2step 1.2

3.1

The bound for positive braids (c, second part). Let $a \in B_{n}^{+}$ and choose a word $w$ with $[w] = a$ . Then $π (a) = σ (w)$ and $ℓ (a) = ∣ w ∣$ , so step 2.1 gives $inv (π (a)) = ∣ N (w) ∣ \leq ∣ w ∣ = ℓ (a)$ .

F1step 2.1step 2.2

3.2

Exchange (f). Let $w = s_{i_{1}} ∣ \dots ∣ s_{i_{k}}$ be reduced for $σ$ and let $σ (j) > σ (j + 1)$ ; by step 2.3 $k = inv (σ) = ∣ E (σ) ∣ = ∣ N (w) ∣$ , so the $k$ sets $c_{1}, \dots, c_{k}$ of step 2.1 are pairwise distinct and $N (w) = ⋃_{t} {c_{t}}$ : if two of them coincided, the symmetric difference would have fewer than $k$ elements. The set $c^{*} : = {σ (j), σ (j + 1)}$ lies in $E (σ)$ , because with $u : = σ (j + 1) < σ (j) = : v$ one has $p_{σ} (u) = j + 1 > j = p_{σ} (v)$ ; hence $c^{*} = c_{r}$ for exactly one $r$ . Write $w = p ∣ s_{i_{r}} ∣ q$ and $ρ : = σ (p)$ , so $σ = ρ s_{i_{r}} σ (q)$ and $c_{r} = {ρ (i_{r}), ρ (i_{r} + 1)}$ . Let $t_{c_{r}}$ be the transposition of these two values. Deleting the $r$ -th letter gives $w^{(r)} = p ∣ q$ and therefore $σ (w^{(r)}) = ρ σ (q) = (ρ s_{i_{r}} ρ^{- 1}) σ = t_{c_{r}} σ$ . Because $c_{r} = {σ (j), σ (j + 1)}$ , the same transposition is $t_{c_{r}} = σ s_{j} σ^{- 1}$ , so $σ (w^{(r)}) = σ s_{j}$ . Now step 2.1 gives $N (w^{(r)}) = E (σ s_{j}) = E (σ) △ {c_{r}}$ ; the equality of these $N$ -sets follows from the permutation calculation, not from simply deleting one crossing label (later prefix labels may change). Finally the deleted word has length $k - 1 = inv (σ s_{j})$ , so it is reduced by step 2.3.

F2step 1.2step 2.1step 2.3

3.3

Well-defined lifts (g). Let $w, w^{'}$ be reduced words for the same $σ$ . By [F4] they are connected by braid moves on the symbols $s_{i}$ , and by [F3] each such move replaces a word by an $\equiv^{+}$ -equivalent word, since the braid move $σ_{i} σ_{i + 1} σ_{i} \leftrightarrow σ_{i + 1} σ_{i} σ_{i + 1}$ and the far-commutation move are exactly the defining pairs $R_{n}$ (note that $m_{s, t} \in {2, 3}$ for type A by step 1.1, so the imported induction's braid relations are precisely these two families). Hence $w \equiv^{+} w^{'}$ and $[w] = [w^{'}]$ ; call this common class $\hat{σ}$ . Then $π (\hat{σ}) = π ([w]) = σ (w) = σ$ , and $ℓ (\hat{σ}) = ∣ w ∣ = inv (σ) = ∥ σ ∥$ by step 2.3, so $\hat{\cdot}$ is a section of $π$ and injective; for a generator, $s_{i}$ has the reduced word of length one, so $\hat{s_{i}} = σ_{i}$ .

F1F3F4step 1.1step 2.2step 2.3

4.1

The half twist represents the longest element (h). Put $c_{k} : = s_{k} s_{k - 1} \dots s_{1}$ , so that $π (T_{k}) = c_{k}$ by step 2.2 and $π (Δ) = c_{1} c_{2} \dots c_{n - 1}$ . First, $c_{k}$ maps $1 \mapsto k + 1$ , $j \mapsto j - 1$ for $2 \leq j \leq k + 1$ , and fixes every $x > k + 1$ : for $k = 1$ this is the transposition $s_{1}$ , and the step from $k - 1$ to $k$ uses $c_{k} = s_{k} c_{k - 1}$ , which sends $1 \mapsto s_{k} (k) = k + 1$ , sends $2 \leq j \leq k$ to $s_{k} (j - 1) = j - 1$ , sends $k + 1$ to $s_{k} (k + 1) = k$ , and fixes $x > k + 1$ . Second, $P_{k} : = c_{1} c_{2} \dots c_{k}$ maps $x \mapsto k + 2 - x$ for $1 \leq x \leq k + 1$ and fixes $x > k + 1$ : for $k = 1$ this is $c_{1}$ , and using $P_{k} = P_{k - 1} c_{k}$ one computes $P_{k} (1) = P_{k - 1} (k + 1) = k + 1$ , $P_{k} (x) = P_{k - 1} (x - 1) = k + 2 - x$ for $2 \leq x \leq k$ , $P_{k} (k + 1) = P_{k - 1} (k) = 1$ , and $P_{k} (x) = x$ for $x > k + 1$ . Hence $π (Δ) = P_{n - 1} = w_{0}$ with $w_{0} (x) = n + 1 - x$ , and $inv (w_{0}) = N$ because every pair $a < b$ has $w_{0} (a) > w_{0} (b)$ ; by step 2.3, $∥ w_{0} ∥ = N = ℓ (Δ)$ , so the defining word of $Δ$ is reduced for $w_{0}$ and $Δ = \hat{w_{0}}$ by step 3.3.

F1F2step 2.2step 2.3step 3.3

5.1

Assembly. Part (a) is step 1.1, part (b) is step 2.2, part (c) is steps 1.2, 2.1 and 3.1, part (d) is step 2.1, part (e) is step 2.3, part (f) is step 3.2, part (g) is step 3.3, and part (h) is step 4.1. The exchange lemma (f) and the invariant (d) are proved here from the inversion calculus, so the only imported ingredient is the braid-connectivity of reduced words [F4]; its hypotheses are the three families verified in step 1.1. For $n \leq 1$ there are no generators: $S_{n}$ and $B_{n}^{+}$ are trivial, and all assertions are vacuous. Every argument is a finite computation or an induction on a natural number, and no choice principle is used. ∎

step 1.1step 1.2step 2.1step 2.2step 2.3step 3.1step 3.2step 3.3step 4.1

Remarks

What is imported, and what is not. The single imported statement is Matsumoto's braid-connectivity of reduced words for type A, quoted in [F4] from Dehornoy et al., Corollary IX.1.11(ii) (printed p. 435); the source derives it by an induction from the exchange property (Proposition IX.1.10, printed p. 434) and the reflection invariant of Lemma IX.1.7--1.9. Both inputs of that induction -- equal lengths of reduced words for one element, and the exchange property -- are re-proved here in steps 2.3 and 3.2, so no appeal to the type-A Coxeter presentation is involved. The exchange lemma itself (part (f)), the prefix invariant (part (d)), and the equality of the length with the inversion number (part (e)) are proved here, by the inversion bookkeeping that the plan of this page asked for: the letter to be deleted is the unique crossing whose associated transposition is the descent pair ${σ (j), σ (j + 1)}$ , and no square-deletion move (which is not a relation of $B_{n}^{+}$ ) is used anywhere.
Why well-definedness is the hard point. The map $π ⁣ : B_{n}^{+} \to S_{n}$ is easy, but it is far from injective: its fibres are infinite for $n \geq 2$ . The lift $\hat{\cdot}$ goes the other way and exists only because all reduced expressions of a permutation are related by the defining relations of $B_{n}^{+}$ ; this is why the type-A Coxeter presentation theorem is not needed here in full, only the braid-connectivity of reduced words.
Consequences used below. Part (c) is what makes $inv (π (a)) \leq ℓ (a)$ available for arbitrary positive braids, which is the inequality used in Simple positive braids are indexed by permutations; part (h) identifies $Δ$ with the lift of the longest element, which is what makes the divisors of $Δ$ correspond to permutations. No geometry of the symmetric group is used: only the transposition action on ${1, \dots, n}$ .
Nothing here uses a choice principle: all words are finite, the minimal word length is a minimum over a nonempty set of natural numbers, and the symmetric difference $N (w)$ is computed from a fixed word.

Depends on

Used by

Exponent sum is not a complete braid normal form Counterexample
The standard type-A reflection realization and its polynomial ring Definition
A left garside normal form computation in b three Example
The full twist in b three Example
The simple braids and divisibility lattice for b three Example
A central positive braid is a power of delta squared for n greater than two Lemma
Simple positive braids are indexed by permutations Lemma
Type-A reduced words and the Coxeter presentation Lemma

Dependency tree · two levels

21 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

Patrick Dehornoy et al., Foundations of Garside Theory, Chapter IX, Proposition 1.10 (exchange) and Corollary 1.11(ii) (Matsumoto), printed pp. 434-435 (standard reference, not scraped)
M. Macauley, Math 4120 lecture notes: Generating sets for S_n (standard reference, not scraped)