6 Cycles, inversions, and the major index

This chapter formalizes Stanley EC1 §1.3 (cycles and inversions), the section that introduces the two foundational permutation statistics beyond descents: the cycle count \(c(w)\) and the two Mahonian statistics inv and maj. It then covers Foata’s first fundamental bijection and MacMahon’s inv-maj equidistribution, the \(q\)-factorial generating function and the bivariate \(q\)-Eulerian polynomial from §1.4, and the longest alternating subsequence characterization from §1.6.2. A final section records the partial formalization of §1.6.4 (André’s reflection method): the headline recurrence \(2 E_{n+2} = \sum _k \binom {n+1}{k} E_k E_{n+1-k}\) is proven modulo one named admit, in the out-of-build-chain file experimental/reflection.v.

This chapter uses the same indexing convention as Chapter 1: Stanley’s \(w \in \mathfrak {S}_n\) becomes our \(\sigma \in \mathfrak {S}_{n+1}\), and Stanley’s descent positions \(1, \dots , n-1\) become our \(\{ 0, \dots , n-1\} \) via the index shift.