5.2 Stanley Proposition 1.6.4
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\} \):
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)\).