A signed occurrence bounds traces in irreducibles by traces on marked words

An occurrence of a signed tensor product in a Specht module bounds its traces by traces on the typed space of marked words.

Let $C$ be a finite set and $W_p=\ell^2\big((C\sqcup C)^p\big)$, on which $S_p$ acts by the signed action $(\rho(g)f)(w)=\varepsilon(g,w)f(w\circ g)$, where $\varepsilon(g,w)$ is the sign of the permutation induced between the odd positions of $w$. For $u+v=p$, $\alpha\vdash u$, $\beta\vdash v$, the type projection $P_{\alpha,\beta}$ is the sum, over placements of $u$ even sites among the $p$ sites, of the tensor product of the projections onto the $S^\alpha$-isotypic part on the even sites and the $S^\beta$-isotypic part on the odd sites.

Let $p+l=n$ and let $M_{p,l,n}$ be the orthogonal sum, over injections of $l$ distinct marks into $n$ positions, of word spaces on the $p$ unmarked positions, with the action of $S_n$ moving marks and transporting the words, and let $P$ be the corresponding global projection of type $(a,b)$, for $a\vdash u$, $b\vdash v$, $u+v=p$. Let $c\vdash l$ and $\lambda\vdash n$, and assume that $a$ and $b$ have row counts embedded in $C$ and that $S^a\otimes S^{b^t}\otimes S^c$ occurs in $S^\lambda$ as a signed occurrence. Then for coefficients $f,k:S_n\to\mathbb{C}$ acting positively in the regular representation,

This passes from an irreducible trace to a trace that splits over mark assignments, which is the entry point of the moment induction.

Formalization Note The statement takes an assignment $z$ and an allocation $S$ as witnesses that the sector is nonempty. It is reproduced verbatim from MarkedTrace.lean.