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

6.8 Longest alternating subsequences (Stanley §1.6.2)

Definition 6.27 Turning-point set

Position \(i \in \{ 0, \dots , n-1\} \) is a turning point of \(\sigma \in \mathfrak {S}_{n+2}\) if the direction of \(\sigma \) changes between slot \(i\) and slot \(i+1\):

\[ \mathrm{is\_ turn}(\sigma , i) \; :=\; \mathrm{is\_ descent}(\sigma , i) \, \oplus \, \mathrm{is\_ descent}(\sigma , i+1). \]

\(\mathrm{turn\_ count}(\sigma ) = \# \{ i \in \{ 0, \dots , n-1\} : \mathrm{is\_ turn}(\sigma , i)\} \).

Definition 6.28 Longest alternating subsequence
#

\(\mathrm{as}(\sigma )\) is the length of the longest alternating subsequence of \(\sigma \), formalized as

\[ \mathrm{as\_ perm\_ max}(\sigma ) \; :=\; \max _{I \subseteq \{ 0, \dots , n+1\} } \{ |I| : \text{the subseq of }\sigma \text{ at positions }I\text{ is alternating}\} . \]
Theorem 6.29 Existence direction

\((\mathrm{turn\_ count}(\sigma )).+2 \leq \mathrm{as\_ perm\_ max}(\sigma )\).

Witness: \(I = \{ 0, n+1\} \cup \{ (\mathrm{val}\, t).+1 : t \text{ is a turning point of }\sigma \} \). Cardinality is \(\mathrm{turn\_ count}(\sigma ) + 2\) (boundary endpoints plus one position per turn). Alternation is verified between consecutive picks via the inter-turn monotonicity lemma applied to the no-turn slot interval between them.

Theorem 6.30 Upper bound

\(\mathrm{as\_ perm\_ max}(\sigma ) \leq (\mathrm{turn\_ count}(\sigma )).+2\).

Proved via the global bound chain: flip_count (number of direction changes in a boolean sequence) is monotone under subsequence, so \(\mathrm{flip\_ count}(\mathrm{sign\_ seq}(\mathrm{pick\_ seq}\, \sigma \, I)) \leq \mathrm{flip\_ count}(\mathrm{sign\_ seq}(\mathrm{perm\_ seq}\, \sigma ))\). The right-hand side equals \(\mathrm{turn\_ count}(\sigma )\) via the bridge .

Corollary 6.31 Alternating-subsequence characterization

Stanley EC1 §1.6.2. For every \(\sigma \in \mathfrak {S}_{n+2}\),

\[ \mathrm{as}(\sigma ) \; =\; \mathrm{turn\_ count}(\sigma ) + 2. \]

The longest alternating subsequence has length exactly two more than the number of turning points: one element from each “monotone run” of \(\sigma \), plus one boundary element.

Formalization remark. This took five sequential interactive subagent sessions. The naive “leftmost turn in \([\sigma _i, \sigma _{i+2})\)” injection (mapping each subseq sign-flip to a turn) is not injective — adjacent flips can share a turn-window. Session B-4 pivoted from per-interval to a global bound via the subseq-monotonicity of \(\mathrm{flip\_ count}\).