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

3.1 The cd-letter alphabet

Definition 3.1 cd-letter alphabet
#

\(\texttt{cde} \; ::=\; \mathtt{C\_ letter} \; \mid \; \mathtt{D\_ letter} \; \mid \; \mathtt{E\_ letter}\). These correspond to Stanley’s cd-letters \(\mathtt{c}\), \(\mathtt{d}\) and the deleted endpoint \(\mathtt{e}\).

Definition 3.2 Vertex classification

Position \(i\) in \(w\) is classified as:

\[ \mathrm{classify\_ vertex\_ cde}(i, w) \; =\; \begin{cases} \mathtt{E\_ letter} & \text{if $i$ is not internal,} \\ \mathtt{D\_ letter} & \text{if $i$ is internal with left child,} \\ \mathtt{C\_ letter} & \text{if $i$ is internal without left child.} \end{cases} \]
Definition 3.3 Unfiltered and cd-monomials

\(\Phi '_{w} = [\, \mathrm{classify\_ vertex\_ cde}(i, w) : i \in \{ 0, \dots , |w|-1\} \, ]\) is the unfiltered list of cd-letters by position. \(\Phi _{w}\) is \(\Phi '_{w}\) with \(\mathtt{E\_ letter}\)s filtered out — Stanley’s \(\Phi _w\), the cd-monomial associated with \(w\) (EC1 pp. 58–59).

Theorem 3.4 Stanley Fact #1, well-definedness

For every \(\mathrm{ss}\) and every uniq \(w\), \(\Phi _{\texttt{apply\_ psis}(\mathrm{ss})(w)} = \Phi _{w}\).

Equivalently: \(\Phi _{w}\) depends only on the M-equivalence class \([w]\) — equivalently, only on \(M(w)\) as an unlabelled tree. This is the well-definedness clause of Stanley’s Fact #1 (EC1 p. 57). Internally it follows from the shape-invariance lemmas in 2.13.