Pipeline-generated

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.

✓ 5 results · all verified · 3 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 2 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Coxeter Descents, Poincaré Polynomials, and Growth

1 · Prerequisites

2 · Summary

Length enumeration measures chamber distance. Coset factorizations give product formulas for the growth series, a descent inclusion-exclusion gives rational growth for every finite-rank Coxeter system, and a coefficientwise comparison with independently determined invariant degrees gives the Poincaré product for every finite type.

This page develops the growth calculus of a Coxeter system with finite generating set: the length generating series and the descent-class series as formal power series, the finite descent parabolics and the parabolic factorizations, the two-case Steinberg inclusion-exclusion identity with rational growth, the explicit classical and dihedral quotients, the six exact exceptional parabolic-orbit certificates, and the exponent product with longest-element reciprocity. Everything is proved from the local suppliers of the earlier pages; the only Choice assumption is the one carried by the invariant-degree determination.

Definition and conventions

Length generating series, descent-class series, spherical subsets, and the multivariate descent polynomial fixes the formal series $P_{A} (t) = \sum_{w \in A} t^{ℓ (w)}$ for $A \subseteq W$ : for finite $S$ every length fiber is finite, so all coefficients are cardinalities of finite sets and no convergence is asserted; when $1 \in A$ the series has constant term $1$ and a recursively determined formal inverse. It defines spherical subsets $I$ by finiteness of $W_{I}$ , the descent-class series $D_{I}^{J} (t) = \sum_{{w : I \subseteq D_{R} (w) \subseteq J}} t^{ℓ (w)}$ with the interval convention, and the multivariate descent polynomial for finite $W$ only. It explicitly asserts nothing about rationality, about the length-additive interpretation of the quotient sets, or about the finiteness of descent parabolics; those are the content of the theorem below, the definition's well-definedness is proved locally by its finite-fiber argument.

Main results

The orbit of a dual fundamental functional: stabilizer, minimal coset length, Schreier distance, and the quotient formula is the geometric engine behind every explicit quotient computation on this page. For the dual fundamental functional $f_{0}$ of $s_{0} \in S$ with $T = S ∖ {s_{0}}$ it proves ${Stab}_{W} (f_{0}) = W_{T}$ , the equivariant bijection $W / W_{T} \to W \cdot f_{0}$ , the identity of the orbit distance $d (v) = \min {ℓ (x) : x \cdot f_{0} = v}$ with the minimal left-coset length, the fact that $d$ is the graph distance in the Schreier graph generated by $S$ (hence $∣ d (s \cdot v) - d (v) ∣ \leq 1$ and every attaining word gives an upper bound), and the quotient formula $P_{W} = P_{W_{T}} \sum_{v} t^{d (v)}$ . No finiteness of $W_{T}$ is assumed, and the lemma uses no Choice.

Finite descent parabolics, parabolic factorization, the Steinberg inclusion-exclusion identity, and rational growth proves that $W_{D_{L} (w)}$ and $W_{D_{R} (w)}$ are finite for every $w$ , with $D_{L} (w_{0} (I)) = D_{R} (w_{0} (I)) = I$ for finite $W_{I}$ and the resulting finite/infinite dichotomy for $D_{S}^{S}$ ; both parabolic factorizations $P_{W} = P_{W^{J}} P_{W_{J}} = P_{^{J} W} P_{W_{J}}$ , with the product formula for disconnected diagrams; the descent inclusion-exclusion $D_{I}^{J} (t) = \sum_{J ∖ I \subseteq K \subseteq J} (- 1)^{∣ J ∖ K ∣} P_{W^{S ∖ K}} (t)$ ; the two-case Steinberg identity $\sum_{K \subseteq S} (- 1)^{∣ K ∣} / P_{W_{K}} (t) = t^{ℓ (w_{0})} / P_{W} (t)$ for finite $W$ and $0$ for infinite $W$ ; and rationality of $P_{W}$ for every finite-rank Coxeter system, by induction on $∣ S ∣$ , with the displayed recursions. No Choice is used.

Classical Poincare products for A, B, D and I2(m) from the permutation and signed-permutation models identifies the canonical reflection representation of each classical diagram $A_{n}$ , $B_{n}$ , $D_{n}$ , $I_{2} (m)$ with its permutation or signed-permutation model through a linear isometry. For the specified terminal nodes it computes the dual-functional orbits and their Schreier distances: $0, \dots, n$ for $A_{n}$ , $0, \dots, 2 n - 1$ for $B_{n}$ , with two vertices at distance $n - 1$ in type $D_{n}$ , and the alternating $m$ -vertex path for $I_{2} (m)$ . Explicit words attain these distances, and the resulting recurrences give $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}$ and $P_{I_{2} (m)} = [2]_{t} [m]_{t}$ , with orders $(n + 1)!$ , $2^{n} n!$ and $2^{n - 1} n!$ . It treats $D_{2}$ directly and uses $D_{3} = A_{3}$ for the recurrence base; the low-rank coincidences are checked, and no invariant degrees enter this item.

Exceptional parabolic-orbit length certificates for E6, E7, E8, F4, H3 and H4 treats $E_{6}, E_{7}, E_{8}, F_{4}, H_{3}, H_{4}$ using the exact certificate file research/coxeter-scaffold/math-checks/finite-degree-poincare-certificates.json. The labelled diagrams and dual action determine the simple-reflection matrices exactly; the file stores each orbit point's coordinates, every generator image, an attaining word and distance, and the bipartite Coxeter-element matrix and characteristic polynomial. The certificate checks orbit closure, inverse edges, word attainment, the distance step bound, the cyclotomic spectrum, and the coefficientwise Poincare product identity over $Q$ , $Q (\sqrt{2})$ and $Q (φ)$ . The six quotient polynomials and their factorizations combine with the classical $D_{5}, B_{3}, I_{2} (5)$ products and the independently determined degree tables to give the exceptional Poincare products. The edge scalars for labels $3, 4, 5$ are derived from trigonometric identities, and the Axiom of Choice enters only through the basic-degree determination. Björner--Brenti, Example 7.1.6, gives an independent $F_{4}$ quotient-polynomial comparison.

The Poincare polynomial as a product of q-integers of the basic degrees, with longest-element reciprocity assembles the classical and exceptional comparisons into $P_{W} (t) = \prod_{i = 1}^{n} [d_{i}]_{t} = \prod_{i = 1}^{n} (1 + t + \dots + t^{e_{i}})$ for every finite Coxeter system, with the reducible case handled by the concatenation of degree multisets; proves the reciprocity $t^{N} P_{W} (t^{- 1}) = P_{W} (t)$ with $N = ℓ (w_{0}) = \sum_{i} e_{i}$ directly from the longest-element bijection $w \mapsto w_{0} w$ ; and records that the degrees are installed independently of the Poincaré series; the product formula and reciprocity are proved independently, and comparing their polynomial degrees then gives the exponent-sum identity. Its AC premise is exactly that of the degree determination.

Prerequisites and reading

Required earlier pages: finite-reflection-arrangements-and-spherical-coxeter-complexes for the longest element $w_{0}$ and its length-complement property, parabolic-subgroups-and-double-coset-geometry for the descent conventions, the quotients $W^{J},^{J} W$ and the length-additive coset factorizations, and finite-coxeter-invariants-and-coinvariant-gradings for the basic degrees and the degree tables together with their Axiom of Choice premise. The earlier weak-order-inversions-and-lattice-operations supplies the full-descent criterion for finite type, permutation-statistics-inversions-and-eulerian-numbers supplies the factorial cardinality of symmetric groups, and braided-and-symmetric-monoidal-categories supplies their Coxeter presentation. The companion coxeter-descents-poincare-polynomials-and-growth-examples tests the insertion recurrences, the $A_{2} = S_{3}$ identities and the infinite dihedral growth. Exact item dependencies and source reading limits are recorded in research/coxeter-scaffold/inventory.json and research/plan-coxeter-groups-track.md.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

Length generating series, descent-class series, spherical subsets, and the multivariate descent polynomial

Definition

Let $(W, S)$ be a Coxeter system with $S$ finite, presented group $W$ , length function $ℓ$ and standard parabolic subgroups $W_{I} = ⟨ s : s \in I ⟩$ (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups), and let $D_{L} (w) = {s \in S : ℓ (s w) < ℓ (w)}$ and $D_{R} (w) = {s \in S : ℓ (w s) < ℓ (w)}$ be the descent sets with the conventions fixed in Standard parabolic subgroups, descent-free one- and two-sided representatives, parabolic and reflection subgroups (2).

(1) Length generating series. Let $A \subseteq W$ . The length generating series (also Poincare series) of $A$ is $P_{A} (t) : = \sum_{w \in A} t^{ℓ (w)} \in Z ⟦ t ⟧$ (Formal power series over a commutative ring and the coefficient-extraction functional $[x^{n}]$ ). It is well defined: for every $n \in N$ the fiber ${w \in W : ℓ (w) = n}$ is finite. Evaluation of the $n$ -letter words gives a map $S^{n} \to W$ , and each element of the fiber is the value of one of its reduced words; $S^{n}$ is finite by The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ . Hence $[t^{n}] P_{A} = ∣ {w \in A : ℓ (w) = n} ∣$ is the cardinality (The cardinality $∣ A ∣$ of a finite set) of a finite set, viewed as an integer. This includes $S = \emptyset$ : the length-zero fiber is ${1}$ and every positive-length fiber is empty. If $1 \in A$ then $P_{A} (0) = 1$ and $P_{A} (t)$ is a unit of $Z ⟦ t ⟧$ with a recursively determined formal inverse (A formal power series is a unit exactly when its constant coefficient is a unit); if $1 \notin A$ then $P_{A} (0) = 0$ and $P_{A} (t)$ is not a unit. Thus $P_{A} (t)$ is a unit exactly when $1 \in A$ . No convergence, radius of convergence or evaluation at a real number is asserted.

(2) Spherical subsets and descent-class series. A subset $I \subseteq S$ is spherical when the standard parabolic $W_{I}$ is finite. For $I \subseteq J \subseteq S$ the descent-class series is $D_{I}^{J} (t) : = \sum_{\begin{array}{c} w \in W \\ I \subseteq D_{R} (w) \subseteq J \end{array}} t^{ℓ (w)} \in Z ⟦ t ⟧ .$

This series is well defined coefficientwise because its length- $n$ summation set is a subset of the finite length- $n$ fiber in (1).

(3) Multivariate descent polynomial (finite $W$ only). For finite $W$ define the marked multivariate descent polynomial $\hat{W} (x, y, t) : = \sum_{w \in W} t^{ℓ (w)} \prod_{s \in D_{R} (w)} x_{s} \prod_{s \in S ∖ D_{R} (w)} y_{s} \in Z [x_{s}, y_{s} : s \in S] [t]$ (Polynomial rings in finitely many commuting indeterminates by iteration). This is a polynomial because the sum is finite. Setting every $y_{s} = 1$ recovers the usual descent polynomial $\sum_{w \in W} t^{ℓ (w)} \prod_{s \in D_{R} (w)} x_{s}$ . For $I \subseteq J \subseteq S$ , substitute $x_{s} = 1, y_{s} = 0$ for $s \in I$ , $x_{s} = y_{s} = 1$ for $s \in J ∖ I$ , and $x_{s} = 0, y_{s} = 1$ for $s \notin J$ . A term survives exactly when $I \subseteq D_{R} (w) \subseteq J$ , and then its descent/non-descent factors all equal $1$ ; hence this evaluation is $D_{I}^{J} (t)$ , also a polynomial. This includes $I = \emptyset, J = S$ (the full series $P_{W}$ ) and $I = J$ (the exact descent set $I$ ).

(4) Conventions and limits. $P_{\emptyset} = 0$ and $P_{{1}} = 1$ . For infinite $S$ no scalar Poincare series is defined here; finite $S$ is the standing hypothesis that ensures the finite-coefficient argument in (1). This definition makes no assertion that $P_{A}$ is rational, that $W^{J}$ has a length-additive interpretation, that $D_{I}^{J} (t)$ has the inclusion-exclusion expansion, or that $W_{D_{R} (w)}$ is finite; those are separate results, not part of the definitions above. No choice principle is used.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-10-08Open item page →

The orbit of a dual fundamental functional: stabilizer, minimal coset length, Schreier distance, and the quotient formula

Statement

Let $(W, S)$ be a Coxeter system with $S$ finite, $V = R^{S}$ with Coxeter form $B$ and canonical reflection homomorphism $ρ : W \to G L (V)$ (The real Coxeter form, its radical, reflections, and form-preserving maps, The canonical reflection homomorphism, roots, reflections, and the positive cone, Descent of the reflection representation, unit root norms, and conjugation of reflections (1), Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups), with the dual (contragredient) left action on $V^{*}$ (The dual action, chambers, faces, and root hyperplanes, The dual action, the faces, and the rank-two chamber tiling (1)), the closed chamber $C = {f \in V^{*} : f (e_{s}) \geq 0 for all s \in S}$ and the Tits cone $U = ⋃_{w \in W} w C$ (The dual action, chambers, faces, and root hyperplanes, The Tits cone, its interior, and the negative-root set of a functional). Fix $s_{0} \in S$ , put $T : = S ∖ {s_{0}}$ , and let $f_{0} \in V^{*}$ be the dual fundamental functional $f_{0} (e_{s}) = δ_{s, s_{0}}$ (The dual family $(b^{*})_{b \in B}$ associated to a Hamel basis $B$ , defined by $b^{*} (c) = δ_{b c}$ , The dual family of a finite basis is a basis of the dual space, with the same dimension); then $f_{0} \in C \subseteq U$ . Then:

(1) Stabilizer and orbit. With $S (f) : = {s \in S : f (e_{s}) = 0}$ one has $S (f_{0}) = T$ and ${Stab}_{W} (f_{0}) = W_{T}$ (Chamber collisions, point stabilizers, and the intersection rule (4)). Hence the orbit map $Φ : W / W_{T} ⟶ W \cdot f_{0}, Φ (w W_{T}) = w \cdot f_{0},$ is a well-defined $W$ -equivariant bijection (Left group actions, transitive actions, and faithful actions, Left and right cosets $g H$ and $H g$ of a subgroup, The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups). If $W / W_{T}$ is finite, this bijection gives $∣ W \cdot f_{0} ∣ = [W : W_{T}]$ (The coset set $G / H$ and the index $[G : H]$ of a subgroup); no finite-cardinality notation is used for an infinite orbit.

(2) Distance equals minimal coset length. For $v \in W \cdot f_{0}$ put $d (v) : = \min {ℓ (x) : x \in W, x \cdot f_{0} = v},$ the minimum being attained because ${ℓ (x) : x \cdot f_{0} = v}$ is a nonempty subset of $N$ (The well-ordering principle). For every $w$ with $w \cdot f_{0} = v$ one has ${x \in W : x \cdot f_{0} = v} = w W_{T}$ , and $d (v) = ℓ (d_{w})$ , where $d_{w}$ is the unique minimal-length element of the left coset $w W_{T}$ , characterized by $ℓ (d_{w} s) > ℓ (d_{w})$ for all $s \in T$ and satisfying $ℓ (d_{w} u) = ℓ (d_{w}) + ℓ (u)$ for all $u \in W_{T}$ (Left and right cosets $g H$ and $H g$ of a subgroup, Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (3) with Standard parabolic subgroups, descent-free one- and two-sided representatives, parabolic and reflection subgroups (2)).

(3) Schreier graph and unit step bound. Let $Γ$ be the graph with vertex set $W \cdot f_{0}$ and an undirected edge between $v$ and $s \cdot v$ for every $s \in S$ and every $v$ (self-loops omitted). Then $d (v)$ is the graph distance in $Γ$ from $f_{0}$ to $v$ ; in particular $d (f_{0}) = 0$ and $∣ d (s \cdot v) - d (v) ∣ \leq 1 for all s \in S, v \in W \cdot f_{0} .$

(4) Parabolic quotient formula. $P_{W} (t) = P_{W_{T}} (t) \cdot \sum_{v \in W \cdot f_{0}} t^{d (v)}$ in $Z ⟦ t ⟧$ (Length generating series, descent-class series, spherical subsets, and the multivariate descent polynomial).

(5) Conventions. The statement requires $s_{0} \in S$ , so $T = S$ does not occur here; the parabolic $W_{T}$ need not be finite. Nothing is asserted about primitive vectors, minuscule weights or the general classification of orbits. No choice principle is used.

Facts & Assumptions

Given: A Coxeter system $(W, S)$ with $S$ finite and length function $ℓ$ ; the reflection representation $ρ$ on $V = R^{S}$ with Coxeter form $B$ ; the dual action on $V^{*}$ , the closed chamber $C$ , its open part and the Tits cone $U$ ; a fixed $s_{0} \in S$ , $T = S ∖ {s_{0}}$ , and the dual fundamental functional $f_{0} = e_{s_{0}}^{*}$ with $f_{0} (e_{s}) = δ_{s, s_{0}}$ .

[F1]

The canonical map $ρ : W \to G L (V)$ is a group homomorphism with $ρ (s) = r_{s}$ (Descent of the reflection representation, unit root norms, and conjugation of reflections (1)); consequently the formula $(w \cdot f) (v) = f (ρ (w)^{- 1} v)$ defines a left action by linear maps (The dual action, chambers, faces, and root hyperplanes, The dual action, the faces, and the rank-two chamber tiling (1), Left group actions, transitive actions, and faithful actions). The closed chamber is $C = {f \in V^{*} : f (e_{s}) \geq 0 for all s}$ and the Tits cone is $U = ⋃_{w \in W} w C$ (The dual action, chambers, faces, and root hyperplanes, The Tits cone, its interior, and the negative-root set of a functional).

[F2]

$W_{T} = ⟨ s : s \in T ⟩$ is the standard parabolic, $D_{R} (w) = {s \in S : ℓ (w s) < ℓ (w)}$ , and the set $w W_{T}$ , a left coset by Left and right cosets $g H$ and $H g$ of a subgroup, has a unique element $d$ of minimal length, characterized by $ℓ (d s) > ℓ (d)$ for all $s \in T$ and satisfying $ℓ (d u) = ℓ (d) + ℓ (u)$ for all $u \in W_{T}$ (Standard parabolic subgroups, descent-free one- and two-sided representatives, parabolic and reflection subgroups, Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (3), The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups).

[F3]

For every $f \in C$ the point stabilizer is ${Stab}_{W} (f) = W_{S (f)}$ , where $S (f) = {s \in S : f (e_{s}) = 0}$ (Chamber collisions, point stabilizers, and the intersection rule (4)).

[F4]

For all $w \in W$ and $s \in S$ one has $ℓ (s w) = ℓ (w) \pm 1$ and $ℓ (w s) = ℓ (w) \pm 1$ (Length parity, exchange, two-letter deletion, and faithfulness of the signed reflection action (1)).

[F5]

Every nonempty subset of $N$ has a least element (The well-ordering principle).

[F6]

$f_{0}$ is the coordinate functional $e_{s_{0}}^{*}$ of the basis element $e_{s_{0}}$ , so $f_{0} (e_{s}) = δ_{s, s_{0}}$ ; and for every $A \subseteq W$ the series $P_{A} = \sum_{w \in A} t^{ℓ (w)}$ is a well-defined element of $Z ⟦ t ⟧$ with finite length fibers (The dual family $(b^{*})_{b \in B}$ associated to a Hamel basis $B$ , defined by $b^{*} (c) = δ_{b c}$ , The dual family of a finite basis is a basis of the dual space, with the same dimension, Length generating series, descent-class series, spherical subsets, and the multivariate descent polynomial (1)).

[F7]

$[W : W_{T}] = ∣ W / W_{T} ∣$ when $W / W_{T}$ is finite; otherwise $[W : W_{T}] = \infty$ is a symbol, not a cardinality (The coset set $G / H$ and the index $[G : H]$ of a subgroup).

[F8]

Every simple generator satisfies $s^{2} = 1$ in $W$ (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups).

Proof

technique · direct

1.1F3F6given

The functional $f_{0}$ vanishes exactly on $T$ : ${s \in S : f_{0} (e_{s}) = 0} = S ∖ {s_{0}} = T$ , and all values $f_{0} (e_{s}) = δ_{s, s_{0}}$ are $\geq 0$ , so $f_{0} \in C$ . By [F3] the point stabilizer is ${Stab}_{W} (f_{0}) = W_{S (f_{0})} = W_{T}$ .

2.1step 1.1F1F7given

For $u \in W_{T}$ one has $u \cdot f_{0} = f_{0}$ by step 1.1, so $w^{'} \in w W_{T}$ (that is, $w^{'} = w u$ with $u \in W_{T}$ ) implies $w^{'} \cdot f_{0} = w \cdot (u \cdot f_{0}) = w \cdot f_{0}$ : the orbit map $Φ$ is well defined. If $w \cdot f_{0} = w^{'} \cdot f_{0}$ , then applying $w^{- 1}$ gives $w^{- 1} w^{'} \cdot f_{0} = f_{0}$ , so $w^{- 1} w^{'} \in {Stab}_{W} (f_{0}) = W_{T}$ and $w W_{T} = w^{'} W_{T}$ : $Φ$ is injective. It is surjective onto $W \cdot f_{0}$ by definition, and $Φ (w^{''} w W_{T}) = w^{''} \cdot Φ (w W_{T})$ for all $w^{''}$ , so it is $W$ -equivariant. Hence $Φ$ is a bijection. If $W / W_{T}$ is finite, [F7] and this bijection give $∣ W \cdot f_{0} ∣ = [W : W_{T}]$ ; in the infinite case the equality of sets remains the assertion, without finite-cardinality notation.

2.2step 1.1F1algebra

Fix $v \in W \cdot f_{0}$ and any $w$ with $w \cdot f_{0} = v$ . For $x \in W$ one has $x \cdot f_{0} = w \cdot f_{0}$ if and only if $w^{- 1} \cdot (x \cdot f_{0}) = f_{0}$ , i.e. $(w^{- 1} x) \cdot f_{0} = f_{0}$ , i.e. $w^{- 1} x \in {Stab}_{W} (f_{0}) = W_{T}$ , i.e. $x \in w W_{T}$ . Thus ${x \in W : x \cdot f_{0} = v} = w W_{T}$ .

3.1step 2.2F2F5

The set ${ℓ (x) : x \in w W_{T}}$ is a nonempty subset of $N$ , so it has a least element by [F5]; by step 2.2 that least element is $d (v)$ . By [F2] the left coset $w W_{T}$ has a unique element $d_{w}$ of minimal length, characterized by $ℓ (d_{w} s) > ℓ (d_{w})$ for all $s \in T$ , and then $ℓ (d_{w} u) = ℓ (d_{w}) + ℓ (u)$ for all $u \in W_{T}$ . Hence $d (v) = ℓ (d_{w})$ .

4.1givenF1F8step 3.1

Let $f_{0} = v_{0}, v_{1}, \dots, v_{m} = v$ be a walk in $Γ$ ; an undirected edge may be traversed in reverse; the same generator still sends the preceding vertex to the next because its square is the identity by [F8], so there are $s_{1}, \dots, s_{m} \in S$ with $v_{i} = s_{i} \cdot v_{i - 1}$ , so $v = s_{m} \dots s_{1} \cdot f_{0}$ and $x : = s_{m} \dots s_{1}$ satisfies $x \cdot f_{0} = v$ and $ℓ (x) \leq m$ . Therefore $d (v) \leq ℓ (x) \leq m$ ; taking the least such $m$ gives $d (v) \leq {dist}_{Γ} (f_{0}, v)$ .

4.2step 3.1F1F4F8algebra

Let $v \in W \cdot f_{0}$ and $s \in S$ , and choose $x$ with $x \cdot f_{0} = v$ and $ℓ (x) = d (v)$ by step 3.1. Then $(s x) \cdot f_{0} = s \cdot v$ , so $d (s \cdot v) \leq ℓ (s x) \leq ℓ (x) + 1 = d (v) + 1$ by [F4]. Applying the same estimate to $s \cdot v$ in place of $v$ and using $s \cdot (s \cdot v) = (s^{2}) \cdot v = v$ gives $d (v) \leq d (s \cdot v) + 1$ . Hence $∣ d (s \cdot v) - d (v) ∣ \leq 1$ for all $s, v$ .

5.1step 3.1step 4.1F1algebra

Conversely let $x = s_{1} \dots s_{m}$ be a reduced expression with $x \cdot f_{0} = v$ and $m = d (v)$ , which exists by step 3.1. The sequence $f_{0}, s_{m} \cdot f_{0}, s_{m - 1} s_{m} \cdot f_{0}, \dots, s_{1} \dots s_{m} \cdot f_{0} = v$ is obtained by successively prepending letters. No consecutive vertices agree: if $s_{i}$ fixed the current suffix image $s_{i + 1} \dots s_{m} \cdot f_{0}$ , deleting $s_{i}$ would still send $f_{0}$ to $v$ and give a representative of length at most $m - 1$ , contrary to $m = d (v)$ . Thus every consecutive pair is an edge (self-loops are omitted), and ${dist}_{Γ} (f_{0}, v) \leq m = d (v)$ . With step 4.1 this gives ${dist}_{Γ} (f_{0}, v) = d (v)$ ; in particular $d (f_{0}) = 0$ because $1 \cdot f_{0} = f_{0}$ and $ℓ (1) = 0$ .

6.1step 2.1step 2.2step 3.1F2F6algebra∎

By [F2] every $w \in W$ has a unique factorization $w = d_{w} u$ with $u \in W_{T}$ and $d_{w}$ the minimal element of the left coset $w W_{T}$ , and $ℓ (w) = ℓ (d_{w}) + ℓ (u)$ . By steps 2.1, 2.2 and 3.1 the assignment $w \mapsto d_{w} \cdot f_{0}$ is a map of $W$ onto $W \cdot f_{0}$ whose fibers are exactly the cosets $w W_{T}$ , and $d (d_{w} \cdot f_{0}) = ℓ (d_{w})$ . Summing $t^{ℓ (w)} = t^{d (d_{w} \cdot f_{0})} t^{ℓ (u)}$ over the unique pairs $(d_{w}, u)$ therefore gives $P_{W} (t) = \sum_{v \in W \cdot f_{0}} \sum_{u \in W_{T}} t^{d (v) + ℓ (u)} = (\sum_{v \in W \cdot f_{0}} t^{d (v)}) P_{W_{T}} (t)$ in $Z ⟦ t ⟧$ . Both factors are well-defined series by [F6]: for each $n$ the set ${v : d (v) = n}$ is contained in the image of the finite fiber ${x : ℓ (x) = n}$ under $x \mapsto x \cdot f_{0}$ , hence finite.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passaudited 2026-10-08Open item page →

Finite descent parabolics, parabolic factorization, the Steinberg inclusion-exclusion identity, and rational growth

Statement

Let $(W, S)$ be a Coxeter system with $S$ finite and length function $ℓ$ (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups), with $W_{I}$ , $D_{L}$ , $D_{R}$ as in Standard parabolic subgroups, descent-free one- and two-sided representatives, parabolic and reflection subgroups and the series $P_{A}$ , $D_{I}^{J}$ of Length generating series, descent-class series, spherical subsets, and the multivariate descent polynomial. Put $W^{J} : = {w \in W : ℓ (w s) > ℓ (w) for all s \in J},^{J} W : = {w \in W : ℓ (s w) > ℓ (w) for all s \in J} .$ Then:

(1) Finite descent parabolics and the finite/infinite dichotomy. If $J \subseteq D_{L} (w)$ for some $w \in W$ (equivalently, if $J \subseteq D_{R} (w)$ for some $w$ ), then $W_{J}$ is finite. In particular $W_{D_{L} (w)}$ and $W_{D_{R} (w)}$ are finite for every $w \in W$ . Conversely, if $W_{J}$ is finite with longest element $w_{0} (J)$ , then $D_{L} (w_{0} (J)) = D_{R} (w_{0} (J)) = J$ . Consequently $W$ is finite if and only if some $x \in W$ satisfies $D_{L} (x) = S$ , if and only if some $x$ satisfies $D_{R} (x) = S$ ; and if $W$ is infinite then no element has all descents. If $W$ is finite, then $D_{S}^{S} (t) = t^{ℓ (w_{0})}$ , while if $W$ is infinite then $D_{S}^{S} (t) = 0$ .

(2) Parabolic factorization. For every $J \subseteq S$ the multiplication maps $W^{J} \times W_{J} \to W$ and $W_{J} \times^{J} W \to W$ are bijections and $ℓ$ is additive along them; consequently $P_{W} = P_{W^{J}} P_{W_{J}} = P_{^{J} W} P_{W_{J}}$ in $Z ⟦ t ⟧$ . If the diagram of $(W, S)$ is disconnected with components on the nonempty pairwise disjoint sets $S_{1}, \dots, S_{k}$ , then $W ≅ W_{S_{1}} \times \dots \times W_{S_{k}}$ , $ℓ (w_{1} \dots w_{k}) = \sum_{i} ℓ (w_{i})$ , and $P_{W} = \prod_{i} P_{W_{S_{i}}}$ . When $S = \emptyset$ , the presentation gives $W = {1}$ and this product over no components is $1$ .

(3) Descent inclusion-exclusion. For all $I \subseteq J \subseteq S$ , $D_{I}^{J} (t) = \sum_{J ∖ I \subseteq K \subseteq J} (- 1)^{∣ J ∖ K ∣} P_{W^{S ∖ K}} (t), where W^{S ∖ K} = {w \in W : D_{R} (w) \subseteq K} .$

(4) Steinberg identity. With formal inverses $1 / P_{W_{K}} (t) \in Z ⟦ t ⟧$ (A formal power series is a unit exactly when its constant coefficient is a unit), valid because $P_{W_{K}} (0) = 1$ , $\sum_{K \subseteq S} \frac{(- 1)^{∣ K ∣}}{P_{W_{K}} (t)} = {\begin{cases} \frac{t^{ℓ (w_{0})}}{P_{W} (t)}, & W finite, \\ 0, & W infinite, \end{cases}$ as an identity in $Z ⟦ t ⟧$ . If $W$ is finite, then $P_{W}$ is a polynomial and $t^{ℓ (w_{0})} P_{W} (t^{- 1}) = P_{W} (t)$ rewrites the identity, in the rational function field $Q (t)$ , as $\frac{1}{P_{W} (t^{- 1})} = \sum_{K \subseteq S} \frac{(- 1)^{∣ K ∣}}{P_{W_{K}} (t)} .$

(5) Rationality. Every $P_{W_{K}}$ $(K \subseteq S)$ is a rational formal power series (Rational formal power series, proper presentations and reduced denominators), by induction on $∣ S ∣$ using proper parabolics as the recursive inputs. For $S \neq \emptyset$ , (4) yields the recursions $\frac{1}{P_{W} (t)} = (- 1)^{∣ S ∣ + 1} \sum_{K \neq S} \frac{(- 1)^{∣ K ∣}}{P_{W_{K}} (t)} (W infinite), P_{W} (t) = \frac{t^{ℓ (w_{0})} - (- 1)^{∣ S ∣}}{\sum_{K \neq S} (- 1)^{∣ K ∣} / P_{W_{K}} (t)} (W finite) .$ The denominator in the finite recursion has nonzero constant term. If $S = \emptyset$ , then $W = {1}$ and $P_{W} = 1$ , so no recursion with an empty denominator is asserted. Hence $P_{W} \in Q (t)$ : the growth series of every finite-rank Coxeter system is rational. No choice principle is used.

Facts & Assumptions

Given: A Coxeter system $(W, S)$ with $S$ finite and length function $ℓ$ , its standard parabolics $W_{J} = ⟨ s : s \in J ⟩$ , the descent sets $D_{L}, D_{R}$ , the quotient sets $W^{J},^{J} W$ , and the series $P_{A}$ , $D_{I}^{J}$ of Length generating series, descent-class series, spherical subsets, and the multivariate descent polynomial.

[F1]

$D_{L} (w) = {s \in S : ℓ (s w) < ℓ (w)}$ and $D_{R} (w) = {s \in S : ℓ (w s) < ℓ (w)}$ for $w \in W$ , and $ℓ (s w) - ℓ (w), ℓ (w s) - ℓ (w) \in {\pm 1}$ for all $s \in S$ (Standard parabolic subgroups, descent-free one- and two-sided representatives, parabolic and reflection subgroups (2), Length parity, exchange, two-letter deletion, and faithfulness of the signed reflection action (1)). Reversing a word for $w$ gives a word of the same length for $w^{- 1}$ , so $ℓ (w^{- 1}) = ℓ (w)$ (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups).

[F2]

For every $J \subseteq S$ and every $w \in W$ there is a unique pair $u \in W_{J}$ , $d \in^{J} W$ with $w = u d$ and $ℓ (w) = ℓ (u) + ℓ (d)$ , and then $ℓ (u^{'} d) = ℓ (u^{'}) + ℓ (d)$ for all $u^{'} \in W_{J}$ ; likewise a unique pair $d \in W^{J}$ , $v \in W_{J}$ with $w = d v$ and $ℓ (w) = ℓ (d) + ℓ (v)$ , and then $ℓ (d v^{'}) = ℓ (d) + ℓ (v^{'})$ for all $v^{'} \in W_{J}$ (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (3)).

[F3]

If $x \in W_{J}$ satisfies $ℓ (s x) < ℓ (x)$ for every $s \in J$ , then $W_{J}$ is finite and $x = w_{0} (J)$ is its longest element (An element with full left descent makes the Coxeter group finite and is the longest element (2)).

[F4]

If $W_{J}$ is finite, its longest element $w_{0} (J)$ is unique and satisfies $w_{0} (J)^{2} = 1$ , $ℓ (w_{0} (J) w) = ℓ (w_{0} (J)) - ℓ (w)$ and $ℓ (w w_{0} (J)) = ℓ (w_{0} (J)) - ℓ (w)$ for all $w \in W_{J}$ , and $w_{0} (J) J w_{0} (J)^{- 1} = J$ ; if $W$ is finite then $w_{0} = w_{0} (S)$ satisfies $ℓ (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)(iii),(2)).

[F5]

$W_{J} = {w \in W : S (w) \subseteq J}$ for the support $S (w)$ of any reduced expression of $w$ , $W_{J} \cap S = J$ , and $(W_{J}, J)$ is a Coxeter system whose intrinsic length function is the restriction of $ℓ$ (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (1),(2)).

[F6]

If the diagram of $(W, S)$ is disconnected with components on the nonempty pairwise disjoint sets $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})$ for all $w_{i} \in W_{S_{i}}$ (Disconnected diagrams, direct products, and comparison of invariant forms (1)).

[F7]

For every $A \subseteq W$ , each length fiber is finite and $P_{A} = \sum_{w \in A} t^{ℓ (w)}$ is a well-defined element of $Z ⟦ t ⟧$ , with $P_{A} (0) = 1$ if $1 \in A$ and $P_{A} (0) = 0$ otherwise (Length generating series, descent-class series, spherical subsets, and the multivariate descent polynomial (1)).

[F8]

The coefficientwise sum and Cauchy product make $Z ⟦ t ⟧$ a commutative ring (Cauchy multiplication makes $R ⟦ x ⟧$ a commutative ring containing $R [x]$ as the finitely supported subring).

[F9]

A formal series is a unit if and only if its constant coefficient is a unit; in particular every $P_{W_{K}}$ is a unit because $P_{W_{K}} (0) = 1$ (A formal power series is a unit exactly when its constant coefficient is a unit).

[F10]

In the additive commutative monoid of $Z ⟦ t ⟧$ , finite sums over finite sets are independent of enumeration, invariant under bijective reindexing and split over finite disjoint unions (A finite sum in a commutative monoid indexed by an arbitrary finite set, Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

[F11]

Since $S$ is finite, its power set $P (S)$ is finite ( $∣ P (A) ∣ = 2^{∣ A ∣}$ for finite $A$ ).

[F12]

A series $F \in Z ⟦ t ⟧$ is rational over $Z$ when $F = U / V$ for $U, V \in Z [t]$ with $V (0) \in {1, - 1}$ (Rational formal power series, proper presentations and reduced denominators). Then $F (0) = U (0) / V (0)$ . If also $F (0) \in {1, - 1}$ , then $U (0) \in {1, - 1}$ , so the reciprocal $V / U$ is rational over $Z$ as well.

[F13]

If $w = s_{1} \dots s_{k}$ is a reduced expression and $s \in S$ satisfies $ℓ (s w) = k - 1$ , then $s w = s_{1} \dots \hat{s_{i}} \dots s_{k}$ for some $i$ ; if instead $ℓ (w s) = k - 1$ then $w s = s_{1} \dots \hat{s_{i}} \dots s_{k}$ for some $i$ (Length parity, exchange, two-letter deletion, and faithfulness of the signed reflection action (2)).

[F14]

Induction on a natural number is valid (The principle of mathematical induction).

[F15]

A finite product of finite sets is finite with cardinality the product of their cardinalities, and a finite disjoint union of finite sets is finite with cardinality the sum of their cardinalities (The product rule: $∣ A \times B ∣ = ∣ A ∣ ∣ B ∣$ , and $∣ \prod_{i < m} A_{i} ∣ = \prod_{i < m} ∣ A_{i} ∣$ , The sum rule: a finite disjoint union is finite with $∣ A \cup B ∣ = ∣ A ∣ + ∣ B ∣$ and $∣ ⋃_{i \in I} A_{i} ∣ = \sum_{i \in I} ∣ A_{i} ∣$ , and a sum over a finite index set splits along a partition).

Proof

technique · direct

1.1F1F2F3F4

Let $J \subseteq S$ and $w \in W$ with $J \subseteq D_{R} (w)$ . Write $w = d v$ with $d \in W^{J}$ , $v \in W_{J}$ as in [F2], so $ℓ (w s) = ℓ (d) + ℓ (v s)$ for every $s \in J$ ; since $ℓ (w s) < ℓ (w) = ℓ (d) + ℓ (v)$ by [F1], we get $ℓ (v s) < ℓ (v)$ for all $s \in J$ . Now $D_{L} (x) = D_{R} (x^{- 1})$ for every $x \in W$ , because $ℓ (x^{- 1}) = ℓ (x)$ and $(x s)^{- 1} = s x^{- 1}$ turn $ℓ (x s) < ℓ (x)$ into $ℓ (s x^{- 1}) < ℓ (x^{- 1})$ ; hence $D_{L} (v^{- 1}) = D_{R} (v) \supseteq J$ , and [F3] applied to $v^{- 1} \in W_{J}$ gives that $W_{J}$ is finite and $v^{- 1} = w_{0} (J)$ ; since $w_{0} (J)^{2} = 1$ by [F4], $v = w_{0} (J)$ . Symmetrically, if $J \subseteq D_{L} (w)$ , write $w = u d$ with $u \in W_{J}$ , $d \in^{J} W$ as in [F2]; then $s w = (s u) d$ for $s \in J$ , so $ℓ (s w) = ℓ (s u) + ℓ (d) < ℓ (u) + ℓ (d) = ℓ (w)$ gives $ℓ (s u) < ℓ (u)$ for all $s \in J$ , and [F3] applied to $u$ shows that $W_{J}$ is finite. In particular $W_{D_{L} (w)}$ and $W_{D_{R} (w)}$ are finite for every $w$ , and taking $J = S$ shows that if some $x$ has $D_{L} (x) = S$ or $D_{R} (x) = S$ then $W = W_{S}$ is finite.

1.2F1F4F5F13

Let $W_{J}$ be finite with longest element $w_{0} (J)$ as in [F4]. For $s \in J$ the element $s$ lies in $W_{J}$ , so $ℓ (s w_{0} (J)) = ℓ (w_{0} (J)) - ℓ (s) = ℓ (w_{0} (J)) - 1 < ℓ (w_{0} (J))$ and likewise $ℓ (w_{0} (J) s) < ℓ (w_{0} (J))$ : thus $J \subseteq D_{L} (w_{0} (J)) \cap D_{R} (w_{0} (J))$ . Conversely let $s \in S ∖ J$ and suppose $ℓ (s w_{0} (J)) < ℓ (w_{0} (J))$ . Fix a reduced expression $w_{0} (J) = s_{1} \dots s_{k}$ with all $s_{i} \in J$ (possible by [F5], since $W_{J} = ⟨ J ⟩$ ); by [F13] $s w_{0} (J) = s_{1} \dots \hat{s_{i}} \dots s_{k}$ is a product of elements of $J$ , hence lies in $W_{J}$ , so $s = w_{0} (J) \cdot (s w_{0} (J))^{- 1} \in W_{J}$ and therefore $s \in W_{J} \cap S = J$ by [F5], a contradiction. Since $ℓ (s w_{0} (J)) - ℓ (w_{0} (J)) \in {\pm 1}$ by [F1], it follows that $ℓ (s w_{0} (J)) > ℓ (w_{0} (J))$ , i.e. $s \notin D_{L} (w_{0} (J))$ . The right-handed version uses the right form of [F13] with the same computation; hence $D_{L} (w_{0} (J)) = D_{R} (w_{0} (J)) = J$ . In particular, if $W$ is finite then $D_{L} (w_{0}) = D_{R} (w_{0}) = S$ for $w_{0} = w_{0} (S)$ .

1.3F2F6F7F8F15

Fix $J \subseteq S$ . By [F2] the maps $W^{J} \times W_{J} \to W$ , $(d, v) \mapsto d v$ , and $W_{J} \times^{J} W \to W$ , $(u, d) \mapsto u d$ , are bijections along which $ℓ$ is additive. For each $n \in N$ , the map $(d, v) \mapsto d v$ restricts to a bijection from the finite disjoint union $⨆_{i = 0}^{n} {d \in W^{J} : ℓ (d) = i} \times {v \in W_{J} : ℓ (v) = n - i}$ onto ${w \in W : ℓ (w) = n}$ ; finiteness follows from [F7, F15]. Its cardinality is exactly the Cauchy-product coefficient $[t^{n}] (P_{W^{J}} P_{W_{J}})$ , so coefficientwise equality gives $P_{W} = P_{W^{J}} P_{W_{J}}$ . The same argument with the factorization $w = u d$ gives $P_{W} = P_{^{J} W} P_{W_{J}}$ . If $S = \emptyset$ , then $W = {1}$ and both series and the empty product are $1$ . Otherwise, in the disconnected case [F6] gives an isomorphism $W_{S_{1}} \times \dots \times W_{S_{k}} \to W$ carrying $(w_{1}, \dots, w_{k})$ to $w_{1} \dots w_{k}$ with additive length. Iterating the same coefficient argument over the finite set of components gives $P_{W} = \prod_{i} P_{W_{S_{i}}}$ .

1.4F1F7F8F10F11algebra

Fix $I \subseteq J \subseteq S$ and for $L \subseteq S$ put $E_{L} : = {w \in W : D_{R} (w) = L}$ , a set partition of $W$ indexed by the finite power set $P (S)$ by [F11], so that $P_{W^{S ∖ K}} = \sum_{L \subseteq K} P_{E_{L}}$ for every $K \subseteq S$ by [F7] and the displayed definition in statement (3), while $D_{I}^{J} = \sum_{I \subseteq L \subseteq J} P_{E_{L}}$ . Substituting the first display into the sum of the statement gives $\sum_{J ∖ I \subseteq K \subseteq J} (- 1)^{∣ J ∖ K ∣} \sum_{L \subseteq K} P_{E_{L}} = \sum_{L \subseteq J} P_{E_{L}} c (L)$ with $c (L) : = \sum_{K : (J ∖ I) \cup L \subseteq K \subseteq J} (- 1)^{∣ J ∖ K ∣}$ , a finite interchange licensed by [F8, F10]. Writing $K = J ∖ N$ with $N \subseteq J$ , the condition $K \supseteq (J ∖ I) \cup L$ becomes $N \subseteq M : = J ∖ ((J ∖ I) \cup L)$ and $∣ J ∖ K ∣ = ∣ N ∣$ , so $c (L) = \sum_{N \subseteq M} (- 1)^{∣ N ∣}$ ; when $M \neq \emptyset$ fix $a \in M$ and the map $N \mapsto N △ {a}$ is a fixed-point-free involution of the subsets of $M$ that negates $(- 1)^{∣ N ∣}$ , so $c (L) = 0$ , and when $M = \emptyset$ the sum is the single term $1$ . Now $M = \emptyset$ means $(J ∖ I) \cup L = J$ , and since $L \subseteq J$ this holds exactly when $I \subseteq L$ : each $x \in I$ lies in $J = (J ∖ I) \cup L$ but not in $J ∖ I$ , hence in $L$ , while $I \subseteq L$ gives $(J ∖ I) \cup L \supseteq (J ∖ I) \cup I = J$ . Together with $L \subseteq J$ this is exactly $I \subseteq L \subseteq J$ , so the whole sum equals $\sum_{I \subseteq L \subseteq J} P_{E_{L}} = D_{I}^{J}$ , which is the asserted identity.

2.1step 1.1step 1.2F4F7

By step 1.2, if $W$ is finite then some element (namely $w_{0}$ ) has all left descents and all right descents; by step 1.1, if some element has all descents then $W$ is finite. Hence $W$ is finite if and only if some $x$ satisfies $D_{L} (x) = S$ , if and only if some $x$ satisfies $D_{R} (x) = S$ ; so if $W$ is infinite then no element has all descents. Now $D_{S}^{S} (t) = \sum_{{w : D_{R} (w) = S}} t^{ℓ (w)}$ . If $W$ is infinite the index set is empty, so $D_{S}^{S} = 0$ . If $W$ is finite and $D_{R} (w) = S$ , apply the factorization argument of step 1.1 with $J = S$ : write $w = d v$ with $d \in W^{S}$ and $v \in W_{S}$ . Since $W_{S} = W$ , the set $w W_{S}$ is all of $W$ , so its unique minimal representative is $d = 1$ and $v = w$ ; the argument in step 1.1 then gives $v^{- 1} = w_{0}$ , so $w = v = w_{0}$ ; conversely $D_{R} (w_{0}) = S$ by step 1.2. Hence $D_{S}^{S} (t) = t^{ℓ (w_{0})}$ in the finite case.

3.1step 1.3step 1.4step 2.1F4F7F8F9F10F11algebra

Take $I = J = S$ in step 1.4; since $S ∖ S = \emptyset$ , this gives $D_{S}^{S} (t) = \sum_{K \subseteq S} (- 1)^{∣ S ∖ K ∣} P_{W^{S ∖ K}} (t) = \sum_{K \subseteq S} (- 1)^{∣ K ∣} P_{W^{K}} (t)$ after the substitution $K \mapsto S ∖ K$ . By step 1.3 $P_{W} = P_{W^{K}} P_{W_{K}}$ for every $K \subseteq S$ , and $P_{W_{K}} (0) = 1$ because $W_{K}$ contains the identity, so [F7, F9] gives $P_{W^{K}} = P_{W} / P_{W_{K}}$ in $Z ⟦ t ⟧$ . Substituting and dividing the resulting identity by the unit $P_{W}$ yields $\sum_{K \subseteq S} \frac{(- 1)^{∣ K ∣}}{P_{W_{K}} (t)} = \frac{D_{S}^{S} (t)}{P_{W} (t)}$ , and step 2.1 evaluates the right side as $t^{ℓ (w_{0})} / P_{W} (t)$ when $W$ is finite and as $0$ when $W$ is infinite, which is the asserted two-case identity. In the finite case, $w \mapsto w_{0} w$ is a bijection of $W$ with $ℓ (w_{0} w) = ℓ (w_{0}) - ℓ (w)$ by [F4], so summing over $w$ gives $P_{W} (t) = \sum_{w} t^{ℓ (w_{0}) - ℓ (w)} = t^{N} P_{W} (t^{- 1})$ for $N = ℓ (w_{0})$ , i.e. $t^{N} P_{W} (t^{- 1}) = P_{W} (t)$ as polynomials; hence $t^{N} / P_{W} (t) = 1 / P_{W} (t^{- 1})$ as rational functions and the identity rewrites as $1 / P_{W} (t^{- 1}) = \sum_{K \subseteq S} (- 1)^{∣ K ∣} / P_{W_{K}} (t)$ .

4.1step 3.1F5F7F8F9F10F11F12F14choosealgebra∎

By [F14], induct on rank, proving rationality over $Z$ in the sense of [F12]. At rank zero $W = {1}$ and $P_{W} = 1 / 1$ . Suppose the assertion holds through rank $n$ , and let $∣ S ∣ = n + 1$ . For every proper $K ⊊ S$ , [F5] identifies $P_{W_{K}}$ with the intrinsic series of $(W_{K}, K)$ , so write $P_{W_{K}} = U_{K} / V_{K}$ with integer polynomials and $V_{K} (0) = \pm 1$ . Its constant term is $1$ by [F7], hence $U_{K} (0) = V_{K} (0) = \pm 1$ and its reciprocal is $V_{K} / U_{K}$ . A finite sum of these signed reciprocals is rational over $Z$ : put it over the common denominator $\prod_{K \neq S} U_{K}$ , which has constant term $\pm 1$ . In the infinite case step 3.1 gives $1 / P_{W} = (- 1)^{∣ S ∣ + 1} \sum_{K \neq S} (- 1)^{∣ K ∣} / P_{W_{K}}$ . This rational series has constant term $1$ , so its reciprocal $P_{W}$ is rational by [F12]. In the finite case the same step gives $P_{W} D = t^{N} - (- 1)^{∣ S ∣}$ for $D = \sum_{K \neq S} (- 1)^{∣ K ∣} / P_{W_{K}}$ . Choose $s_{0} \in S$ ; pairing $K$ with $K △ {s_{0}}$ cancels the full alternating subset sum, so $D (0) = \sum_{K \neq S} (- 1)^{∣ K ∣} = - (- 1)^{∣ S ∣} = \pm 1$ . Thus $1 / D$ is rational over $Z$ by [F12], and so is $P_{W} = (t^{N} - (- 1)^{∣ S ∣}) / D$ . This proves the induction, both recursions, and in particular rationality in $Q (t)$ . The single finite-set selection and all unique factorizations use no choice principle.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

Classical Poincare products for A, B, D and I2(m) from the permutation and signed-permutation models

Statement

Fix the following numbering of the classical diagrams, and let $(W, S)$ be the irreducible finite Coxeter system of that type with its canonical reflection representation $ρ : W \to G L (V)$ , $V = R^{S}$ , and Coxeter form $B$ (The real Coxeter form, its radical, reflections, and form-preserving maps, The canonical reflection homomorphism, roots, reflections, and the positive cone):

$A_{n}$ ( $n \geq 1$ ): $S = {s_{1}, \dots, s_{n}}$ , $m (s_{i}, s_{j}) = 3$ if $∣ i - j ∣ = 1$ and $2$ otherwise;
$B_{n}$ ( $n \geq 2$ ): $m (s_{i}, s_{i + 1}) = 3$ $(1 \leq i \leq n - 2)$ , $m (s_{n - 1}, s_{n}) = 4$ , other pairs $2$ ;
$D_{n}$ ( $n \geq 4$ ): $m (s_{1}, s_{3}) = m (s_{2}, s_{3}) = 3$ , $m (s_{i}, s_{i + 1}) = 3$ $(3 \leq i \leq n - 1)$ , other pairs $2$ ;
$I_{2} (m)$ ( $m \geq 3$ ): $S = {s_{1}, s_{2}}$ with $m (s_{1}, s_{2}) = m$ . Write $[k]_{t} : = 1 + t + \dots + t^{k - 1}$ and $[k]_{t}! : = [1]_{t} [2]_{t} \dots [k]_{t}$ . Then:

(1) Permutation and signed-permutation models. For each type the canonical representation is carried by a linear isometry onto the following model representation, in such a way that $ρ (s)$ corresponds to the model's displayed simple reflection: (a) $A_{n}$ : the standard representation of the symmetric group $S_{n + 1}$ on $V ≅ {x \in R^{n + 1} : \sum_{i} x_{i} = 0}$ (equivalently on the quotient $R^{n + 1} / R (1, \dots, 1)$ ), where $ρ (s_{i})$ corresponds to the adjacent transposition $(i i + 1)$ (The finite symmetric group $S_{n}$ , one-line notation, and cycle notation, Adjacent transpositions generate the finite symmetric group $S_{n}$ ); under the resulting isomorphism $W \to S_{n + 1}$ the length is the inversion number (Inversions, inversion number, the sign $sgn (σ) = (- 1)^{inv (σ)}$ , and even and odd permutations), as proved in step 3.1. (b) $B_{n}$ : the group of signed permutations of $[n]$ , acting on $R^{n}$ with orthonormal basis $ε_{1}, \dots, ε_{n}$ , where $ρ (s_{i})$ $(i \leq n - 1)$ exchanges the $i$ -th and $(i + 1)$ -st coordinates and $ρ (s_{n})$ changes the sign of the $n$ -th coordinate; equivalently the Weyl group $W (B_{n})$ of the classical root system $B_{n} = {\pm ε_{i}} \cup {\pm ε_{i} \pm ε_{j}}$ (Root systems of the classical complex Lie algebras, Weyl group). (c) $D_{n}$ : the group of signed permutations with an even number of sign changes, where $ρ (s_{1})$ exchanges coordinates $1, 2$ , $ρ (s_{2})$ maps $(x_{1}, x_{2}) \mapsto (- x_{2}, - x_{1})$ , and $ρ (s_{i})$ $(i \geq 3)$ exchanges coordinates $i - 1, i$ ; equivalently the Weyl group $W (D_{n})$ of the classical root system $D_{n} = {\pm ε_{i} \pm ε_{j} : i < j}$ (Root systems of the classical complex Lie algebras, Weyl group). (d) $I_{2} (m)$ : the dihedral group of order $2 m$ acting on $R^{2}$ generated by the reflections in two lines meeting at angle $π / m$ , in the standard coordinates attached to the two simple roots.

(2) Orbit and quotient polynomial. Choose $s_{0} = s_{n}$ in type $A_{n}$ , $s_{0} = s_{1}$ in type $B_{n}$ , $s_{0} = s_{n}$ in type $D_{n}$ , and $s_{0} = s_{1}$ in type $I_{2} (m)$ . Put $T : = S ∖ {s_{0}}$ and $W_{T} : = ⟨ s : s \in T ⟩$ (Standard parabolic subgroups, descent-free one- and two-sided representatives, parabolic and reflection subgroups (1)), and let $f_{0}$ be the dual fundamental functional of The orbit of a dual fundamental functional: stabilizer, minimal coset length, Schreier distance, and the quotient formula. In type $B_{n}$ , $s_{1}$ is the long-root endpoint and $s_{n}$ is the sign-change endpoint. In type $D_{n}$ , $s_{n}$ is the far endpoint of the chain $s_{1}, s_{3}, s_{4}, \dots, s_{n}$ . Then the orbit $W \cdot f_{0}$ , described in the model coordinates, has the following distance function $d$ , which satisfies $∣ d (s v) - d (v) ∣ \leq 1$ at every generator and is attained by the explicit words displayed in the proof: (a) $A_{n}$ : if $n = 1$ , $T = \emptyset$ and $W_{T} = {1}$ ; if $n \geq 2$ , $W_{T} ≅ A_{n - 1}$ . Writing $y_{j} (x) = x_{j} ∣_{H}$ and $z_{j} = - \sqrt{2} y_{j}$ , the orbit is ${z_{1}, \dots, z_{n + 1}}$ on $H = {x : \sum_{i} x_{i} = 0}$ , with Schreier graph the path $z_{1} - z_{2} - \dots - z_{n + 1}$ ; $d$ takes each value $0, 1, \dots, n$ exactly once and $\sum_{v} t^{d (v)} = [n + 1]_{t}$ . (b) $B_{n}$ ( $n \geq 2$ ): $W_{T} ≅ B_{n - 1}$ . Writing $y_{i} (x) = x_{i}$ and $z_{i} = \sqrt{2} y_{i}$ on $R^{n}$ , $W \cdot f_{0} = {\pm z_{1}, \dots, \pm z_{n}}$ and the Schreier graph is the path $z_{1} - z_{2} - \dots - z_{n} - (- z_{n}) - (- z_{n - 1}) - \dots - (- z_{1})$ ; $d$ takes each value $0, 1, \dots, 2 n - 1$ exactly once and $\sum_{v} t^{d (v)} = [2 n]_{t}$ . (c) $D_{n}$ ( $n \geq 4$ ): $W_{T} ≅ D_{n - 1}$ . Writing $y_{i} (x) = x_{i}$ and $z_{i} = \sqrt{2} y_{i}$ on $R^{n}$ , $W \cdot f_{0} = {\pm z_{1}, \dots, \pm z_{n}}$ , with the Schreier graph obtained from the paths $z_{1} - z_{2} - \dots - z_{n}$ and $(- z_{1}) - (- z_{2}) - \dots - (- z_{n})$ by the cross edges $z_{1} - (- z_{2})$ and $(- z_{1}) - z_{2}$ ; the distances are $0, 1, \dots, n - 2$ and $n, \dots, 2 n - 2$ , each once, together with $n - 1$ twice, so $\sum_{v} t^{d (v)} = [n]_{t} (1 + t^{n - 1})$ . (d) $I_{2} (m)$ ( $m \geq 3$ ): $W_{T} ≅ A_{1}$ ; writing $r = s_{1} s_{2}$ and $v_{k} : = r^{k} \cdot f_{0}$ for $k \in Z / m$ , the Schreier graph is the path $v_{0} - v_{1} - v_{- 1} - v_{2} - v_{- 2} - \dots$ , $d$ takes each value $0, \dots, m - 1$ exactly once and $\sum_{v} t^{d (v)} = [m]_{t}$ .

(3) Products. With the usual low-rank diagram identifications $A_{1} = B_{1}$ , $A_{2} = I_{2} (3)$ , $B_{2} = I_{2} (4)$ , $D_{2} = A_{1} \times A_{1} = I_{2} (2)$ , and $D_{3} = A_{3}$ (verified from their Coxeter presentations in step 5.1), $P_{A_{n}} (t) = [n + 1]_{t}! (n \geq 1), P_{S_{n}} (t) = P_{A_{n - 1}} (t) = [n]_{t}! (n \geq 2),$ $P_{B_{n}} (t) = \prod_{i = 1}^{n} [2 i]_{t} (n \geq 1), P_{D_{n}} (t) = [n]_{t} \prod_{i = 1}^{n - 1} [2 i]_{t} (n \geq 2), P_{I_{2} (m)} (t) = [2]_{t} [m]_{t} (m \geq 3),$ where $P_{B_{1}}$ uses $B_{1} = A_{1}$ , and $P_{D_{2}}, P_{D_{3}}$ use the displayed low-rank identifications. Here $P_{S_{n}}$ refers to the type $A_{n - 1}$ presentation of $S_{n}$ . In particular $P_{A_{n}} (1) = (n + 1)!$ , $P_{B_{n}} (1) = 2^{n} n!$ , and $P_{D_{n}} (1) = 2^{n - 1} n!$ . No invariant degrees and no exceptional-case computation enter this item; the products are proved by the explicit recurrences of (2), with $D_{2}$ treated directly. No choice principle is used.

Facts & Assumptions

Given: An irreducible finite Coxeter system of type $A_{n}$ , $B_{n}$ , $D_{n}$ or $I_{2} (m)$ with its numbering as displayed, its canonical representation $ρ$ on $V = R^{S}$ with Coxeter form $B$ , the Euclidean model space $E$ with orthonormal basis $ε_{1}, \dots$ , and the dual fundamental functional $f_{0}$ of the terminal node.

[F1]

$B$ is the symmetric bilinear form with $B (e_{s}, e_{s}) = 1$ and $B (e_{s}, e_{t}) = - \cos (π / m (s, t))$ for $s \neq t$ ; the reflection with normal $a$ is $r_{a} (v) = v - \frac{2 B (v, a)}{B (a, a)} a$ (The real Coxeter form, its radical, reflections, and form-preserving maps (2),(3)).

[F2]

$ρ : W \to G L (V)$ is the canonical homomorphism with $ρ (s) = r_{e_{s}}$ , and for $s \neq t$ the product $ρ (s) ρ (t)$ has order exactly $m (s, t)$ (The canonical reflection homomorphism, roots, reflections, and the positive cone, Reflections: involutivity, form invariance, fixed hyperplane, and exact rank-two order (3)(iv)).

[F3]

The assignment $s \mapsto g_{s}$ into a group extends uniquely to a homomorphism $W \to G$ whenever $g_{s}^{2} = 1$ and $(g_{s} g_{t})^{m (s, t)} = 1$ for all $s \neq t$ with $m (s, t) < \infty$ (Coxeter matrices, the presented Coxeter group, reduced words, length, and standard parabolic subgroups, Monoid homomorphism and group homomorphism).

[F4]

In the type- $A_{n}$ coordinate model, use the one-based letters $1, \dots, n + 1$ , transported from the library's ${0, \dots, n}$ by the increasing bijection $k \mapsto k + 1$ . The adjacent transpositions $(i i + 1)$ , $1 \leq i \leq n$ , generate this model of $S_{n + 1}$ for $n \geq 1$ ; the inversion number of a permutation is the number of pairs $i < j$ whose values are inverted (Adjacent transpositions generate the finite symmetric group $S_{n}$ , The finite symmetric group $S_{n}$ , one-line notation, and cycle notation, Inversions, inversion number, the sign $sgn (σ) = (- 1)^{inv (σ)}$ , and even and odd permutations).

[F5]

The coordinate root sets displayed for $B_{n}$ and $D_{n}$ in Statement (1) are the root systems of those types (Root systems of the classical complex Lie algebras); the Weyl group of a root system is generated by its root reflections (Weyl group).

[F6]

For the orbit of the dual fundamental functional of $s_{0} \in S$ with $T = S ∖ {s_{0}}$ , the orbit map $W / W_{T} \to W \cdot f_{0}$ is a bijection, $d (v)$ is the minimal length in the corresponding coset and the graph distance in the Schreier graph, and $∣ d (s \cdot v) - d (v) ∣ \leq 1$ for all generators (The orbit of a dual fundamental functional: stabilizer, minimal coset length, Schreier distance, and the quotient formula (1)-(3)).

[F7]

Isometries carry reflections to reflections: if $ϕ$ is a linear isometry and $B (a, a) \neq 0$ , then $ϕ r_{a} ϕ^{- 1} = r_{ϕ (a)}$ ; $r_{- a} = r_{a}$ ; and $g r_{a} g^{- 1} = r_{g a}$ for every orthogonal $g$ (Linear isometries, and orthogonal or unitary operators on finite-dimensional inner product spaces, Invertible linear maps, linear isomorphisms, and inverse linear maps, Real and complex inner product spaces, with the inner product linear in the first argument, Basis of a vector space: a linearly independent spanning subset; and ordered basis: an injective finite list whose image is a basis, The real Coxeter form, its radical, reflections, and form-preserving maps (3), Reflections: involutivity, form invariance, fixed hyperplane, and exact rank-two order (2)).

[F8]

The group generated by a set, a group homomorphism and its isomorphisms, and the order of an element are as in The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups, Monoid homomorphism and group homomorphism, Group isomorphisms, automorphisms and the set $Aut (G)$ , The order $∣ G ∣$ of a finite group and the order $ord (g)$ of an element, with $ord (g) = \infty$ when no positive power of $g$ is the identity, Powers $g^{n}$ : natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$ .

[F9]

For every $T \subseteq S$ , $W_{T} = ⟨ s : s \in T ⟩$ is the standard parabolic; in particular $W_{\emptyset} = {1}$ (Standard parabolic subgroups, descent-free one- and two-sided representatives, parabolic and reflection subgroups (1)).

[F10]

The order of a finite group $G$ means the finite cardinality $∣ G ∣$ of its underlying set (The cardinality $∣ A ∣$ of a finite set).

[F11]

For a polynomial $f$ over a commutative ring, $f (1)$ is its value at $1$ under the polynomial evaluation map (Evaluation and roots of a polynomial in a commutative target ring).

[F12]

$∣ S_{n} ∣ = n!$ for every $n \in N$ (The Lehmer code gives $∣ S_{n} ∣ = n!$ again).

[F13]

For $A \subseteq W$ , $P_{A} (t) = \sum_{w \in A} t^{ℓ (w)}$ (Length generating series, descent-class series, spherical subsets, and the multivariate descent polynomial (1)).

[F14]

For $J \subseteq S$ , put $W^{J} : = {w \in W : ℓ (w s) > ℓ (w) for all s \in J}$ . Multiplication gives a length-additive bijection $W^{J} \times W_{J} \to W$ , so $W^{J}$ consists of the unique minimal representatives of the sets $w W_{J}$ , which are left cosets by Left and right cosets $g H$ and $H g$ of a subgroup, and $P_{W} = P_{W^{J}} P_{W_{J}}$ (Finite descent parabolics, parabolic factorization, the Steinberg inclusion-exclusion identity, and rational growth (2), Left and right cosets $g H$ and $H g$ of a subgroup).

[F15]

The canonical reflection homomorphism $ρ$ is injective (The root-length criterion and faithfulness of the canonical reflection representation (3)).

[F16]

For each $J \subseteq S$ , $(W_{J}, J)$ is the Coxeter system of the restricted matrix and its intrinsic length agrees with the restriction of $ℓ$ (Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (2)).

[F17]

The Gram comparison uses $\cos (π / 3) = 1 / 2$ , $\cos (π / 4) = 1 / \sqrt{2}$ and $\cos (π / 2) = 0$ . Indeed the quarter-turn formulas and parity give $\cos (π - θ) = - \cos θ$ ; with $c = \cos (π / 3) > 0$ the double-angle identity yields $- c = 2 c^{2} - 1$ , hence $(2 c - 1) (c + 1) = 0$ and $c = 1 / 2$ . With $d = \cos (π / 4) > 0$ , the same identity gives $0 = 2 d^{2} - 1$ , hence $d = 1 / \sqrt{2}$ by uniqueness of the nonnegative square root. Positivity follows from strict decrease of cosine on $[0, π]$ and its zero at $π / 2$ (Quarter-turn values and shifts by pi/2 and pi, Parity and the Pythagorean identity for sine and cosine, Double-angle and quadratic power-reduction identities, Signs, monotonicity intervals, and ranges of sine and cosine, Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

Proof

technique · direct

1.1F1F17algebra

Coordinate roots and the Gram isometry. In type $A_{n}$ take $E = H = {x \in R^{n + 1} : \sum_{i} x_{i} = 0}$ and $α_{i} = ε_{i} - ε_{i + 1}$ ; these roots have squared norm $2$ , inner product $- 1$ for adjacent indices and $0$ otherwise. In type $B_{n}$ take $E = R^{n}$ , $α_{i} = ε_{i} - ε_{i + 1}$ for $i < n$ and $α_{n} = ε_{n}$ ; their normalized adjacent inner products are $- \frac{1}{2}$ along the $3$ -edges and $- \frac{1}{\sqrt{2}} = - \cos (π / 4)$ at the $4$ -edge. In type $D_{n}$ take $α_{1} = ε_{1} - ε_{2}$ , $α_{2} = - (ε_{1} + ε_{2})$ and $α_{i} = ε_{i - 1} - ε_{i}$ for $3 \leq i \leq n$ ; the two fork inner products and chain inner products are $- 1$ , and the other pairs are orthogonal. For $I_{2} (m)$ take two normals of length $\sqrt{2}$ with angle $π - π / m$ . In each case the normalized roots ${\hat{α}}_{s}$ have Gram matrix $B (e_{s}, e_{t})$ . They form a basis: the type- $A$ differences form a basis of $H$ , the type- $B$ roots are a coordinate-triangular basis, a relation among the type- $D$ roots has $c_{n} = 0$ and successively $c_{n - 1} = \dots = c_{3} = 0$ , after which $c_{1} - c_{2} = - c_{1} - c_{2} = 0$ forces $c_{1} = c_{2} = 0$ , and the two $I_{2} (m)$ normals are independent. Since $(e_{s})_{s \in S}$ is a basis of $V$ , $ϕ (e_{s}) = {\hat{α}}_{s}$ extends to a linear isometry $ϕ : V \to E$ .

2.1step 1.1F1F2F3F7F8F15algebra

Conjugating the canonical action. By [F7], $ϕ ρ (s) ϕ^{- 1} = r_{{\hat{α}}_{s}}$ . The reflection formula gives the adjacent coordinate swaps in types $A_{n}, B_{n}, D_{n}$ , the sign change of the last coordinate for $s_{n}$ in type $B_{n}$ , the signed swap $(x_{1}, x_{2}) \mapsto (- x_{2}, - x_{1})$ for $s_{2}$ in type $D_{n}$ , and the two line reflections for $I_{2} (m)$ . Let $G = ⟨ r_{{\hat{α}}_{s}} : s \in S ⟩$ . Its displayed generators are involutions, and [F2] transported by $ϕ$ shows that each pair product has the required Coxeter order, so [F3] gives a surjective homomorphism $θ : W \to G$ . The conjugate representation $ψ (w) = ϕ^{- 1} θ (w) ϕ$ agrees with $ρ$ on every generator; uniqueness in [F3] gives $ψ = ρ$ . Since $ρ$ is injective by [F15], $θ$ is injective as well, hence $W ≅ G$ .

3.1step 2.1F4F5F8F10algebra

Identifying the model groups. In type $A_{n}$ , the adjacent swaps generate $S_{n + 1}$ by [F4]; if a permutation acts trivially on $H$ , it fixes every $ε_{i} - ε_{j}$ , which forces it to fix each index, so this action is faithful and $G ≅ S_{n + 1}$ . In one-line notation, right multiplication by an adjacent transposition swaps two adjacent entries, changing only their mutual inversion and hence changing $inv$ by exactly $1$ or $- 1$ . Therefore every word for $π$ has at least $inv (π)$ letters. If $π \neq 1$ , its one-line list has an adjacent descent; swapping that pair on the right reduces the inversion number by one. Repeating this operation reaches the increasing identity list after exactly $inv (π)$ swaps, and reversing the swaps expresses $π$ by a word of that length. Thus $ℓ (π) = inv (π)$ . In type $B_{n}$ , the reflections in roots $ε_{i}$ negate coordinate $i$ , those in $ε_{i} - ε_{j}$ swap coordinates $i, j$ , and those in $ε_{i} + ε_{j}$ swap and negate coordinates $i, j$ ; these formulas show every root reflection is a signed permutation. Conversely the simple reflections $s_{1}, \dots, s_{n - 1}$ are adjacent swaps and $s_{n}$ is one coordinate sign change, so they generate all coordinate permutations and all individual sign changes, hence every signed permutation. As each is in the Weyl group and every root reflection is one of these signed permutations, $G = W (B_{n})$ . In type $D_{n}$ , reflections in $ε_{i} - ε_{j}$ swap coordinates and those in $ε_{i} + ε_{j}$ swap and negate them; each has even sign parity, which is multiplicative under composition. The simple reflections $s_{1}, s_{3}, \dots, s_{n}$ generate all coordinate permutations, and $s_{1} s_{2}$ negates coordinates $1, 2$ ; conjugating this pair negation by permutations gives a negation of any pair of coordinates, and partitioning any even set into pairs gives every even sign pattern. Thus $G$ is the group of even signed permutations, and every root reflection lies in it, so $G = W (D_{n})$ . In type $I_{2} (m)$ , $r = r_{{\hat{α}}_{1}} r_{{\hat{α}}_{2}}$ is a rotation by $2 π / m$ and has order $m$ . Every word in two involutions reduces to an alternating word, hence to one of at most the $m$ powers $r^{k}$ or the $m$ elements $r^{k} r_{{\hat{α}}_{1}}$ . The powers are distinct; the latter elements are distinct and have determinant $- 1$ , unlike the powers, so $∣ G ∣ = 2 m$ and $G$ is dihedral.

4.1step 1.1step 3.1F6F9algebra

Type $A_{n}$ ( $n \geq 1$ ), $s_{0} = s_{n}$ , $T = {s_{1}, \dots, s_{n - 1}}$ . If $n = 1$ , then $T = \emptyset$ and $W_{T} = {1}$ by [F9]; if $n \geq 2$ , deleting $s_{n}$ from the displayed chain leaves type $A_{n - 1}$ . Let $y_{j} (x) = x_{j} ∣_{H}$ and $z_{j} = - \sqrt{2} y_{j}$ . Then $f_{0} \circ ϕ^{- 1} = z_{n + 1}$ : $z_{n + 1}$ vanishes on ${\hat{α}}_{i} = (ε_{i} - ε_{i + 1}) / \sqrt{2}$ for $i \leq n - 1$ and has value $1$ on ${\hat{α}}_{n}$ . By step 3.1 the model group is $S_{n + 1}$ acting by permuting the $z_{j}$ , so $W \cdot f_{0} = {z_{1}, \dots, z_{n + 1}}$ ; each $s_{i}$ swaps $z_{i}, z_{i + 1}$ and fixes the others, giving the path $z_{1} - z_{2} - \dots - z_{n + 1}$ . For $j \leq n$ the word $s_{j} s_{j + 1} \dots s_{n}$ carries $z_{n + 1}$ to $z_{j}$ and has length $n + 1 - j$ ; for $j = n + 1$ the empty word gives $z_{n + 1}$ . Conversely $d^{'} (z_{j}) : = n + 1 - j$ changes by at most one at every generator and vanishes at $z_{n + 1}$ , so $d^{'} \leq d$ by the graph-distance clause of [F6]. Hence $d = d^{'}$ and $\sum_{v} t^{d (v)} = \sum_{j = 1}^{n + 1} t^{n + 1 - j} = [n + 1]_{t}$ .

4.2step 1.1step 3.1F6F9algebra

Type $B_{n}$ ( $n \geq 2$ ), $s_{0} = s_{1}$ , $T = {s_{2}, \dots, s_{n}}$ . Deleting $s_{1}$ leaves the type- $B_{n - 1}$ chain; for $n = 2$ the remaining one-generator Coxeter presentation is type $A_{1}$ , also denoted $B_{1}$ . Put $y_{i} (x) = x_{i}$ and $z_{i} = \sqrt{2} y_{i}$ on $R^{n}$ ; then $f_{0} \circ ϕ^{- 1} = z_{1}$ , since it takes value $1$ on ${\hat{α}}_{1}$ and vanishes on every ${\hat{α}}_{i}$ for $i \geq 2$ . By step 3.1 the model group is the signed permutation group, so $W \cdot f_{0} = {\pm z_{1}, \dots, \pm z_{n}}$ . The generators $s_{i}$ for $2 \leq i \leq n - 1$ swap $z_{i}, z_{i + 1}$ together with their negatives, $s_{1}$ swaps $z_{1}, z_{2}$ , and $s_{n}$ exchanges $z_{n}$ with $- z_{n}$ ; hence the Schreier graph is the path $z_{1} - z_{2} - \dots - z_{n} - (- z_{n}) - \dots - (- z_{1})$ . For $i = 1$ the empty word carries $z_{1}$ to itself; for $2 \leq i \leq n$ , $s_{i - 1} \dots s_{2} s_{1}$ carries $z_{1}$ to $z_{i}$ . For each $1 \leq i \leq n$ , $s_{i} s_{i + 1} \dots s_{n - 1} s_{n} s_{n - 1} \dots s_{1}$ carries $z_{1}$ to $- z_{i}$ . These words have lengths $i - 1$ and $2 n - i$ . Thus $d (z_{i}) \leq i - 1$ and $d (- z_{i}) \leq 2 n - i$ . The function $d^{'} (z_{i}) = i - 1$ , $d^{'} (- z_{i}) = 2 n - i$ vanishes at $z_{1}$ and changes by at most one along every edge, so $d^{'} = d$ by [F6]. Hence $\sum_{v} t^{d (v)} = \sum_{i = 1}^{n} (t^{i - 1} + t^{2 n - i}) = [2 n]_{t}$ .

4.3step 1.1step 3.1F6F9algebra

Type $D_{n}$ ( $n \geq 4$ ), $s_{0} = s_{n}$ , $T = {s_{1}, \dots, s_{n - 1}}$ . Deleting $s_{n}$ leaves the type- $D_{n - 1}$ diagram; when $n = 4$ the remaining three nodes form the path $s_{1} - s_{3} - s_{2}$ , the type- $A_{3}$ presentation denoted $D_{3}$ in the low-rank convention. Put $y_{i} (x) = x_{i}$ and $z_{i} = \sqrt{2} y_{i}$ on $R^{n}$ ; then $f_{0} \circ ϕ^{- 1} = - z_{n}$ , since $- \sqrt{2} y_{n}$ vanishes on ${\hat{α}}_{i}$ for $i \leq n - 2$ , on ${\hat{α}}_{n - 1} = (ε_{n - 2} - ε_{n - 1}) / \sqrt{2}$ and on ${\hat{α}}_{2} = - (ε_{1} + ε_{2}) / \sqrt{2}$ , while it takes value $1$ on ${\hat{α}}_{n} = (ε_{n - 1} - ε_{n}) / \sqrt{2}$ . By step 3.1 the model group is the even signed permutation group, so $W \cdot f_{0} = {\pm z_{1}, \dots, \pm z_{n}}$ . The generators $s_{i}$ for $i \neq 2$ swap adjacent coordinate functionals, while $s_{2}$ sends $z_{1} \mapsto - z_{2}$ and $z_{2} \mapsto - z_{1}$ and fixes $z_{j}$ for $j \geq 3$ ; thus the Schreier graph consists of the paths $z_{1} - \dots - z_{n}$ and $(- z_{1}) - \dots - (- z_{n})$ joined by $z_{1} - (- z_{2})$ and $(- z_{1}) - z_{2}$ . The word $s_{j + 1} s_{j + 2} \dots s_{n}$ carries $- z_{n}$ to $- z_{j}$ for $2 \leq j \leq n$ , so $d (- z_{j}) \leq n - j$ ; the word $s_{1} s_{3} s_{4} \dots s_{n}$ carries $- z_{n}$ to $- z_{1}$ , giving $d (- z_{1}) \leq n - 1$ . For $2 \leq j \leq n$ , $s_{j} s_{j - 1} \dots s_{3} s_{2} s_{1} s_{3} s_{4} \dots s_{n}$ carries $- z_{n}$ to $z_{j}$ (the initial string is empty for $j = 2$ ), and has length $n + j - 2$ . Also $s_{2} s_{3} \dots s_{n}$ carries $- z_{n}$ to $z_{1}$ , so $d (z_{1}) \leq n - 1$ . The function $d^{'} (- z_{j}) = n - j$ and $d^{'} (z_{j}) = n + j - 2$ vanishes at $- z_{n}$ ; each generator changes it by at most one along the displayed graph, so $d^{'} = d$ by [F6]. Its values are $0, \dots, n - 2$ once each, $n - 1$ twice, and $n, \dots, 2 n - 2$ once each. Therefore $\sum_{v} t^{d (v)} = (1 + t + \dots + t^{n - 2}) + 2 t^{n - 1} + (t^{n} + \dots + t^{2 n - 2}) = [n]_{t} (1 + t^{n - 1})$ .

4.4step 1.1step 3.1F6F9algebra

Type $I_{2} (m)$ , $s_{0} = s_{1}$ , $T = {s_{2}}$ . Here $T$ has one node and is type $A_{1}$ . Let $η_{1} \in E^{*}$ be dual to ${\hat{α}}_{1}, {\hat{α}}_{2}$ , so $η_{1} ({\hat{α}}_{1}) = 1$ and $η_{1} ({\hat{α}}_{2}) = 0$ ; then $f_{0} \circ ϕ^{- 1} = η_{1}$ . By step 3.1 the group is dihedral of order $2 m$ , and the cosets $r^{k} W_{T}$ map bijectively to $v_{k} = r^{k} \cdot f_{0}$ by [F6]. Since $s_{2} r = r^{- 1} s_{2}$ and $s_{1} = r s_{2}$ , the left action is $s_{2} \cdot v_{k} = v_{- k}$ and $s_{1} \cdot v_{k} = v_{1 - k}$ . Omitting loops, these edges form the path $v_{0} - v_{1} - v_{- 1} - v_{2} - v_{- 2} - \dots$ through all $m$ vertices. The vertex at position $2 a$ is $(s_{2} s_{1})^{a} \cdot f_{0} = v_{- a}$ and the vertex at position $2 a + 1$ is $s_{1} (s_{2} s_{1})^{a} \cdot f_{0} = v_{a + 1}$ ; these alternating words attain each path position. Thus [F6] gives distances $0, 1, \dots, m - 1$ and $\sum_{v} t^{d (v)} = [m]_{t}$ .

5.1F3F6F8F9F13F14F16step 4.1step 4.2step 4.3step 4.4algebra

Parabolic recurrences and low-rank bases. By [F6], the orbit is in bijection with the cosets $w W_{T}$ and $d (v)$ is the length of the unique minimal representative of its coset. These are left cosets by [F14]. By [F16], each parabolic $W_{T}$ has the restricted Coxeter presentation and its intrinsic length equals the ambient length; deleting the selected node gives the smaller type named in each recurrence. The factorization in [F14] gives $P_{W} = P_{W^{T}} P_{W_{T}}$ ; the minimal representatives in $W^{T}$ therefore give $P_{W^{T}} = \sum_{v} t^{d (v)}$ , so each quotient polynomial in (2) yields the corresponding recurrence. The one-generator presentations for $A_{1}$ and $B_{1}$ coincide; the two-generator presentations for $A_{2}$ and $I_{2} (3)$ both have one edge labelled $3$ , and those for $B_{2}$ and $I_{2} (4)$ both have one edge labelled $4$ . The standard $D_{3}$ diagram is the three-node path $A_{3}$ , so the generator bijection gives a length-preserving presentation isomorphism. Step 4.1 gives $P_{A_{1}} = [2]_{t}$ because $W_{T} = {1}$ , and for $n \geq 2$ gives $P_{A_{n}} = P_{A_{n - 1}} [n + 1]_{t}$ . For $n \geq 2$ , $P_{B_{n}} = P_{B_{n - 1}} [2 n]_{t}$ with $P_{B_{1}} = P_{A_{1}}$ . In type $D_{2}$ , its two generators commute and are involutions. The presentation map $s_{1} \mapsto (1, 0)$ , $s_{2} \mapsto (0, 1)$ into ${0, 1}^{2}$ under componentwise addition modulo $2$ , and the map $(a, b) \mapsto s_{1}^{a} s_{2}^{b}$ back are inverse homomorphisms: the first respects the Coxeter relators, and the second is a homomorphism because the generators commute and square to $1$ . Hence its elements have lengths $0, 1, 1, 2$ , so $P_{D_{2}} = [2]_{t}^{2}$ ; this is the same two-generator presentation as $I_{2} (2)$ under the extended notation and the direct product $A_{1} \times A_{1}$ . Also $P_{D_{3}} = P_{A_{3}}$ by the path-presentation isomorphism above, while for $n \geq 4$ step 4.3 gives $P_{D_{n}} = P_{D_{n - 1}} [n]_{t} (1 + t^{n - 1})$ . Step 4.4 gives $P_{I_{2} (m)} = P_{A_{1}} [m]_{t}$ for $m \geq 3$ .

6.1step 5.1algebra

Telescoping the recurrences. The type- $A$ recurrence gives $P_{A_{n}} = \prod_{k = 2}^{n + 1} [k]_{t} = [n + 1]_{t}!$ and hence $P_{S_{n}} = P_{A_{n - 1}} = [n]_{t}!$ for $n \geq 2$ . The type- $B$ recurrence with $B_{1} = A_{1}$ gives $P_{B_{n}} = \prod_{i = 1}^{n} [2 i]_{t}$ for $n \geq 1$ . In type $D$ , the identity $(1 + t^{n - 1}) [n - 1]_{t} = [2 n - 2]_{t}$ changes the recurrence for $n \geq 4$ into $P_{D_{n}} = [n]_{t} \prod_{i = 1}^{n - 1} [2 i]_{t}$ ; this formula also holds for $D_{3} = A_{3}$ and for $D_{2}$ by step 5.1. Step 5.1 gives $P_{I_{2} (m)} = [2]_{t} [m]_{t}$ .

7.1step 3.1step 5.1step 6.1F10F11F12F13algebra∎

Evaluation at one and group orders. By [F11] and [F13], $P_{W} (1) = \sum_{w \in W} 1 = ∣ W ∣$ (with cardinality as in [F10]); the polynomial evaluation is valid because the groups identified in step 3.1 are finite. The formulas give $P_{A_{n}} (1) = (n + 1)!$ , $P_{B_{n}} (1) = 2^{n} n!$ , $P_{D_{n}} (1) = 2^{n - 1} n!$ for $n \geq 2$ , and $P_{I_{2} (m)} (1) = 2 m$ . These are the group orders: [F12] gives $∣ S_{n + 1} ∣ = (n + 1)!$ and $∣ S_{n} ∣ = n!$ ; each permutation has $2^{n}$ sign assignments in type $B_{n}$ and $2^{n - 1}$ even sign assignments in type $D_{n}$ (the first $n - 1$ signs determine the last); the direct $D_{2}$ presentation in step 5.1 has four elements; and the dihedral group has order $2 m$ by step 3.1. The low-rank coincidences are respected: $P_{A_{1}} = P_{B_{1}}$ , $P_{A_{2}} = [2]_{t} [3]_{t} = P_{I_{2} (3)}$ , $P_{B_{2}} = [2]_{t} [4]_{t} = P_{I_{2} (4)}$ , $P_{D_{2}} = [2]_{t}^{2}$ , and $P_{D_{3}} = [2]_{t} [3]_{t} [4]_{t} = P_{A_{3}}$ . No invariant degrees and no exceptional diagrams are used.

LemmaStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

Exceptional parabolic-orbit length certificates for E6, E7, E8, F4, H3 and H4

Statement

Assume the Axiom of Choice (The Axiom of Choice), used only to install the basic degrees through Basic degrees, exponents, and the graded coinvariant algebra of a finite Coxeter system and A regular Coxeter eigenvector determines the basic degrees: the exponent-residue identification and the complete degree tables for all finite Coxeter types.

Let $(W, S)$ be the irreducible finite Coxeter system of one of the types $E_{6}, E_{7}, E_{8}, F_{4}, H_{3}, H_{4}$ with its canonical reflection representation and positive definite Coxeter form (The real Coxeter form, its radical, reflections, and form-preserving maps, The canonical reflection homomorphism, roots, reflections, and the positive cone, Classification of finite Coxeter systems, including the H and dihedral families, Coxeter diagrams: edges, labels, components and finite type). In each type let $s_{0}$ be the deleted node and $T = S ∖ {s_{0}}$ the parabolic complement recorded in the exact certificate file research/coxeter-scaffold/math-checks/finite-degree-poincare-certificates.json. Its diagrams have edges $E_{6} : (0, 1), (1, 2), (2, 3), (3, 4), (2, 5)$ ; $E_{7} : (0, 1), (1, 2), (2, 3), (3, 4), (4, 5), (2, 6)$ ; $E_{8} : (0, 1), \dots, (5, 6), (2, 7)$ all labelled $3$ ; $F_{4} : (0, 1), (1, 2), (2, 3)$ with $(1, 2)$ labelled $4$ ; $H_{3} : (0, 1), (1, 2)$ with $(0, 1)$ labelled $5$ ; and $H_{4} : (0, 1), (1, 2), (2, 3)$ with $(0, 1)$ labelled $5$ . The deleted nodes are $0, 5, 6, 0, 2, 3$ , respectively. By the intrinsic parabolic presentation in Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (2) and the classification, the resulting Coxeter systems $(W_{T}, T)$ have types $E_{6} \supset D_{5}, E_{7} \supset E_{6}, E_{8} \supset E_{7}, F_{4} \supset B_{3}, H_{3} \supset I_{2} (5), H_{4} \supset H_{3} .$

(1) The certificate. For each type, the certificate records the exact coefficient field $Q$ , $Q (\sqrt{2})$ with ${\sqrt{2}}^{2} = 2$ , or $Q (φ)$ with $φ = 2 \cos (π / 5)$ and $φ^{2} = φ + 1$ (the edge scalars are derived in [F7]); the labelled diagram, deleted node, orbit $W \cdot f_{0}$ of the dual fundamental functional $f_{0}$ of that node, one exact coordinate for every orbit point, the image index for every generator at every orbit point, an applied word reaching every orbit point and its distance, the Coxeter-applied sequence, the exact matrix of the induced dual action in dual-simple-root coordinates, and its characteristic polynomial. The dual simple-reflection matrices are determined exactly by the recorded diagram and the coordinate action in [F2], but are not stored as separate fields. The recorded orbit sizes and quotient polynomials $\sum_{v \in W \cdot f_{0}} t^{d (v)}$ are $\begin{array}{cccc} type & ∣ W \cdot f_{0} ∣ & \sum_{v} t^{d (v)} & parabolic type of W_{T} \\ E_{6} & 27 & [9]_{t} (1 + t^{4} + t^{8}) & D_{5} \\ E_{7} & 56 & [14]_{t} (1 + t^{5}) (1 + t^{9}) & E_{6} \\ E_{8} & 240 & [30]_{t} (1 + t^{6}) (1 + t^{10}) (1 + t^{12}) & E_{7} \\ F_{4} & 24 & [8]_{t} (1 + t^{4} + t^{8}) & B_{3} \\ H_{3} & 12 & [6]_{t} (1 + t^{5}) & I_{2} (5) \\ H_{4} & 120 & [30]_{t} (1 + t^{6}) (1 + t^{10}) & H_{3} \end{array}$

(2) The lengths are the distances. For each type the recorded function $d$ satisfies $∣ d (s v) - d (v) ∣ \leq 1$ at every generator and orbit point, the recorded words attain every recorded value, and the orbit is closed under all generators. Consequently $d$ equals the minimal-coset-length distance of The orbit of a dual fundamental functional: stabilizer, minimal coset length, Schreier distance, and the quotient formula (2)-(3), and $P_{W} (t) = P_{W_{T}} (t) \cdot \sum_{v \in W \cdot f_{0}} t^{d (v)} .$

(3) Degree comparison and the Poincare product for the six types. The basic degrees of A regular Coxeter eigenvector determines the basic degrees: the exponent-residue identification and the complete degree tables for all finite Coxeter types (2) are $D (W) = {2, 5, 6, 8, 9, 12}$ for $E_{6}$ , ${2, 6, 8, 10, 12, 14, 18}$ for $E_{7}$ , ${2, 8, 12, 14, 18, 20, 24, 30}$ for $E_{8}$ , ${2, 6, 8, 12}$ for $F_{4}$ , ${2, 6, 10}$ for $H_{3}$ , and ${2, 12, 20, 30}$ for $H_{4}$ . For the six parabolics, respectively, the degree multisets are $D (W_{T}) = {2, 4, 5, 6, 8}$ , ${2, 5, 6, 8, 9, 12}$ , ${2, 6, 8, 10, 12, 14, 18}$ , ${2, 4, 6}$ , ${2, 5}$ , and ${2, 6, 10}$ , from the same degree suppliers. The certificate verifies coefficientwise that $(\sum_{v \in W \cdot f_{0}} t^{d (v)}) \prod_{d^{'} \in D (W_{T})} [d^{'}]_{t} = \prod_{d \in D (W)} [d]_{t} .$ Therefore, by (2) and induction on rank along $B_{3} \to F_{4}$ , $I_{2} (5) \to H_{3} \to H_{4}$ , and $D_{5} \to E_{6} \to E_{7} \to E_{8}$ , whose initial parabolics are covered by Classical Poincare products for A, B, D and I2(m) from the permutation and signed-permutation models (3), one has $P_{W} (t) = \prod_{d \in D (W)} [d]_{t} = \prod_{i = 1}^{∣ S ∣} (1 + t + \dots + t^{d_{i} - 1})$ for each of the six exceptional types. The six quotient expressions in (1) agree coefficientwise with the corresponding identities and the certificate's exact distance histograms.

Facts & Assumptions

Given: The certificate file research/coxeter-scaffold/math-checks/finite-degree-poincare-certificates.json (version 1, exact arithmetic over the stated fields and no floating point), its six case records with the diagrams, deleted nodes, fields, orbit data, degree multisets and check flags, and for each type the Coxeter system $(W, S)$ , its canonical reflection representation $ρ$ on $V = R^{S}$ with Coxeter form $B$ , and the dual fundamental functional $f_{0} = e_{s_{0}}^{*}$ .

[F1]

$B (e_{s}, e_{s}) = 1$ and $B (e_{s}, e_{t}) = - \cos (π / m (s, t))$ for $s \neq t$ ; the reflection is $r_{a} (v) = v - \frac{2 B (v, a)}{B (a, a)} a$ , is a $B$ -preserving linear involution, and $r_{e_{s}} (e_{t}) = e_{t} + 2 \cos (π / m (s, t)) e_{s}$ for $t \neq s$ (The real Coxeter form, its radical, reflections, and form-preserving maps (2)-(3), Reflections: involutivity, form invariance, fixed hyperplane, and exact rank-two order (2)).

[F2]

In dual simple-root coordinates $f_{t} : = f (e_{t})$ , the dual simple reflection $s \cdot f = f (ρ (s)^{- 1} \cdot)$ acts by $f_{s} \mapsto - f_{s}$ and $f_{t} \mapsto f_{t} + 2 \cos (π / m (s, t)) f_{s}$ for $t \neq s$ ; this is the dual action of The orbit of a dual fundamental functional: stabilizer, minimal coset length, Schreier distance, and the quotient formula, under which $W \cdot f_{0}$ is the orbit of the certificate's seed coordinate.

[F3]

Each table orbit size is the finite cardinality of the listed certificate states (The cardinality $∣ A ∣$ of a finite set). For the orbit of a dual fundamental functional, $d (v)$ is the minimal length in the corresponding left coset $w W_{T}$ (Left and right cosets $g H$ and $H g$ of a subgroup), equals graph distance in the Schreier graph, satisfies $∣ d (s \cdot v) - d (v) ∣ \leq 1$ , and $P_{W} = P_{W_{T}} \sum_{v} t^{d (v)}$ (The orbit of a dual fundamental functional: stabilizer, minimal coset length, Schreier distance, and the quotient formula (2)-(4)).

[F4]

The degree tables $D (W)$ and $D (W_{T})$ displayed in the Statement are the basic degrees of Basic degrees, exponents, and the graded coinvariant algebra of a finite Coxeter system and A regular Coxeter eigenvector determines the basic degrees: the exponent-residue identification and the complete degree tables for all finite Coxeter types (1)-(3). Their Axiom-of-Choice premise is assumed here (The Axiom of Choice).

[F5]

The classical products $P_{B_{3}} = [2]_{t} [4]_{t} [6]_{t}$ , $P_{I_{2} (5)} = [2]_{t} [5]_{t}$ , and $P_{D_{5}} = [2]_{t} [4]_{t} [5]_{t} [6]_{t} [8]_{t}$ are proved in Classical Poincare products for A, B, D and I2(m) from the permutation and signed-permutation models (3).

[F6]

The six diagrams are the standard $E_{6}, E_{7}, E_{8}, F_{4}, H_{3}, H_{4}$ diagrams of the classification, so $W$ is finite and the Coxeter form is positive definite (hence its Gram matrix is invertible); deleting the stated node leaves the displayed standard parabolic diagram, and Support, intrinsic parabolic presentations, minimal coset representatives and length additivity, with the type-A identification (2) identifies the subgroup generated by that node set with the Coxeter system on the restricted matrix. In particular $W_{T}$ is finite as a subgroup of $W$ (Classification of finite Coxeter systems, including the H and dihedral families (1), Coxeter diagrams: edges, labels, components and finite type (1)-(2)).

[F7]

Exact arithmetic in the three coefficient fields. For $m = 3, 4, 5$ , put $x_{m} = 2 \cos (π / m) > 0$ ; positivity follows from $0 < π / m < π / 2$ , strict decrease of cosine on $[0, π]$ , and $\cos (π / 2) = 0$ (Pi as twice the smallest positive zero of cosine, Signs, monotonicity intervals, and ranges of sine and cosine, Quarter-turn values and shifts by pi/2 and pi). The power-series definition gives $\cos 0 = 1$ , and the cosine addition formulas and parity give $C_{k + 1} = 2 c C_{k} - C_{k - 1}$ for $C_{k} = \cos (k θ)$ , $C_{0} = 1$ , and $C_{1} = c = \cos θ$ , so $C_{3} = 4 c^{3} - 3 c$ and $C_{5} = 16 c^{5} - 20 c^{3} + 5 c$ (Sine and cosine defined by their real power series, The addition formulas for sine and cosine, Parity and the Pythagorean identity for sine and cosine). At $θ = π / 3$ , $C_{3} = \cos π = - 1$ gives $(x_{3} - 1)^{2} (x_{3} + 2) = 0$ , hence $x_{3} = 1$ . At $θ = π / 4$ , the double-angle identity and $\cos (π / 2) = 0$ give $x_{4}^{2} = 2$ , so $x_{4} = \sqrt{2}$ by positivity and uniqueness of the nonnegative square root (Double-angle and quadratic power-reduction identities, Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ). At $θ = π / 5$ , $C_{5} = \cos π = - 1$ gives $(x_{5} + 2) (x_{5}^{2} - x_{5} - 1)^{2} = 0$ , hence $x_{5}^{2} = x_{5} + 1$ ; setting $φ = x_{5}$ gives the stated real quadratic field relation. Thus the edge scalars are $1$ for label $3$ , $\sqrt{2}$ for label $4$ , and $φ$ for label $5$ .

[F8]

The characteristic polynomial of the recorded bipartite Coxeter matrix is computed from exact matrix entries by the adjugate/Newton trace argument and agrees with the polynomial recorded in the certificate (The six exceptional Coxeter spectra: characteristic polynomials, orders and spectral exponents from exact matrices (Statement), Proof (2.1), (3.1), (4.1), (6.1)).

Proof

technique · exact finite coordinate certificate, followed by the orbit-distance argument and rank induction

1.1F1F2F6F7F8given

Data and dual matrices. For each of the six rows, [F6] identifies the recorded diagram with the standard diagram of the type and the recorded parabolic with the stated type, and the deleted nodes of the statement are exactly the certificate's deleted-node entries. By [F7] every edge scalar is exact in the recorded coefficient field; [F2] then gives the exact dual simple-reflection matrices in dual simple-root coordinates, while nonedges have scalar $2 \cos (π / 2) = 0$ . The script applies these matrices to the seed coordinate vector, performs exact breadth-first search, and records each state, each generator image, an attaining word and its graph distance. The certificate matrix is for the dual action. If $R_{t}$ is a canonical simple-reflection matrix and $G$ is the Gram matrix, then $R_{t}^{T} G R_{t} = G$ and $R_{t}^{2} = I$ by [F1], so its dual matrix $R_{t}^{T} = G R_{t} G^{- 1}$ . Multiplying in the same recorded order shows that the dual-action Coxeter matrix is similar to the canonical Coxeter matrix; thus their characteristic polynomials agree. The canonical characteristic polynomial is the exact trace result of [F8], and the certificate also checks its cyclotomic factorization. The seven certificate flags (orbit closure, word upper bounds, edge-distance lower bounds, reflection involutions, the Poincare product identity, the cyclotomic spectrum identity, and the final characteristic recurrence) are true; rerunning the script reproduces the certificate byte for byte. Thus these are exact coordinate computations, with no floating-point approximation.

2.1step 1.1F3algebra

The recorded lengths are the distances. Fix one of the six types. The recorded state set contains the seed and is closed under every generator, and every recorded state is reached from the seed by its recorded generator sequence; hence it is exactly the orbit $W \cdot f_{0}$ . Let $d^{'}$ be the recorded distance. Each recorded word has length $d^{'}$ , so the graph distance $d$ is at most $d^{'}$ . Conversely, the certificate verifies that $d^{'}$ changes by at most one along every generator edge and vanishes at the seed; summing this bound along any edge path gives $d^{'} \leq d$ . Therefore $d^{'} = d$ , which by [F3] is the minimal left-coset length. The recorded orbit sizes and distance polynomials are thus correct, and [F3] gives $P_{W} = P_{W_{T}} \sum_{v} t^{d (v)}$ .

3.1step 2.1F4F5algebra∎

Degree comparison and induction. The exact coefficient check of the Poincare product identity agrees with the degree multisets of [F4]. The six identities reduce to $[4]_{t} (1 + t^{4} + t^{8}) = [12]_{t}$ , $[5]_{t} (1 + t^{5}) = [10]_{t}$ , $[9]_{t} (1 + t^{9}) = [18]_{t}$ , $[6]_{t} (1 + t^{6}) = [12]_{t}$ , $[10]_{t} (1 + t^{10}) = [20]_{t}$ , and $[12]_{t} (1 + t^{12}) = [24]_{t}$ , where $[n]_{t} = 1 + t + \dots + t^{n - 1}$ ; multiplying by the corresponding parabolic degree products gives exactly the six ambient degree products in the statement. Using the quotient factorization established in step 2.1, each identity converts a known $P_{W_{T}}$ into $P_{W}$ . For $F_{4}$ , [F5] gives $P_{B_{3}} = [2]_{t} [4]_{t} [6]_{t}$ , and the first relation gives $P_{F_{4}} = [2]_{t} [6]_{t} [8]_{t} [12]_{t}$ . For $H_{3}$ , [F5] gives $P_{I_{2} (5)} = [2]_{t} [5]_{t}$ , and the second relation gives $P_{H_{3}} = [2]_{t} [6]_{t} [10]_{t}$ ; the fourth and fifth relations then give $P_{H_{4}} = [2]_{t} [12]_{t} [20]_{t} [30]_{t}$ . For $E_{6}$ , [F5] gives $P_{D_{5}} = [2]_{t} [4]_{t} [5]_{t} [6]_{t} [8]_{t}$ , and the first relation gives $P_{E_{6}} = [2]_{t} [5]_{t} [6]_{t} [8]_{t} [9]_{t} [12]_{t}$ ; the second and third relations give $P_{E_{7}} = [2]_{t} [6]_{t} [8]_{t} [10]_{t} [12]_{t} [14]_{t} [18]_{t}$ ; the fourth, fifth and sixth relations give $P_{E_{8}} = [2]_{t} [8]_{t} [12]_{t} [14]_{t} [18]_{t} [20]_{t} [24]_{t} [30]_{t}$ . Each result is $\prod_{d \in D (W)} [d]_{t} = \prod_{i = 1}^{∣ S ∣} (1 + t + \dots + t^{d_{i} - 1})$ . Choice enters only through the degree determinations of [F4]; the certificate's orbit and distance verification is choice-free.

TheoremStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-08Open item page →

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.

5 · Examples, counterexamples and false statements

None yet.

Coxeter Descents, Poincaré Polynomials, and Growth

1 · Prerequisites

2 · Summary

Definition and conventions

Main results

Prerequisites and reading

3 · Logical flowchart

4 · Definitions, theorems and proofs

Length generating series, descent-class series, spherical subsets, and the multivariate descent polynomial

Definition

The orbit of a dual fundamental functional: stabilizer, minimal coset length, Schreier distance, and the quotient formula

Statement

Facts & Assumptions

Proof

Finite descent parabolics, parabolic factorization, the Steinberg inclusion-exclusion identity, and rational growth

Statement

Facts & Assumptions

Proof

Classical Poincare products for A, B, D and I2(m) from the permutation and signed-permutation models

Statement

Facts & Assumptions

Proof

Exceptional parabolic-orbit length certificates for E6, E7, E8, F4, H3 and H4

Statement

Facts & Assumptions

Proof

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

Statement

Facts & Assumptions

Proof

5 · Examples, counterexamples and false statements

Sources