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

6.4 The major index

Definition 6.13 Major index
#

The major index is the sum of (1-indexed) descent positions:

\[ \mathrm{maj}(\sigma ) \; =\; \sum _{i \in D(\sigma )} (i + 1) \; =\; \sum _{i \in D(w)} i \quad (\text{Stanley's notation, p.~ 22}). \]
Lemma 6.14 Identity has zero major index

\(\mathrm{maj}(\mathrm{id}) = 0\).

Lemma 6.15 Major index bound

\(\mathrm{maj}(\sigma ) \leq \binom {n+1}{2}\). The maximum is achieved by the order-reversing permutation, where every position is a descent and the sum is \(1 + 2 + \dots + n = \binom {n+1}{2}\).

Theorem 6.16 Major index reversal identity

For \(\rev _n \in \mathfrak {S}_{n+1}\),

\[ \mathrm{maj}(\rev _n \cdot \sigma ) + (n + 1) \cdot \operatorname {des}(\sigma ) \; =\; \binom {n+1}{2} + \mathrm{maj}(\sigma ). \]

The naive identity \(\mathrm{maj}(\rev _n \cdot \sigma ) = \binom {n+1}{2} - \mathrm{maj}(\sigma )\) is false in general: the asymmetry comes from \(\mathrm{maj}\)’s 1-indexed positions. The correct identity above accounts for it via the per-descent offset \((n - i) + (i + 1) = n + 1\).