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

2.2 Windows, internal vertices, and left children

For a position \(i\) in \(w\), its window is the interval \([i,\; i + \operatorname {win}_i(w))\), the in-order range of the subtree rooted at the \(\mathrm{Node}\) for position \(i\) in \(M(w)\).

Definition 2.5 Window size

\(\operatorname {win}_i(w)\) is defined by fuel-based recursion that descends \(M(w)\) via \(\texttt{mm\_ pos}\): at the root position one returns \(|w| - i\); otherwise one recurses into the left or right subtree according to whether \(i\) lies before or after the root.

Definition 2.6 Internal vertex

Position \(i\) is internal in \(w\) iff \(i {\lt} |w|\) and \(\operatorname {win}_i(w) {\gt} 1\). Equivalently, the \(\mathrm{Node}\) for position \(i\) in \(M(w)\) has at least one non-\(\mathrm{Leaf}\) child.

Definition 2.7 Has left child

\(\operatorname {hlc}_i(w)\) is true iff in \(M(w)\) the \(\mathrm{Node}\) at position \(i\) has a non-\(\mathrm{Leaf}\) left subtree. This is Stanley’s \(\operatorname {hlc}\) predicate from p. 57 (it distinguishes the cd-letters c and d; see Chapter 3).

Definition 2.8 Internal vertices of \(w\)

\(\texttt{internal\_ vertices}(w)\) is the strictly increasing sequence of positions \(i\) for which \(\operatorname {int}_i(w)\) holds.