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.

Infinite dihedral type: lower intervals are chains, but the two atoms have no upper bound

Example

Let $S = {s, t}$ with $s \neq t$ and $m (s, t) = \infty$ (infinite dihedral type), let $W$ be the presented group with length $ℓ$ , and let $\leq_{R}, \leq_{L}$ be the weak orders of The right and left weak orders, intervals, covers, and meets and joins of subsets. For $q \geq 1$ let $a_{q}$ (respectively $b_{q}$ ) be the value of the alternating word of length $q$ beginning with $s$ (respectively with $t$ ). Then:

(1) Alternating structure. Every reduced expression of an element of $W$ is alternating, and every element of $W$ has exactly one reduced expression: two alternating words of the same length beginning with the same letter are equal, and if two alternating words of length $q$ beginning with different letters represented the same element, then for even $q$ one would have $(s t)^{q / 2} = (s t)^{- q / 2}$ and for odd $q$ one would have $(s t)^{q - 1} = t s = (s t)^{- 1}$ , and each identity gives $(s t)^{q} = 1$ , which is false because $s t$ has infinite order by The rank-two block computation, exact dihedral orders, the signed reflection action, and ambient reducedness (4). Consequently $(s t)^{k} \neq 1$ for every $k \neq 0$ and the powers $(s t)^{k}$ ( $k \in Z$ ) are pairwise distinct, so $W$ is infinite.

(2) Every lower interval is a chain. For every $v \in W$ the interval $[1, v]_{R}$ is the finite chain consisting of the values of the distinct prefixes of the unique alternating reduced expression of $v$ : in particular

$[1, s t s]_{R} = {1, s, s t, s t s}, [1, t s]_{R} = {1, t, t s} .$

Meets and joins of nonempty subsets of these intervals are their least and greatest elements, e.g. $s \land s t = s$ and $s \lor s t = s t$ ; and the interval translation of The length identity, the prefix property, left translation, and interval translation for weak order (4) gives the order isomorphism $[s, s t s]_{R} = {s, s t, s t s} \to [1, t s]_{R} = {1, t, t s}$ , $x \mapsto s x$ .

(3) The two atoms have no join. The elements $s$ and $t$ are incomparable in both orders, and ${s, t}$ has no upper bound: if $z$ were an upper bound, then by the prefix property both $s$ and $t$ would be the first letter of a reduced expression of $z$ , so $z = a_{q} = b_{q}$ with $q = ℓ (z)$ , contradicting (1). Hence $s \lor t$ does not exist, $W$ is not a lattice, and every nonempty subset of $[1, s t s]_{R}$ is bounded above (by $s t s$ ) and therefore has a join by Weak order is a meet-semilattice, finite Coxeter groups are lattices, and joins of simple reflections exist exactly for finite parabolics (1), while the empty subset also has the join $1$ , the least element of $\leq_{R}$ ; the example thus shows that the boundedness hypothesis there cannot be dropped.

Facts & Assumptions

Given: $S = {s, t}$ with $s \neq t$ and $m (s, t) = \infty$ , the presented group $W$ with length $ℓ$ , weak orders $\leq_{R}, \leq_{L}$ as in The right and left weak orders, intervals, covers, and meets and joins of subsets, and the alternating-word values $a_{q}, b_{q}$ for $q \geq 1$ .

[F1]

Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups: $ℓ (w)$ is the minimum length of a word in $S$ representing $w$ , and a reduced expression is a word whose length equals $ℓ (w)$ .

[F2]

Length parity, exchange, two-letter deletion, and faithfulness of the signed reflection action (3): if a word in $S$ is not reduced, then deleting a suitable pair of its letters leaves the value unchanged; hence a reduced word cannot be shortened by deleting two letters.

[F3]

The rank-two block computation, exact dihedral orders, the signed reflection action, and ambient reducedness (4): for distinct $s, t \in S$ , $s \neq t$ in $W$ and $s t$ has order exactly $m (s, t)$ , infinite here.

[F4]

The right and left weak orders, intervals, covers, and meets and joins of subsets (1): $u \leq_{R} v$ iff $v = u x$ with $ℓ (v) = ℓ (u) + ℓ (x)$ .

[F5]

The length identity, the prefix property, left translation, and interval translation for weak order (2): $u \leq_{R} v$ iff some reduced expression of $v$ has a reduced expression of $u$ as its initial segment.

[F6]

Weak order is a meet-semilattice, finite Coxeter groups are lattices, and joins of simple reflections exist exactly for finite parabolics (1): a nonempty subset of $W$ has a join if and only if it is bounded above, in which case the join exists.

[F7]

The rank-two block computation, exact dihedral orders, the signed reflection action, and ambient reducedness (1): $ℓ (u) = 1$ for every $u \in S$ .

[F8]

The rank-two block computation, exact dihedral orders, the signed reflection action, and ambient reducedness (7): for distinct $s, t$ with $m (s, t) = \infty$ , every alternating word of length $q \geq 1$ beginning with $s$ is ambient reduced; applying the clause to $(t, s)$ gives the same for words beginning with $t$ .

[F9]

The length identity, the prefix property, left translation, and interval translation for weak order (4): for $u \leq_{R} v$ , $x \mapsto u x$ is an order isomorphism $[1, u^{- 1} v]_{R} \to [u, v]_{R}$ .

[F10]

The right and left weak orders, intervals, covers, and meets and joins of subsets (3): a right upper bound $z$ of $A$ satisfies $a \leq_{R} z$ for every $a \in A$ ; a right join is an upper bound below every upper bound. A right meet is a lower bound above every lower bound.

[F11]

The right and left weak orders, intervals, covers, and meets and joins of subsets (1): $u \leq_{L} v$ iff $v = x u$ with $ℓ (v) = ℓ (u) + ℓ (x)$ .

[F12]

Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups: the presentation has relator $u^{2} = 1$ for every $u \in S$ .

[F13]

Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups: the empty word has value $1$ and length $0$ , so $ℓ (1) = 0$ .

[F14]

The right and left weak orders, intervals, covers, and meets and joins of subsets (2): $[u, v]_{R} = {w \in W : u \leq_{R} w and w \leq_{R} v}$ , with the analogous definition for left intervals.

[F15]

Lattices, distributive lattices, and order ideals: a lattice is a poset in which every pair has a least upper bound.

[F16]

The length identity, the prefix property, left translation, and interval translation for weak order (2): $u \leq_{L} v$ iff some reduced expression of $v$ has a reduced expression of $u$ as its terminal segment.

[A1]

For each $q \geq 1$ , the alternating words of length $q$ are exactly the words valued by $a_{q}$ and $b_{q}$ , according as the first letter is $s$ or $t$ ; the only word of length $0$ is the empty word with value $1$ .

Proof

1.1A1F1F2F3F8F12givenalgebra

Every reduced expression is alternating and every element of $W$ has exactly one reduced expression. If a reduced expression had equal adjacent letters, [F2] would delete them and shorten a word for the same element, a contradiction; thus every reduced expression is alternating by [A1]. Conversely every alternating word is reduced by [F8]. If two reduced expressions have the same value, their lengths both equal the length of that element by [F1], so they have the same length $q$ . For $q = 0$ both are the empty word; for $q \geq 1$ , [A1] says each is $a_{q}$ or $b_{q}$ . If their first letters agree then the words are identical. If $q = 2 k$ is even and the first letters differ, equality would give $(s t)^{k} = (t s)^{k} = (s t)^{- k}$ , using $s^{2} = t^{2} = 1$ from [F12], and hence $(s t)^{q} = 1$ , contrary to [F3]. If $q = 2 k + 1$ is odd, equality $(s t)^{k} s = (t s)^{k} t$ gives $(s t)^{k} = (s t)^{- k} t s = (s t)^{- k - 1}$ after right multiplication by $s$ , again forcing $(s t)^{q} = 1$ , contrary to [F3]. Thus reduced expressions are unique; every element has one by the definition of $ℓ$ in [F1].

1.2F1F3F4F7F11F13givenalgebra

The generators are incomparable in both orders. If $s \leq_{R} t$ , then [F4] gives $t = s x$ and $ℓ (t) = ℓ (s) + ℓ (x) = 1 + ℓ (x)$ by [F7]. Since $ℓ (t) = 1$ , $ℓ (x) = 0$ , so $x = 1$ by [F1] and [F13], contradicting $s \neq t$ in [F3]. Interchanging $s, t$ excludes $t \leq_{R} s$ . If $s \leq_{L} t$ , then [F11] gives $t = x s$ and $ℓ (t) = ℓ (x) + ℓ (s) = ℓ (x) + 1$ ; the same length-zero argument gives $x = 1$ and $t = s$ , a contradiction. Interchanging $s, t$ excludes $t \leq_{L} s$ .

2.1A1F3F12step 1.1givenalgebra

The powers $(s t)^{k}$ , $k \in Z$ , are pairwise distinct, and $W$ is infinite. For $k \geq 1$ , $(s t)^{k}$ is the value $a_{2 k}$ ; for $k \leq - 1$ , $(s t)^{k} = (t s)^{- k}$ is the value $b_{- 2 k}$ by [F12]; and $(s t)^{0} = 1$ . If $(s t)^{i} = (s t)^{j}$ for $i \neq j$ , cancellation gives $(s t)^{i - j} = 1$ , contrary to the infinite order in [F3]. Thus the powers are pairwise distinct and form an infinite subset of $W$ .

2.2A1F1F5F8F14step 1.1givenalgebra

For every $v \in W$ , $[1, v]_{R}$ is the finite chain of values of the prefixes of its unique reduced expression; in particular $[1, s t s]_{R} = {1, s, s t, s t s}$ and $[1, t s]_{R} = {1, t, t s}$ . Let $p_{j}$ be the prefix of length $j$ of the unique reduced expression of $v$ . Each prefix is alternating and hence reduced by [F8], so prefixes of different lengths have different values by [F1]. By [F5], $u \leq_{R} v$ holds exactly when the reduced expression of $u$ is a prefix of this unique expression of $v$ ; thus the elements of $[1, v]_{R}$ are exactly the prefix values, ordered by prefix inclusion. They form a finite chain with $ℓ (v) + 1$ elements. The displayed intervals follow because $s t s$ and $t s$ are alternating reduced words.

2.3F5F10F15F16step 1.1givenalgebra

The set ${s, t}$ has no upper bound in either weak order, so its right join $s \lor t$ does not exist and $W$ is not a lattice. If $z$ were a right upper bound, $s \leq_{R} z$ and $t \leq_{R} z$ would give, by [F5], reduced expressions of $z$ beginning with $s$ and with $t$ . This contradicts the uniqueness in step 1.1. If $z$ were a left upper bound, [F16] would give reduced expressions of $z$ ending in $s$ and in $t$ , the same contradiction. Therefore there is no upper bound in either order; by [F10] a right join must be an upper bound, so $s \lor t$ does not exist. Since a lattice has a join for every pair by [F15], $W$ is not a lattice.

3.1F10F14step 2.2givenalgebra

If $\emptyset \neq X \subseteq [1, v]_{R}$ , then $X$ has a meet and a join: they are its least and greatest elements in the finite chain of step 2.2. The least element is a lower bound of $X$ , and every lower bound is below it because it belongs to $X$ ; hence it is $⋀ X$ by [F10]. Dually, the greatest element is an upper bound of $X$ and is below every upper bound, so it is $⋁ X$ . In particular, $s \land s t = s$ and $s \lor s t = s t$ in $[1, s t s]_{R}$ .

3.2F9F12F14step 2.2givenalgebra

The interval translation isomorphism: $s \leq_{R} s t s$ by step 2.2, and $s^{- 1} (s t s) = s (s t s) = t s$ by [F12]. Hence [F9] gives the order isomorphism $x \mapsto s x$ from $[1, t s]_{R}$ to $[s, s t s]_{R}$ . Using the displayed interval of step 2.2, its values are $s, s t, s t s$ , so $[s, s t s]_{R} = {s, s t, s t s}$ .

4.1F4F6F10F13step 2.2step 2.3step 3.1givenalgebra∎

Every nonempty subset of $[1, s t s]_{R}$ has a join, while the empty subset also has join $1$ . Every nonempty such subset is bounded above by $s t s$ , so [F6] supplies its join. For the empty subset, every element is an upper bound by vacuity; [F13] gives $ℓ (1) = 0$ , and [F4] gives $1 \leq_{R} w$ for every $w \in W$ by writing $w = 1 \cdot w$ with $ℓ (w) = ℓ (1) + ℓ (w)$ . Thus $1$ is the least upper bound of the empty set by [F10]. The operations on nonempty subsets were explicitly computed from finite chains in step 3.1, and the empty join was proved directly, so no Axiom of Choice is used. In contrast, step 2.3 shows that ${s, t}$ has no join; hence the boundedness hypothesis for nonempty subsets in Weak order is a meet-semilattice, finite Coxeter groups are lattices, and joins of simple reflections exist exactly for finite parabolics (1) cannot be dropped.

Depends on

Used by

Nothing in the library uses this result yet.

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 (Graduate Texts in Mathematics 231, Springer 2005; author-hosted complete PDF) (standard reference, not scraped)