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

4.2 The \(\omega (D)\) map

Definition 4.5 The omega map on descent sets
#

For \(D \subseteq \{ 0, \dots , n\} \), the omega set is

\[ \omega (D) \; =\; \{ \, k \in \{ 0, \dots , n-1\} : (k \in D) \oplus (k+1 \in D)\, \} \; \subseteq \; \{ 0, \dots , n-1\} . \]

This is exactly Stanley’s \(\omega (S)\) from EC1 just before eq. (1.64), p. 60: positions \(k\) where exactly one of \(\{ k, k+1\} \) lies in \(D\). Equivalently, \(\omega (D) = D \, \triangle \, (D - 1)\) where \(D - 1\) is \(D\) shifted by one.

Lemma 4.6 Membership criterion for \(\omega (D)\)

\(k \in \omega (D)\) iff toggling \(D\) at one of \(\{ k, k+1\} \) flips the membership at the other position.