ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedjudge 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.

Bruhat versus weak comparability in S4

Example

Let $W = S_{4}$ with $ℓ$ the inversion number (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (4)). Besides the Bruhat order (The Bruhat graph by length-increasing reflection chains, the Bruhat order, inversion symmetry, and reflection parity) consider the two weak relations defined by length-increasing simple multiplications: put $u \leq_{R} v$ if there are $u_{0}, \dots, u_{k} \in W$ with $u_{0} = u$ , $u_{k} = v$ and $u_{j + 1} = u_{j} s_{i_{j}}$ for a simple generator with $ℓ (u_{j + 1}) > ℓ (u_{j})$ ; and $u \leq_{L} v$ if $u_{j + 1} = s_{i_{j}} u_{j}$ with the same length condition. (These are the right and left weak orders of $(W, S)$ ; their systematic theory belongs to a later pair of this track and is not needed for the comparisons below.)

(i) $u = 2143$ and $v = 2341$ satisfy $u \leq v$ in Bruhat order but neither $u \leq_{R} v$ nor $u \leq_{L} v$ : $u = s_{1} s_{3}$ is the subword at positions $1, 3$ of $v = s_{1} s_{2} s_{3}$ , while $ℓ (v) - ℓ (u) = 1$ and none of the six products $u s_{i}$ , $s_{i} u$ ( $i = 1, 2, 3$ ) equals $2341$ .

(ii) Weak comparability implies Bruhat comparability. Indeed every right- or left-weak step with increasing length is a Bruhat edge, because a simple generator is a reflection ( $s = 1 \cdot s \cdot 1^{- 1} \in T$ ) and, for the left version, left multiplication by a reflection of increasing length is a Bruhat edge (clauses (1) and (3) of The Bruhat graph by length-increasing reflection chains, the Bruhat order, inversion symmetry, and reflection parity); hence $u \leq_{R} v$ or $u \leq_{L} v$ implies $u \leq v$ . For example $1234 \leq_{R} 2134 \leq_{R} 2314 \leq_{R} 2341$ , and the same chain is a Bruhat chain.

(iii) The converse of (ii) fails: by (i), Bruhat comparability is strictly weaker than comparability in either weak order already in $S_{4}$ .

Facts & Assumptions

Given: $W = S_{4}$ with generators $s_{1}, s_{2}, s_{3}$ , the elements $u = 2143$ , $v = 2341$ and the weak relations $\leq_{R}$ , $\leq_{L}$ of the statement.

[F1]

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

[F2]

One-line notation lists the values of a permutation in order of the arguments, and the composition convention is $(σ τ) (i) = σ (τ (i))$ ; hence right multiplication by $s_{i} = (i i + 1)$ swaps the entries in positions $i$ and $i + 1$ , and left multiplication swaps the values $i$ and $i + 1$ . (The finite symmetric group $S_{n}$ , one-line notation, and cycle notation)

[F3]

The inversion number of $σ$ is $inv (σ) = ∣ {(i, j) : i < j, σ (i) > σ (j)} ∣$ . (Inversions, inversion number, the sign $sgn (σ) = (- 1)^{inv (σ)}$ , and even and odd permutations)

[F4]

Bruhat edges: $x \to y$ if and only if $y = x t$ for some $t \in T$ with $ℓ (y) > ℓ (x)$ ; the reflections are $T = {w s w^{- 1} : w \in W, s \in S}$ , so every simple generator is a reflection; and if $x \in W$ , $t \in T$ satisfy $ℓ (t x) > ℓ (x)$ , then $x \to t x$ . (The Bruhat graph by length-increasing reflection chains, the Bruhat order, inversion symmetry, and reflection parity (1), (3))

[F5]

Subword criterion: for a reduced expression $v = r_{1} \dots r_{q}$ and $x \in W$ , one has $x \leq v$ if and only if there are $1 \leq i_{1} < \dots < i_{k} \leq q$ with $x = r_{i_{1}} \dots r_{i_{k}}$ , and the indices may be chosen with $k = ℓ (x)$ . (The subword characterization of Bruhat order and its independence of the reduced expression (1))

Verification

1.1F1F2F3F5

For the Bruhat relation in (i): $u = s_{1} s_{3}$ is the value of the subword at positions $1, 3$ of the word $s_{1} s_{2} s_{3}$ , and $2341 = s_{1} s_{2} s_{3}$ because right multiplying the identity by $s_{1}, s_{2}, s_{3}$ in turn gives $2134, 2314, 2341$ by [F2]; both words are reduced, since their lengths $2$ and $3$ equal the inversion numbers of their values $2143$ and $2341$ by [F1] and [F3]. The subword criterion [F5] therefore gives $u \leq v$ .

1.2F3F4

For (ii): a right-weak step $x \to x s_{i}$ with $ℓ (x s_{i}) > ℓ (x)$ is a Bruhat edge because $s_{i} \in S \subseteq T$ by [F4]; a left-weak step $x \to s_{i} x$ with $ℓ (s_{i} x) > ℓ (x)$ is a Bruhat edge by the left-multiplication clause of [F4]. Chains of Bruhat edges are Bruhat chains, so $u \leq_{R} v$ or $u \leq_{L} v$ implies $u \leq v$ ; in particular the chain $1234 \to 2134 \to 2314 \to 2341$ is a chain of $R$ -steps with increasing lengths (each step applies $s_{1}$ , $s_{2}$ , $s_{3}$ in turn and raises the inversion number by $1$ by [F1], [F2], [F3]), so $1234 \leq_{R} 2134 \leq_{R} 2314 \leq_{R} 2341$ and the same four elements form a Bruhat chain.

2.1F2step 1.1

For the weak relations in (i): a chain realizing $u \leq_{R} v$ or $u \leq_{L} v$ has steps of length increase at least $1$ , so a chain with $k$ steps satisfies $ℓ (v) \geq ℓ (u) + k$ , that is, $k \leq ℓ (v) - ℓ (u) = 3 - 2 = 1$ ; since $u \neq v$ at least one step is needed, so exactly one step occurs and $v = u s_{i}$ (for $\leq_{R}$ ) or $v = s_{i} u$ (for $\leq_{L}$ ) with $ℓ$ increasing. The six products, computed by the position- and value-swapping rules of [F2], are $u s_{1} = 1243$ , $u s_{2} = 2413$ , $u s_{3} = 2134$ , $s_{1} u = 1243$ , $s_{2} u = 3142$ and $s_{3} u = 2134$ , and none of them equals $2341$ ; hence neither $u \leq_{R} v$ nor $u \leq_{L} v$ holds.

3.1step 1.2step 2.1∎

For (iii): step 2.1 exhibits $u \leq v$ in Bruhat order together with the failure of both $u \leq_{R} v$ and $u \leq_{L} v$ , so the converse of the implication proved in step 1.2 fails, in the sharp form that Bruhat comparability does not imply comparability in either weak order already in $S_{4}$ . All assertions are finite computations in $S_{4}$ and use no choice principle.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

42 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 (Graduate Texts in Mathematics 231, Springer 2005; author-hosted complete PDF) (standard reference, not scraped)
Grant T. Barkley, Bruhat order and applications, Lecture 3 (CMND lecture notes, author-hosted) (standard reference, not scraped)