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.