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

4 The toggle action and the \(\omega (S)\) map

This chapter formalizes Stanley EC1 §1.6.3, pp. 57–60: the single-position toggle action on descent sets (the combinatorial shadow of Fact #2), the \(\omega (S)\) map characterizing when consecutive positions of \(S\) flip membership, and Stanley’s equation (1.65) (p. 60) — the alternating descent set is exactly the one with \(\omega (S)\) equal to the universal set. These ingredients feed directly into Proposition 1.6.4 and Corollary 1.6.5 (Chapter 5).