Corner ranks determine the lower–lower Bruhat permutation

Let $K$ be a field and let $A=E_1\,\Pi\,E_2$ be an $m\times m$ matrix, where $E_1,E_2$ are lower triangular with nonzero diagonal and $\Pi$ is a partial permutation matrix ($0/1$ entries, at most one $1$ in each row and column). Then for all indices $i,j$,

where $A[\,0..i,\ j..m-1\,]$ is the submatrix of rows $\le i$ and columns $\ge j$.

So the partial permutation of a lower–lower Bruhat factorization (which exists by IntMul.OpenAI.lower_triangular_factorization) is determined by $A$ alone, through these northeast-corner ranks. The batched-recursion arguments for the $\kappa$-saving networks, such as the partial-swap batching lemma, the flag basis and the reversed-run (opposite bank order) compile of Jain's rounds, read off the recursive interchange calls of an edge from this Bruhat profile: a pivot $(a,b)$ is one interchange of the fields $H_a,D_b$, and an order-preserving run of pivots is one batched call.

Formalization Note Rows $\le i$ and columns $\ge j$ are indexed by the subtypes {r // r ≤ i} and {c // j ≤ c} of Fin m.