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

2 Min-max trees and the \(\psi _{i}\) operators

This chapter formalizes Stanley EC1 §1.6.3, pp. 56–57: the min-max tree construction \(M(w)\), its window structure, and the involutive operators \(\psi _{i}\) that generate the \(M\)-equivalence class \([w]\) on which the cd-monomial \(\Phi _{w}\) will be defined (Chapter 3).