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

5.1 The witness construction

Definition 5.1 Stanley’s witness \(\Phi _{w} = c^{i-1}\, d\, c^{n-2-i}\)
✓
#

Uses

Rocq declarations

For \(n, k \in \mathbb {N}\), \(\texttt{witness\_ perm}(n, k)\) is an explicit sequence whose cd-monomial is \(c^{k-1}\, d\, c^{n-2-k}\) and whose \(S_w\)-set equals \(\{ k\} \).

This is exactly Stanley’s witness from the proof of Proposition 1.6.4 (EC1 p. 61):

“If \(i \in \omega (T) \setminus \omega (S)\) then let \(\Phi _{w} = c^{i-1}\, d\, c^{n-2-i}\), so \(S_w = \{ i\} \).”
Lemma 5.2 The witness is a permutation
✓
#

Uses

Rocq declarations

\(\texttt{witness\_ perm}(n, k)\) is a uniq sequence of length \(n\) whose multiset of values is \(\{ 0, \dots , n-1\} \). Combined with 5.1, this gives a permutation \(\sigma _{n, k} \in \mathfrak {S}_{n}\) with the prescribed cd-monomial.