2.3 The operators \(\psi _{i}\)
For each internal position \(i\), \(\psi _{i}\) is a permutation on sequences that toggles the local order of the window at \(i\) without changing the unlabelled tree shape. This is Stanley’s \(\psi _i\) from EC1 §1.6.3, p. 57.
For an internal position \(i\) of \(w\), \(\psi _{i}(w)\) is defined by a rank-shift inside the window at \(i\) (the precise formula is given in psi_core.v:219). For non-internal \(i\), \(\psi _{i}\) acts as the identity.
For every \(i \in \mathbb {N}\) and every uniq sequence \(w\), \(\psi _{i}(\psi _{i}(w)) = w\).
For all \(i, j \in \mathbb {N}\) and every uniq sequence \(w\), \(\psi _{i}(\psi _{j}(w)) = \psi _{j}(\psi _{i}(w))\). This is the commutativity half of Stanley’s Fact #1 (EC1 p. 57): the \(\psi _{i}\) for internal vertices generate an abelian group \(G_w \cong (\mathbb {Z}/2)^{\iota (w)}\), where \(\iota (w)\) is the number of internal vertices.
For a sequence \(\mathrm{ss}\) of internal positions, \(\texttt{apply\_ psis}(\mathrm{ss})(w)\) is the left-fold composition of the corresponding \(\psi _{i}\). By Theorem 2.11 and Theorem 2.10, the result depends only on the set \(\mathrm{ss} \subseteq \texttt{internal\_ vertices}(w)\), and the M-equivalence class \([w] = \{ \texttt{apply\_ psis}(\mathrm{ss})(w) : \mathrm{ss} \subseteq \texttt{internal\_ vertices}(w)\} \) has size \(2^{\iota (w)}\).
For every \(\mathrm{ss}\), every position \(i\), and every uniq \(w\): \(\operatorname {win}_i(\texttt{apply\_ psis}(\mathrm{ss})(w)) = \operatorname {win}_i(w)\), \(\operatorname {hlc}_i(\texttt{apply\_ psis}(\mathrm{ss})(w)) = \operatorname {hlc}_i(w)\), \(\operatorname {int}_i(\texttt{apply\_ psis}(\mathrm{ss})(w)) = \operatorname {int}_i(w)\), and the lists of internal vertices coincide.
These four invariances express that \(\Psi \)-action permutes labels inside windows but preserves the unlabelled tree shape — the load-bearing geometric fact behind Stanley Fact #1’s well-definedness clause for \(\Phi _{w}\) (Chapter 3).