TheoremStatement: AI-adaptedProof: 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.

The Poincare polynomial as a product of q-integers of the basic degrees, with longest-element reciprocity

Statement

Assume the Axiom of Choice (The Axiom of Choice), used only through the degree determination below. Let $(W, S)$ be a finite Coxeter system with diagram as defined in Coxeter diagrams: edges, labels, components and finite type and $n = ∣ S ∣$ , and let $d_{1} \leq \dots \leq d_{n}$ be its basic degrees and $e_{i} : = d_{i} - 1$ its exponents, as installed in Basic degrees, exponents, and the graded coinvariant algebra of a finite Coxeter system and independently determined, together with their complete type tables, in A regular Coxeter eigenvector determines the basic degrees: the exponent-residue identification and the complete degree tables for all finite Coxeter types (1)-(3). Write $[d]_{t} : = 1 + t + \dots + t^{d - 1}$ and let $P_{W}$ be the length generating series of Length generating series, descent-class series, spherical subsets, and the multivariate descent polynomial. Then:

For $n = 0$ , the Coxeter presentation has $W = {1}$ , the degree and exponent families are empty, and $P_{W} (t) = 1$ ; all empty products are $1$ . This is the rank-zero case of the displayed product.

(1) The Poincare product. $P_{W} (t) = \prod_{i = 1}^{n} [d_{i}]_{t} = \prod_{i = 1}^{n} (1 + t + \dots + t^{e_{i}})$ , a polynomial of degree $\sum_{i} e_{i}$ with $P_{W} (0) = 1$ and $P_{W} (1) = ∣ W ∣ = \prod_{i} d_{i}$ . This includes $H_{3}$ , $H_{4}$ and every $I_{2} (m)$ , and every reducible type: if the diagram is disconnected with components on $S_{1}, \dots, S_{k}$ , then $P_{W} = \prod_{j} P_{W_{S_{j}}}$ and the degree multiset is the concatenation of the components' multisets (Disconnected diagrams, direct products, and comparison of invariant forms (1), Classification of finite Coxeter systems, including the H and dihedral families (2)).

(2) Reciprocity. With $N : = ∣ Φ_{+} ∣ = ℓ (w_{0}) = \sum_{i = 1}^{n} e_{i}$ (The longest element as the opposition of the chamber, and longest elements of finite parabolics (1)(ii),(iii), A regular Coxeter eigenvector determines the basic degrees: the exponent-residue identification and the complete degree tables for all finite Coxeter types (1)), $t^{N} P_{W} (t^{- 1}) = P_{W} (t),$ i.e. the coefficient sequence of $P_{W}$ is palindromic. This is proved directly from the longest-element bijection $w \mapsto w_{0} w$ and does not use (1).

(3) Independence. The degrees $d_{i}$ are not defined by (1) and are not inferred from it: they are supplied by the Molien/Jacobian/regular-eigenvector determination of A regular Coxeter eigenvector determines the basic degrees: the exponent-residue identification and the complete degree tables for all finite Coxeter types, whose tables agree with the products of (1) by Classical Poincare products for A, B, D and I2(m) from the permutation and signed-permutation models (3) and Exceptional parabolic-orbit length certificates for E6, E7, E8, F4, H3 and H4 (3). Neither (1) nor (2) is used to prove the other; in particular the exponent comparison $\sum_{i} e_{i} = N$ is not used to determine the degrees, and the degree product is not used to prove reciprocity.

Facts & Assumptions

Given: A finite Coxeter system $(W, S)$ with $n = ∣ S ∣$ , length function $ℓ$ , its basic degrees $d_{1} \leq \dots \leq d_{n}$ and exponents $e_{i} = d_{i} - 1$ installed under the Axiom of Choice, its longest element $w_{0}$ , and the series $P_{A}$ of Length generating series, descent-class series, spherical subsets, and the multivariate descent polynomial.

[F1]

The finite irreducible Coxeter systems are exactly the types listed in the Statement, and every reducible finite system decomposes into these components (Classification of finite Coxeter systems, including the H and dihedral families (1)-(2), Coxeter diagrams: edges, labels, components and finite type).

[F2]

The basic degrees are the degrees of a minimal homogeneous generating family of the invariant ring, determined independently of the Poincare series, with the complete tables of A regular Coxeter eigenvector determines the basic degrees: the exponent-residue identification and the complete degree tables for all finite Coxeter types (1)-(3): $A_{n} : 2, 3, \dots, n + 1$ ; $B_{n} : 2, 4, \dots, 2 n$ ; $D_{n} : 2, 4, \dots, 2 n - 2$ together with $n$ ; $I_{2} (m) : 2, m$ ; $E_{6} : 2, 5, 6, 8, 9, 12$ ; $E_{7} : 2, 6, 8, 10, 12, 14, 18$ ; $E_{8} : 2, 8, 12, 14, 18, 20, 24, 30$ ; $F_{4} : 2, 6, 8, 12$ ; $H_{3} : 2, 6, 10$ ; $H_{4} : 2, 12, 20, 30$ ; for reducible systems the degree multiset is the concatenation of the components' multisets, and $\prod_{i} d_{i} = ∣ W ∣$ (Basic degrees, exponents, and the graded coinvariant algebra of a finite Coxeter system, The Axiom of Choice).

[F3]

Classical products and exceptional products: $P_{A_{n}} = [n + 1]_{t}!$ , $P_{B_{n}} = \prod_{i = 1}^{n} [2 i]_{t}$ , $P_{D_{n}} = [n]_{t} \prod_{i = 1}^{n - 1} [2 i]_{t}$ , $P_{I_{2} (m)} = [2]_{t} [m]_{t}$ (Classical Poincare products for A, B, D and I2(m) from the permutation and signed-permutation models (3)), and $P_{W} = \prod_{d \in D (W)} [d]_{t}$ for $W$ of type $E_{6}, E_{7}, E_{8}, F_{4}, H_{3}, H_{4}$ (Exceptional parabolic-orbit length certificates for E6, E7, E8, F4, H3 and H4 (3)).

[F4]

If the diagram is disconnected with nonempty components on $S_{1}, \dots, S_{k}$ , then $W ≅ W_{S_{1}} \times \dots \times W_{S_{k}}$ and $ℓ (w_{1} \dots w_{k}) = \sum_{i} ℓ (w_{i})$ , so $P_{W} = \prod_{j} P_{W_{S_{j}}}$ (Disconnected diagrams, direct products, and comparison of invariant forms (1)).

[F5]

If $W$ is finite, there is a unique $w_{0} \in W$ with $N : = ℓ (w_{0}) = ∣ Φ_{+} ∣$ maximal, $w_{0}^{2} = 1$ , and $ℓ (w_{0} w) = ℓ (w_{0}) - ℓ (w)$ for all $w \in W$ (The longest element as the opposition of the chamber, and longest elements of finite parabolics (1)(ii),(iii),(iv)).

[F6]

The series is $P_{A} (t) = \sum_{w \in A} t^{ℓ (w)}$ with finite length fibers; for finite $W$ it is a polynomial, has constant coefficient $1$ , and $P_{W} (1) = ∣ W ∣$ . If $S = \emptyset$ , then $W = {1}$ and $P_{W} = 1$ . For a polynomial of degree $N$ , $t^{N} P_{W} (t^{- 1}) = P_{W} (t)$ is equivalent by coefficient comparison to palindromicity (Length generating series, descent-class series, spherical subsets, and the multivariate descent polynomial (1),(4), The cardinality $∣ A ∣$ of a finite set).

Proof

technique · direct

1.1F1F2F3algebra

Irreducible types. If $(W, S)$ is irreducible, then by [F1] it is of one of the listed types. For $W = A_{n}$ the table of [F2] gives $\prod_{i} [d_{i}]_{t} = \prod_{k = 2}^{n + 1} [k]_{t} = [n + 1]_{t}! = P_{A_{n}}$ by [F3]; for $B_{n}$ it gives $\prod_{i = 1}^{n} [2 i]_{t} = P_{B_{n}}$ ; for $D_{n}$ the multiset ${2, 4, \dots, 2 n - 2} \cup {n}$ gives $[n]_{t} \prod_{i = 1}^{n - 1} [2 i]_{t} = P_{D_{n}}$ ; and for $I_{2} (m)$ it gives $[2]_{t} [m]_{t} = P_{I_{2} (m)}$ . For the six exceptional types the same comparison is the content of [F3]. Hence $P_{W} = \prod_{i = 1}^{n} [d_{i}]_{t}$ for every irreducible finite type.

1.2F5F6algebra

Reciprocity. The map $w \mapsto w_{0} w$ is a bijection of $W$ with itself, and $ℓ (w_{0} w) = ℓ (w_{0}) - ℓ (w)$ for all $w$ by [F5]. Summing $t^{ℓ (w)}$ over $W$ and substituting $w_{0} w$ for $w$ gives $P_{W} (t) = \sum_{w \in W} t^{ℓ (w_{0} w)} = \sum_{w \in W} t^{N - ℓ (w)} = t^{N} P_{W} (t^{- 1})$ as an identity of polynomials, since $ℓ (w) \leq N$ for all $w$ ; equivalently $[t^{k}] P_{W} = [t^{N - k}] P_{W}$ for every $k$ , so the coefficient sequence is palindromic.

2.1step 1.1F2F4F6algebra

Reducible types and the numerical consequences. If $n = 0$ , then $W = {1}$ and the degree and exponent lists are empty; [F6] gives $P_{W} = 1$ , so the product, constant-term and evaluation claims hold with empty products equal to $1$ . For $n > 0$ , step 1.1 gives the product when the diagram is connected. If it is disconnected, let its nonempty components be $S_{1}, \dots, S_{k}$ . By [F4], $P_{W} = \prod_{j} P_{W_{S_{j}}}$ , and each component product equals $\prod_{d \in D (W_{S_{j}})} [d]_{t}$ by step 1.1. By [F2], the degree multiset of $W$ is the concatenation of the component multisets, so $P_{W} = \prod_{i = 1}^{n} [d_{i}]_{t}$ . In either positive-rank case, each $[d_{i}]_{t}$ has constant term $1$ and $d_{i}$ terms; therefore the product has degree $\sum_{i} (d_{i} - 1) = \sum_{i} e_{i}$ , constant term $1$ , and value $\prod_{i} d_{i} = ∣ W ∣$ at $t = 1$ by [F2].

3.1step 1.1step 1.2step 2.1F2F3algebra∎

Independence. The degrees $d_{i}$ are the degrees of a minimal homogeneous generating family of the invariant ring; the determination of [F2] uses the Molien identity, the invariant Jacobian and the regular Coxeter eigenvector, and never the series $P_{W}$ ; the tables it produces are compared with the products of [F3]. Hence (1) is proved from the independently given degrees and does not define them, and (2) is proved in step 1.2 without using (1). Finally, the exponent identity $\sum_{i} e_{i} = N$ follows by comparing degrees: step 2.1 shows that $\deg P_{W} = \sum_{i} e_{i}$ with leading coefficient $1$ , while step 1.2 shows that $t^{N} P_{W} (t^{- 1}) = P_{W} (t)$ with $[t^{N}] P_{W} = [t^{0}] P_{W} = 1$ , so $\deg P_{W} = N$ and $\sum_{i} e_{i} = N$ ; this comparison is a consequence of (1) and (2), not an input to either. No choice beyond the AC premise of the degree determination of [F2] is used.

Depends on

Used by

Dependency tree · two levels

117 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)