ExampleConstruction: AI-adaptedVerification: 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 growth, the infinite Steinberg identity, and the failure of polynomial reciprocity

Example

Let $W = ⟨ s, t ∣ s^{2} = t^{2} = 1 ⟩$ be the infinite dihedral Coxeter group, so $S = {s, t}$ and $m (s, t) = \infty$ (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups, The rank-two block computation, exact dihedral orders, the signed reflection action, and ambient reducedness (3)(c),(4)). Then:

(1) Growth series. Every word reduces by canceling adjacent equal generators to an alternating word. For each $q \geq 1$ , the two alternating words $(s t)^{q}$ and $(t s)^{q}$ have length $2 q$ ; for each $q \geq 0$ , $(s t)^{q} s$ and $(t s)^{q} t$ have length $2 q + 1$ . These words are reduced by The rank-two block computation, exact dihedral orders, the signed reflection action, and ambient reducedness (7), with the generators interchanged for the words beginning with $t$ ; their pairwise distinctness is proved in step 1.1 below using the infinite order of $s t$ from (4). They exhaust the nonidentity elements, so $W$ has one element of length $0$ and exactly two of each length $n \geq 1$ : $P_{W} (t) = 1 + 2 t + 2 t^{2} + 2 t^{3} + \dots = 1 + \frac{2 t}{1 - t} = \frac{1 + t}{1 - t} \in Q (t)$ The coefficientwise identity $(1 - t) P_{W} = 1 + t$ follows from the displayed coefficients by the Cauchy product (Formal power series over a commutative ring and the coefficient-extraction functional $[x^{n}]$ ), and $1 - t$ has unit constant term (A formal power series is a unit exactly when its constant coefficient is a unit, Rational formal power series, proper presentations and reduced denominators).

(2) The infinite Steinberg identity. The spherical subsets are $\emptyset, {s}, {t}$ , with $P_{W_{\emptyset}} = 1$ , $P_{W_{{s}}} = P_{W_{{t}}} = 1 + t$ , and $P_{W} = (1 + t) / (1 - t)$ ; the infinite case of Finite descent parabolics, parabolic factorization, the Steinberg inclusion-exclusion identity, and rational growth (4) reads $1 - \frac{2}{1 + t} + \frac{1 - t}{1 + t} = 0,$ i.e. $1 / P_{W} (t) = \frac{1 - t}{1 + t}$ , as the formal inverse of $(1 + t) / (1 - t)$ requires (A formal power series is a unit exactly when its constant coefficient is a unit).

(3) Failure of polynomial reciprocity. The reduced words in (1) have unbounded lengths, so $W$ has no longest element; the infinite-case result of Finite descent parabolics, parabolic factorization, the Steinberg inclusion-exclusion identity, and rational growth (1) also gives that no element has all descents. For comparison, the finite-case pattern $t^{N} P_{W} (t^{- 1}) = P_{W} (t)$ is the reciprocity of The Poincare polynomial as a product of q-integers of the basic degrees, with longest-element reciprocity (2). Here the rational function satisfies $P_{W} (t^{- 1}) = \frac{1 + t^{- 1}}{1 - t^{- 1}} = - \frac{1 + t}{1 - t} = - P_{W} (t) .$ Thus, for every $N \geq 0$ , $t^{N} P_{W} (t^{- 1}) = - t^{N} P_{W} (t)$ ; equality with $P_{W} (t)$ would force $t^{N} = - 1$ in $Q (t)$ , which is impossible. The substitution is interpreted in the rational-function field, not as an element of $Z ⟦ t ⟧$ . More generally, an infinite Coxeter group with finite $S$ has unbounded length (there are only finitely many words of bounded length), so its growth series is not a polynomial and the finite reciprocity theorem does not apply as a polynomial statement. This alone makes no assertion about rational-function reciprocity for other infinite Coxeter systems.

(4) Rank-one comparison. The parabolic $W_{{s}} = {1, s}$ has $P_{W_{{s}}} (t) = 1 + t = [2]_{t}$ . The infinite growth series is not a finite product $[m]_{t} [2]_{t}$ for any finite $m$ , since every such product is a polynomial while $P_{W}$ has infinitely many nonzero coefficients. With the conventions of the companion page, this same group is denoted $I_{2} (\infty)$ .

Facts & Assumptions

Given: The presented group $W = ⟨ s, t ∣ s^{2} = t^{2} = 1 ⟩$ , the Coxeter matrix with $m (s, t) = \infty$ on $S = {s, t}$ , its length function $ℓ$ , and the series $P_{A} (t) = \sum_{w \in A} t^{ℓ (w)}$ of Length generating series, descent-class series, spherical subsets, and the multivariate descent polynomial.

[L1]

For $m (s, t) = \infty$ the rank-two product $s t$ has infinite order in $W$ and the elements $s, t \in W$ are distinct involutions (The rank-two block computation, exact dihedral orders, the signed reflection action, and ambient reducedness (3)(c),(4)).

[L2]

Every alternating word beginning with either $s$ or $t$ of length $q \geq 1$ is reduced in the ambient group (apply the source also with $s, t$ interchanged) (The rank-two block computation, exact dihedral orders, the signed reflection action, and ambient reducedness (7)).

[L3]

The defining relators $s^{2} = t^{2} = 1$ allow adjacent equal letters to be canceled without changing the represented element; $ℓ (w)$ is the minimum length of a generator word representing $w$ (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups).

[L4]

For every $A \subseteq W$ the series $P_{A} = \sum_{w \in A} t^{ℓ (w)}$ is well-defined (Length generating series, descent-class series, spherical subsets, and the multivariate descent polynomial (1)); a series is rational if $Q F = P$ for polynomials with $Q (0)$ a unit (Rational formal power series, proper presentations and reduced denominators).

[L5]

For $J \subseteq S$ , $W^{J} = {w : ℓ (w s) > ℓ (w) for all s \in J}$ and $P_{W} = P_{W^{J}} P_{W_{J}}$ (Finite descent parabolics, parabolic factorization, the Steinberg inclusion-exclusion identity, and rational growth (2)).

[L6]

For infinite $W$ , $\sum_{K \subseteq S} (- 1)^{∣ K ∣} / P_{W_{K}} (t) = 0$ (Finite descent parabolics, parabolic factorization, the Steinberg inclusion-exclusion identity, and rational growth (4)).

[L7]

For infinite $W$ , no element has all descents (Finite descent parabolics, parabolic factorization, the Steinberg inclusion-exclusion identity, and rational growth (1)).

[L8]

The finite-case pattern is $t^{N} P_{W} (t^{- 1}) = P_{W} (t)$ with $N = ℓ (w_{0})$ (The Poincare polynomial as a product of q-integers of the basic degrees, with longest-element reciprocity (2)); its longest-element reciprocity argument is choice-free and its basic-degree branch is not used here.

[L9]

The Cauchy product is defined coefficientwise by finite sums, and a series with unit constant term has a unique formal inverse; here $1 + t$ and $(1 + t) / (1 - t)$ have constant term $1$ (Formal power series over a commutative ring and the coefficient-extraction functional $[x^{n}]$ , A formal power series is a unit exactly when its constant coefficient is a unit).

Verification

technique · direct

1.1L1L2L3L4L9algebra

Every word in $s, t$ can be shortened by canceling an adjacent pair $s s$ or $t t$ by [L3], so a shortest word is alternating. For each $q \geq 1$ the two alternating words of length $2 q$ are $(s t)^{q}, (t s)^{q}$ , and for each $q \geq 0$ the two of length $2 q + 1$ are $(s t)^{q} s, (t s)^{q} t$ . They are reduced by [L2], so unequal lengths give unequal elements. Put $r = s t$ , so $t s = r^{- 1}$ and $t = r^{- 1} s$ . At the same even length $2 q > 0$ , equality of the two words would give $r^{q} = r^{- q}$ and hence $r^{2 q} = 1$ ; at the same odd length $2 q + 1$ , equality would give $r^{q} s = r^{- q} t = r^{- q - 1} s$ and hence $r^{2 q + 1} = 1$ . Both contradict the infinite order in [L1]. Equivalently, the presentation admits the parity homomorphism sending both generators to $- 1$ , because each defining relator has even length, so even and odd words cannot coincide. Every element has one of these forms or is the identity. Thus $[t^{0}] P_{W} = 1$ and $[t^{n}] P_{W} = 2$ for every $n \geq 1$ . By the Cauchy-product definition, $(1 - t) P_{W} = 1 + t$ : its coefficients are $1$ at degree $0$ , $2 - 1 = 1$ at degree $1$ , and $2 - 2 = 0$ at every degree $n \geq 2$ . Since $1 - t$ has unit constant term, $P_{W} = (1 + t) / (1 - t)$ in $Z ⟦ t ⟧$ , and [L4] makes this a rational series.

2.1step 1.1L1L6algebra

A subset $I \subseteq S$ is spherical exactly when $W_{I}$ is finite. The three proper parabolics $W_{\emptyset} = {1}$ , $W_{{s}} = {1, s}$ and $W_{{t}} = {1, t}$ are finite; $W_{S} = W$ is infinite by [L1]. Thus the spherical subsets are exactly $\emptyset, {s}, {t}$ , with $P_{W_{\emptyset}} = 1$ and $P_{W_{{s}}} = P_{W_{{t}}} = 1 + t$ , while all four subsets occur in the Steinberg sum of [L6]. Substituting $P_{W} = (1 + t) / (1 - t)$ from step 1.1 gives $1 - 2 / (1 + t) + 1 / P_{W} = 1 - 2 / (1 + t) + (1 - t) / (1 + t) = 0$ , the infinite case of [L6].

2.2step 1.1L1L7L8algebra

In $Q (t)$ , $P_{W} (t^{- 1}) = (1 + t^{- 1}) / (1 - t^{- 1}) = - P_{W} (t)$ . If $t^{N} P_{W} (t^{- 1}) = P_{W} (t)$ for some $N \geq 0$ , then $- t^{N} P_{W} (t) = P_{W} (t)$ ; since $P_{W} \neq 0$ , this forces $t^{N} = - 1$ , impossible in $Q (t)$ . Thus no such $N$ exists. The alternating words in step 1.1 have unbounded lengths, so $W$ has no longest element; the infinite-case statement of [L7] also says no element has all descents.

3.1step 1.1step 2.1L4L9algebra

The series $P_{W} = (1 + t) / (1 - t)$ and $(1 - t) / (1 + t)$ are inverse to each other in $Q ⟦ t ⟧$ : their product is $1$ , and both have constant term $1$ , so by [L9] $(1 - t) / (1 + t) = 1 / P_{W} (t)$ as a formal inverse. This is the identity verified in step 2.1 and shows that $1 / P_{W}$ is rational while $P_{W}$ has infinitely many positive coefficients.

4.1step 1.1step 2.1L4L5algebra∎

The rank-one parabolic $W_{{s}} = {1, s}$ has $P_{W_{{s}}} (t) = 1 + t = [2]_{t}$ . The reduced forms in step 1.1 with no right $t$ -descent are the identity and the alternating words ending in $s$ , exactly one of each length; hence $P_{W^{{t}}} = 1 + t + t^{2} + \dots$ . By [L5], $P_{W} = P_{W^{{t}}} P_{W_{{t}}} = (1 + t) (1 + t + t^{2} + \dots)$ , which is not a polynomial. No finite $m$ has $[2]_{t} [m]_{t} = (1 + t) / (1 - t)$ , since the left side is a polynomial and the right has infinitely many nonzero coefficients. The same group is denoted $I_{2} (\infty)$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

73 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

A. Björner and F. Brenti, Combinatorics of Coxeter Groups, GTM 231 (class-hosted complete PDF) (standard reference, not scraped)
M. W. Davis, The Geometry and Topology of Coxeter Groups (author manuscript of the book) (standard reference, not scraped)