Trace bound for fixed marks in a signed sweep step

This is the bound at a fixed assignment of marks in one step of the signed sweep moment induction.

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 $n=2^{a+b}$, identified with the rectangle $2^a\times2^b$ through the binary coordinates, let $p+l=n$, let $z$ be an injection of $l$ marks into the $n$ positions and $\iota$ an enumeration of the other $p$ positions, and let $0\le\eta\le1$, $\tau\in\mathbb{R}$, $q>0$, $j\in\mathbb{N}$, $R\ge2\max(2^a,2^b)+2q+1$. Write $J_r(\lambda)=\dim S^\lambda\operatorname{Re}\operatorname{Tr}_{S^\lambda}\big((T^*T)^r\big)$ for the weighted moment of the $d$-coordinate sweep $T$, and

Assume that for $d\in\{a,b\}$ and every signed occurrence of $(\alpha,\beta,\gamma)$ in $\lambda\vdash2^d$ one has $J_{2^j}(\lambda)\le\exp(\eta F(\alpha,\beta)+g_\tau(2^d,|\gamma|))$. Let $c,c'$ be the coefficients on $S_{2^{a+b}}$ of the $2^j$-th powers of the positive squares of the products of column sweeps and of row sweeps, and let $c_z,c'_z$ be their restrictions to $S_p$ along $\iota$. Then for $u+v=p$, $\alpha\vdash u$, $\beta\vdash v$ with at most $q$ rows,

Here, with $h_j$ marks in column $j$ and $b_i$ marks in row $i$, $\Phi(z)=\prod_j(2^a)_{h_j}^{-1}\prod_i(2^b)_{b_i}^{-1}$ is the product of inverse falling factorials, $\Gamma_\tau(z)=\sum_jg_\tau(2^a,h_j)+\sum_ig_\tau(2^b,b_i)$, and

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

The bound is what remains to be summed over mark assignments in the induction step.

Formalization Note The upstream statement is reproduced verbatim from OccupiedSweep.lean; columns are indexed by $2^b$ and rows by $2^a$ through sweepBoard.