3.4 Stanley Fact #3
Stanley’s statement (verbatim, p. 58):
Let \(w \in \mathfrak {S}_n\), and let \([w]\) be the M-equivalence class containing \(w\). Then \(\sum _{v \in [w]} u_{D(v)} = \Phi _{w}(a + b,\; ab + ba)\).
Our formalization, with multisets represented as sorted seqs:
Stanley uses Fact #3 as a stepping stone to Theorem 1.6.3 (the ab-index of \(\mathfrak {S}_n\) factors through the cd-substitution); our \(\texttt{fact3}\) matches this directly.
The right-hand side is enumerated by Stanley’s bit-string expansion (3.5), and the left-hand side is enumerated by ranging over subsets of \(\texttt{internal\_ vertices}(w)\). Both have size \(2^{\iota (w)}\) where \(\iota (w)\) is the number of internal vertices.
The map \(\mathrm{ss} \mapsto u_{\texttt{apply\_ psis}(\mathrm{ss})(w)}\) is shown to be injective via a bit-level recovery argument (in ): for each internal vertex \(v\), one can read off \((v \in \mathrm{ss})\) from the bits of \(u_{\texttt{apply\_ psis}(\mathrm{ss})(w)}\) at positions owned by \(v\). Disjointness of the bit-positions across distinct internal vertices follows from (D-vertex predecessors are non-internal). Equality of the two multisets then follows from injectivity plus equal cardinality.