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

4.1 The toggle action

Definition 4.1 Symmetric difference
#

For \(D, E \subseteq \{ 0, \dots , n-1\} \), \(D \, \triangle \, E = (D \setminus E) \cup (E \setminus D)\).

Definition 4.2 Single-position toggle

\(D\, \triangle \, \{ i\} = D \, \triangle \, \{ i\} \) flips the membership of position \(i\) in \(D\).

Lemma 4.3 Toggle is an involution

\((D\, \triangle \, \{ i\} )\, \triangle \, \{ i\} = D\).

Remark 4.4 Stanley Fact #2 as block-toggle calculus
#

Stanley’s Fact #2 (EC1 pp. 57–58) describes how the descent set changes under \(\psi _{i}\): in the right-only-child case \(D(\psi _{i}(w)) = D(w) \, \triangle \, \{ i\} \), while in the two-children case \(D(\psi _{i}(w)) = D(w) \, \triangle \, \{ i-1, i\} \).

The combinatorial heart of this — that toggling a single descent at position \(i\) propagates correctly through “blocks” of consecutive descents/ascents — is captured in by \(\texttt{block\_ left\_ le}\), \(\texttt{block\_ right\_ ge}\), \(\texttt{block\_ descent\_ chain}\), \(\texttt{block\_ chain\_ step}\), \(\texttt{block\_ chain\_ values}\) (all \(\rocqok \)).