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

3.3 Stanley’s identity for \(\Phi _{w}\)

The next theorem is the load-bearing intermediate step in Stanley’s proof of Proposition 1.6.4 (p. 60–61). It says that the bit-strings in \(\texttt{expand\_ cde}\, (\Phi _{w})\) are exactly those whose induced descent pattern is compatible with \(S_w\) (the position set of D-letters in \(\Phi _{w}\), see 4 and Chapter 5).

Theorem 3.8 Stanley’s \(\Phi _{w} = \sum _{\omega (X) \supseteq S_w} u_{X}\)

For every uniq \(w\) with \(|w| \geq 2\) and every bit-string \(X\) with \(|X| = |w| - 1\):

\[ X \in \texttt{expand\_ cde}\, (\Phi _{w}) \; \Longleftrightarrow \; \forall k \in S_w,\; \; k \in \omega (\, \text{descent positions of }X\, ). \]

This formalizes Stanley’s identity at the top of EC1 p. 61 inside the proof of Prop 1.6.4.

The supporting bit-level definitions (\(\texttt{cde\_ width}\), \(\texttt{cde\_ total\_ width}\), \(\texttt{cde\_ offset}\), \(\texttt{D\_ offsets}\), \(\texttt{expand\_ cde\_ mem\_ iff}\)) live in .