A 0/1 matrix is determined by its corner counts

Proved

IntMul.OpenAI.partial_perm_eq_of_corner_counts

by xuanji · Oct 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsinteger-multiplication

Let $P,P'$ be $n\times n$ matrices with entries in $\{0,1\}$ . Suppose that for all $X,Y\in\mathbb N$ they have the same number of entries equal to $1$ in the northeast corner of rows $<X$ and columns $\ge Y$ :

\#\{(a,b):a<X,\ b\ge Y,\ P_{ab}=1\}=\#\{(a,b):a<X,\ b\ge Y,\ P'_{ab}=1\}.

Then $P=P'$ .

Each entry is recovered from four corner counts by inclusion–exclusion,

[P_{ij}=1]=c(i{+}1,j)-c(i,j)-c(i{+}1,j{+}1)+c(i,j{+}1).

Together with IntMul.OpenAI.bruhat_rank_profile, this shows that the partial permutation of a lower–lower Bruhat factorization $A=E_1\Pi E_2$ is unique. So the number and the widths of the recursive interchange calls compiled from an edge matrix are intrinsic to the matrix; this is used by every batching argument for the $\kappa$ -saving networks.

Formalization Note The entry type only needs 0, 1 and decidable equality.

Preamble

import Mathlib
open Finset

Formal statement

namespace IntMul.OpenAI

theorem partial_perm_eq_of_corner_counts {n : ℕ} {K : Type*} [Zero K] [One K] [DecidableEq K]
    (P P' : Matrix (Fin n) (Fin n) K)
    (h01 : ∀ i j, P i j = 0 ∨ P i j = 1) (h01' : ∀ i j, P' i j = 0 ∨ P' i j = 1)
    (h : ∀ X Y : ℕ,
      (univ.filter fun x : Fin n × Fin n => x.1.val < X ∧ Y ≤ x.2.val ∧ P x.1 x.2 = 1).card =
      (univ.filter fun x : Fin n × Fin n => x.1.val < X ∧ Y ≤ x.2.val ∧ P' x.1 x.2 = 1).card) :
    P = P' := by sorry

end IntMul.OpenAI

Source

OpenAI, Integer multiplication below n log n (preprint, 23 Sep 2026), Section 4.1 (Bruhat factorization); uniqueness of the Bruhat permutation via rank conditions, used in S. Jain, integer-mult-kappa notes/partial-swap-batching.tex

View graph