Permutation descents, Eulerian numbers, and the cd-index
A Rocq / MathComp formalization of Stanley EC1 §1.4 + §1.6

6.7 The \(q\)-Eulerian polynomial — joint \((\mathrm{maj},\operatorname {des})\) distribution

Definition 6.24 \(q\)-Eulerian polynomial

Stanley EC1 §1.4. The bivariate generating function for the joint distribution of \((\mathrm{maj}, \operatorname {des})\) over \(\mathfrak {S}_{n+1}\):

\[ A_n(q, t) \; :=\; \sum _{\sigma \in \mathfrak {S}_{n+1}} q^{\mathrm{maj}(\sigma )} \cdot t^{\operatorname {des}(\sigma )}. \]

Formalized in \(\mathbb {Z}[q][t]\) (mathcomp’s {poly {poly int}}).

Theorem 6.25 Specialization \(t = 1\) — the \(q\)-factorial

\(A_n(q, 1) = [n+1]_q!\). Setting \(t = 1\) collapses the bivariate to the marginal generating function for \(\mathrm{maj}\), which is the q-factorial by 6.23.

Theorem 6.26 Specialization \(q = 1\) — the classical Eulerian polynomial

\(A_n(1, t) = \mathrm{eul\_ pol}_n(t) := \sum _{k=0}^{n} A_{n+1, k+1} \cdot t^k\). Setting \(q = 1\) drops the \(\mathrm{maj}\) weight, leaving the classical Eulerian polynomial \(\sum _\sigma t^{\operatorname {des}(\sigma )}\). Formalized via the rmorphism wrapper \(\mathrm{horner\_ eval}(1)\) applied coefficient-wise across the outer polynomial.