Product of local stabilizer traces for prescribed block types

This is the local stabilizer trace estimate of the signed sweep moment induction, in product form over the blocks of a rectangle.

Throughout, $S_p$ acts on the word space $W_p=\ell^2\big((C\sqcup C)^p\big)$, with $C=\{1,\dots,q\}$ two-coloured into even and odd letters, 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 $g$ induces between the odd positions of $w$. For $u+v=p$ and partitions $\alpha\vdash u$, $\beta\vdash v$, the operator $P_{\alpha,\beta}$ is the sum, over the placements of $u$ even sites among the $p$ sites, of the tensor product of the orthogonal projections onto the $S^\alpha$-isotypic part of the $u$ even sites and the $S^\beta$-isotypic part of the $v$ odd sites. Its entropy is $F(\alpha,\beta)=\sum_{a\in\alpha\cup\beta}a\log\frac{u+v}{a}$, and a local type on $k$ sites is such a pair of total size $k$. For an enumeration $e$ of the $p$ sites by blocks $j\in J$ with $k_j$ sites each and local types $t=(t_j)_j$, $P^{e}_{t}$ is the corresponding tensor product of local type projections, with $F(t)=\sum_jF(t_j)$. For a coefficient function $f:G\to\mathbb{C}$ on a finite group and a representation $\pi$, $\pi(f)=\sum_gf(g)\pi(g)$.

Let $J$ be a finite index set, let $k_j\le t$ for $j\in J$, let $e$ enumerate $p=\sum_jk_j$ sites by the blocks, and fix local types $a_j$ on $k_j$ sites and injections $i_j:\{1,\dots,k_j\}\hookrightarrow\{1,\dots,t\}$. Let $f_j:S_t\to\mathbb{C}$ act as a positive operator in the regular representation, let $\eta,G_j\in\mathbb{R}$, and let $R\ge 2t+2q+1$. Assume that for every $j$ with $a_j$ of height at most $q$, for all $\lambda\vdash t$ and all partitions $c$ of $t-k_j$ such that $\lambda$ contains the signed occurrence of $(a_j,c)$,

Write $\tilde f$ for the coefficient on $S_p$ obtained by pushing the product of the restrictions $g\mapsto f_j(g^{i_j})$ along the block embedding $\prod_jS_{k_j}\to S_p$, where $g^{i_j}$ acts as $g$ on the image of $i_j$ and fixes the other points. Then

where $E_{\mathrm{loc}}(t,q,R)=\big(2\lfloor\sqrt t\rfloor+26q^2+8q+1\big)\log R+8q+1$.

This reduces traces on the occupied part of a rectangle to the inductive moment bound on each line, with the exact pointwise-stabilizer index retained.

Formalization Note The hypothesis is stated only for types of height at most $q$, and the bound also covers types of larger height. The upstream statement is reproduced verbatim from OccupiedTrace.lean.