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

1.3 The refined count \(\beta _n(S)\)

Definition 1.11 Set-refined descent count
#

For \(D \subseteq \{ 0, \dots , n-1\} \),

\[ \beta (D) = \# \{ \sigma \in \mathfrak {S}_{n+1} : D(\sigma ) = D\} . \]

This is Stanley’s \(\beta _n(S)\) from EC1 eq. (1.32), p. 30.

Lemma 1.12 Boundary cases
#

\(\beta (\emptyset ) = 1\) (only the identity has empty descent set) and \(\beta (\{ 0, \dots , n-1\} ) = 1\) (only the order-reversing permutation has full descent set).

Theorem 1.13 Total partition by descent set

\(\sum _{D \subseteq \{ 0, \dots , n-1\} } \beta (D) = (n+1)!\).

Theorem 1.14 Refining the Eulerian count

For each \(0 \leq k \leq n\),

\[ \sum _{|D| = k} \beta (D) = A_{n+1,k+1}. \]

Aggregating \(\beta \) over descent sets of fixed size recovers the Eulerian number.

Lemma 1.15 Reversal symmetry of \(\beta \)

\(\beta (D) = \beta (\, \rev _n \cdot D^{c}\, )\), where \(D^{c}\) denotes the set complement and \(\rev _n\) acts pointwise. In particular the two alternating descent sets have equal \(\beta \)-value.