Corner ranks of a partial-swap frame

Let $K$ be a field and $p$ an $m\times m$ idempotent matrix ($p^2=p$), and put $q=1-p$. The partial swap frame on paired fields $(H,D)$ is the $2m\times 2m$ matrix

with rows and columns ordered $H_0,\dots,H_{m-1},D_0,\dots,D_{m-1}$. For $X,Y\in\mathbb N$ write $p[{<}X,{\ge}Y]$ for the block of rows $<X$ and columns $\ge Y$. The northeast corners of $S_p$ have the following ranks:

• (B) rows $H_{<X}$, columns $H_{\ge Y}\cup D$: $\ \#[Y,X)+\operatorname{rank}p[{<}\min(X,Y),\,\cdot\,]$;
• (C) rows $H\cup D_{<X}$, columns $D_{\ge Y}$: $\ \#[Y,X)+\operatorname{rank}p[\,\cdot\,,{\ge}\max(X,Y)]$;
• (D) rows $H\cup D_{<X}$, columns $H_{\ge Y}\cup D$: $\ \#\{c\ge Y\}+\min(X,m)+\operatorname{rank}p[{<}Y,{\ge}X]$.

The remaining corners (rows in $H$, columns in $D$) are blocks of $p$ itself. Combined with IntMul.OpenAI.bruhat_rank_profile and IntMul.OpenAI.partial_perm_eq_of_corner_counts, these formulas show that the lower–lower Bruhat involution of $S_p$ can be read off from the Bruhat pivots of $p$: it swaps $H_i\leftrightarrow D_j$ for every pivot $(i,j)$ of $p$ and fixes all other coordinates. This is the "runs" principle of Jain's flag-basis and partial-swap batching notes: a frame change $S_p$ on an edge of the two-stage bit interchange costs exactly $\operatorname{rank}p$ field transpositions, grouped into runs that follow the pivots of $p$.

Formalization Note The blocks are written with Matrix.of on sum and subtype index types; $\#[Y,X)$ counts $c\in$ Fin m with $Y\le c<X$.