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

5.2 Stanley Proposition 1.6.4

Proposition 5.3 Stanley Prop 1.6.4: omega-monotonicity of \(\beta \)

Stanley’s statement (verbatim, EC1 p. 60):

Let \(S, T \subseteq [n-1]\). If \(\omega (S) \subsetneq \omega (T)\), then \(\beta _n(S) {\lt} \beta _n(T)\).

Our formalization, for \(D, E \subseteq \{ 0, \dots , m\} \):

\[ \omega (D) \subsetneq \omega (E) \; \Longrightarrow \; \beta (D) {\lt} \beta (E). \]
Proof outline (faithful to Stanley)

Pick \(k \in \omega (E) \setminus \omega (D)\). By 3.8 — Stanley’s identity \(\Phi _{w} = \sum _{\omega (X) \supseteq S_w} u_{X}\) — for every permutation \(\sigma \) with descent set \(D\), the bit-vector \(\texttt{descent\_ to\_ bvec}(D)\) lies in \(\texttt{expand\_ cde}(\Phi _{\texttt{perm\_ to\_ seq}(\sigma )})\). The same holds for \(\texttt{descent\_ to\_ bvec}(E)\) whenever \(\omega (E) \supseteq S_w\).

The witness \(\texttt{witness\_ perm}\) from 5.1, instantiated at \(i = k\), gives a sequence with cd-monomial \(c^{k-1}\, d\, c^{n-2-k}\) and \(S_w = \{ k\} \). Hence \(\omega (E) \supseteq \{ k\} = S_w\) but \(\omega (D) \not\supseteq \{ k\} \) (since \(k \notin \omega (D)\)). This produces a permutation \(\sigma \) with \(D(\sigma ) = E\) that is not in the image of any class map starting from a permutation with descent set \(D\). Counting, via 3.9 and the \(M\)-equivalence class enumeration, then yields \(\beta (D) {\lt} \beta (E)\).