OP-00110 Lean verified

The Rowland–Wu polynomial identity for Sinkhorn limits

Let $m, n \ge 1$ and let $A = (a_{ij}) \in \mathbb{R}^{m \times n}$ have positive entries. Its Sinkhorn limit $\operatorname{Sink}(A)$ is the unique matrix $D_1 A D_2$, with $D_1, D_2$ positive diagonal, whose row sums are $1$ and column sums $m/n$; let $x = \operatorname{Sink}(A)_{11}$. Let $$\mathcal D = \{(R, C) : R \subseteq \{2, \dots, m\},\ C \subseteq \{2, \dots, n\},\ |R| = |C|\},$$ and for $(R, C) \in \mathcal D$ let $\Delta(R, C) = \det A_{\{1\} \cup R, \{1\} \cup C}$ and $\Gamma(R, C) = a_{11} \det A_{R, C}$, with the rows and columns of submatrices in increasing order; empty determinants and products are $1$. For $\mathcal S \subseteq \mathcal D$ let $$M(\mathcal S) = \prod_{(R,C) \in \mathcal S} \Delta(R, C) \prod_{(R,C) \in \mathcal D \setminus \mathcal S} \Gamma(R, C).$$ For a finite set $U$ of integers and $s \in U$, let $p_s(U)$ be the position of $s$ in the increasing list of $U$, counting from $1$. For $\mathcal S = \{(R_1, C_1), \dots, (R_k, C_k)\} \subseteq \mathcal D$, let $H_{\mathcal S} \in \mathbb{Z}^{k \times k}$ have diagonal entries $(H_{\mathcal S})_{ii} = |R_i|(m+n) - mn$ and, for $i \ne j$, with $\tau_{ij} = (R_i \setminus R_j,\ R_j \setminus R_i,\ C_i \setminus C_j,\ C_j \setminus C_i)$, $$(H_{\mathcal S})_{ij} = \begin{cases} (-1)^{p_s(R_j) + p_t(C_j)}\, m, & \tau_{ij} = (\varnothing, \{s\}, \varnothing, \{t\}),\\ (-1)^{p_s(R_i) + p_t(C_i) + 1}\, n, & \tau_{ij} = (\{s\}, \varnothing, \{t\}, \varnothing),\\ (-1)^{p_s(C_i) + p_t(C_j)}\, m, & \tau_{ij} = (\varnothing, \varnothing, \{s\}, \{t\}),\\ (-1)^{p_s(R_i) + p_t(R_j)}\, n, & \tau_{ij} = (\{s\}, \{t\}, \varnothing, \varnothing),\\ 0, & \text{otherwise}. \end{cases}$$ The determinant of $H_{\mathcal S}$ does not depend on the order chosen for $\mathcal S$. Rowland and Wu found the identity below by computer experiments, and proved a polynomial equation of degree at most $6$ for $x$ when $m = n = 3$. The identity would make $x$ algebraic over the field generated by the entries of $A$, of degree at most $\binom{m+n-2}{m-1}$; Fang proved this degree bound.

Problem. Is $$\sum_{\mathcal S \subseteq \mathcal D} \det\!\left(m^{-1} H_{\mathcal S}\right) M(\mathcal S)\, x^{|\mathcal S|} = 0$$ for all $m, n \ge 1$ and every $A \in \mathbb{R}^{m \times n}$ with positive entries?

Source: Rowland and Wu (2025), Conjecture 2, in the second version of arXiv:2409.02789; the first version (2024) did not yet determine the signs.

Imported from github.com/ajt60gaibb/OpenProblemsInNLA.

Classification

Primary: NA — Numerical Analysis
Secondary: AC, CO
Keywords: matrix scaling, OpenProblemsInNLA, Sinkhorn limits

References

@misc{rowland2025,
  author        = {Rowland, Eric and Wu, Jason},
  title         = {The entries of the {S}inkhorn limit of an $m \times n$ matrix},
  year          = {2025},
  eprint        = {2409.02789},
  archivePrefix = {arXiv},
  note          = {Version 2, 25 May 2025},
}
@misc{fang2025,
  author        = {Fang, Max Chicky},
  title         = {Closed Form of a Generalized {S}inkhorn Limit},
  year          = {2025},
  eprint        = {2506.06338},
  archivePrefix = {arXiv},
}
@misc{openproblemsinnla-nm04,
  author       = {Townsend, Alex},
  title        = {{NM-04}: The Rowland–Wu polynomial identity for Sinkhorn limits},
  howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
  year         = {2026},
  url          = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/nonnegative-and-positive-factorizations/NM-04/README.md},
  note         = {Read at commit e375a6f, 2026-09-30},
}

Canonical Lean statement

A submission resolves this problem by proving the constant Problem_OP_00110.

namespace RegistryProblems.OP_00110
noncomputable section

open scoped BigOperators Matrix

/-- Stands in for the source's `attribute [local instance] Classical.propDecidable`, which
registers the classical decision procedure at default priority: the same instance, at the
same priority, so the definitions below elaborate with the same decidability instances. -/
noncomputable local instance (priority := default) propDecidableDefault (a : Prop) : Decidable a :=
  Classical.propDecidable a

universe u v w
variable {α : Type u} {β : Type v} {𝕜 : Type w}

/-- A pair of actual finite subsets with equal cardinalities. -/
abbrev MinorIndex (α : Type u) (β : Type v) :=
  {RC : Finset α × Finset β // RC.1.card = RC.2.card}

/-- One-based position in the increasing order. Only member positions enter signs. -/
def position [LinearOrder α] (s : α) (U : Finset α) : ℕ :=
  (U.filter (fun t => t < s)).card + 1

/-- The two maps enumerate the selected rows and columns in increasing order. -/
def minorMatrix [LinearOrder α] [LinearOrder β]
    (T : Matrix α β 𝕜) (I : MinorIndex α β) :
    Matrix (Fin I.1.1.card) (Fin I.1.1.card) 𝕜 :=
  fun i j => T (I.1.1.orderEmbOfFin rfl i)
    (I.1.2.orderEmbOfFin I.property.symm j)

def minor [LinearOrder α] [LinearOrder β] [CommRing 𝕜]
    (T : Matrix α β 𝕜) (I : MinorIndex α β) : 𝕜 :=
  (minorMatrix T I).det

/-- Literal singleton supports from the canonical four off-diagonal cases. -/
def RaisingSupport [DecidableEq α] [DecidableEq β]
    (I J : MinorIndex α β) (s : α) (t : β) : Prop :=
  I.1.1 \ J.1.1 = ∅ ∧ J.1.1 \ I.1.1 = {s} ∧
  I.1.2 \ J.1.2 = ∅ ∧ J.1.2 \ I.1.2 = {t}

def LoweringSupport [DecidableEq α] [DecidableEq β]
    (I J : MinorIndex α β) (s : α) (t : β) : Prop :=
  I.1.1 \ J.1.1 = {s} ∧ J.1.1 \ I.1.1 = ∅ ∧
  I.1.2 \ J.1.2 = {t} ∧ J.1.2 \ I.1.2 = ∅

def ColumnExchangeSupport [DecidableEq α] [DecidableEq β]
    (I J : MinorIndex α β) (s t : β) : Prop :=
  I.1.1 \ J.1.1 = ∅ ∧ J.1.1 \ I.1.1 = ∅ ∧
  I.1.2 \ J.1.2 = {s} ∧ J.1.2 \ I.1.2 = {t}

def RowExchangeSupport [DecidableEq α] [DecidableEq β]
    (I J : MinorIndex α β) (s t : α) : Prop :=
  I.1.1 \ J.1.1 = {s} ∧ J.1.1 \ I.1.1 = {t} ∧
  I.1.2 \ J.1.2 = ∅ ∧ J.1.2 \ I.1.2 = ∅

def raisingCoefficient [Fintype α] [Fintype β] [LinearOrder α] [LinearOrder β]
    (I J : MinorIndex α β) : ℤ :=
  ∑ s : α, ∑ t : β, if RaisingSupport I J s t then
    (-1) ^ (position s J.1.1 + position t J.1.2) else 0

def loweringCoefficient [Fintype α] [Fintype β] [LinearOrder α] [LinearOrder β]
    (I J : MinorIndex α β) : ℤ :=
  ∑ s : α, ∑ t : β, if LoweringSupport I J s t then
    (-1) ^ (position s I.1.1 + position t I.1.2) else 0

def columnExchangeCoefficient [Fintype β] [DecidableEq α] [LinearOrder β]
    (I J : MinorIndex α β) : ℤ :=
  ∑ s : β, ∑ t : β, if ColumnExchangeSupport I J s t then
    (-1) ^ (position s I.1.2 + position t J.1.2) else 0

def rowExchangeCoefficient [Fintype α] [LinearOrder α] [DecidableEq β]
    (I J : MinorIndex α β) : ℤ :=
  ∑ s : α, ∑ t : α, if RowExchangeSupport I J s t then
    (-1) ^ (position s I.1.1 + position t J.1.1) else 0

abbrev Rect (m n : ℕ) := Matrix (Fin m) (Fin n) ℝ

/-- Original labels 2,...,m, stored as their zero-based `Fin m` indices. -/
abbrev Tail (m : ℕ) := {i : Fin m // 0 < i.val}
abbrev Index (m n : ℕ) := MinorIndex (Tail m) (Tail n)

def firstIndex {m : ℕ} (hm : 1 ≤ m) : Fin m := ⟨0, hm⟩

def tailMatrix {m n : ℕ} (A : Rect m n) : Matrix (Tail m) (Tail n) ℝ :=
  fun i j => A i.val j.val

/-- First index followed by increasing tail indices is the source's increasing order. -/
def delta {m n : ℕ} (A : Rect m n) (hm : 1 ≤ m) (hn : 1 ≤ n)
    (I : Index m n) : ℝ :=
  Matrix.det (A.submatrix
    (Fin.cons (firstIndex hm) (fun i => (I.1.1.orderEmbOfFin rfl i).val))
    (Fin.cons (firstIndex hn) (fun j => (I.1.2.orderEmbOfFin I.property.symm j).val)))

def gamma {m n : ℕ} (A : Rect m n) (hm : 1 ≤ m) (hn : 1 ≤ n)
    (I : Index m n) : ℝ :=
  A (firstIndex hm) (firstIndex hn) * minor (tailMatrix A) I

/-- Integer arithmetic, including the negative diagonal and lowering coefficient. -/
def H (m n : ℕ) : Matrix (Index m n) (Index m n) ℤ :=
  fun I J => if I = J then
    (I.1.1.card : ℤ) * ((m : ℤ) + (n : ℤ)) - (m : ℤ) * (n : ℤ)
  else (m : ℤ) * raisingCoefficient I J - (n : ℤ) * loweringCoefficient I J +
    (m : ℤ) * columnExchangeCoefficient I J + (n : ℤ) * rowExchangeCoefficient I J

def HReal (m n : ℕ) : Matrix (Index m n) (Index m n) ℝ :=
  fun I J => (H m n I J : ℝ)

def Positive {m n : ℕ} (A : Rect m n) : Prop := ∀ i j, 0 < A i j

def Balanced {m n : ℕ} (S : Rect m n) : Prop :=
  (∀ i, ∑ j, S i j = 1) ∧ (∀ j, ∑ i, S i j = (m : ℝ) / (n : ℝ))

/-- Entrywise form of multiplication by the actual two diagonal matrices. -/
def diagonalScale {m n : ℕ} (A : Rect m n) (a : Fin m → ℝ)
    (b : Fin n → ℝ) : Rect m n := fun i j => a i * A i j * b j

def ScaledBalanced {m n : ℕ} (A S : Rect m n) : Prop :=
  ∃ (a : Fin m → ℝ) (b : Fin n → ℝ),
    (∀ i, 0 < a i) ∧ (∀ j, 0 < b j) ∧ S = diagonalScale A a b ∧ Balanced S

/-- Total choice only. Existence, uniqueness and exclusion of the fallback on
    positive inputs are separate contracts and are not assumptions of this definition. -/
def sinkhorn {m n : ℕ} (A : Rect m n) : Rect m n :=
  if h : ∃ S, ScaledBalanced A S then Classical.choose h else 0

/-- OP-00110: The Rowland–Wu polynomial identity for Sinkhorn limits -/
def _root_.RegistryProblems.Problem_OP_00110 : Prop :=
  ∀ {m n : ℕ} (hm : 1 ≤ m) (hn : 1 ≤ n) (A : Rect m n), Positive A →
    (∑ E : Finset (Index m n),
      ((m : ℝ)⁻¹ • (HReal m n).submatrix
        (Subtype.val : E → Index m n) (Subtype.val : E → Index m n)).det *
      (∏ I ∈ E, delta A hm hn I) * (∏ I ∈ (Finset.univ \ E), gamma A hm hn I) *
      ((sinkhorn A) (firstIndex hm) (firstIndex hn)) ^ E.card) = 0

end
end RegistryProblems.OP_00110

Formalised by George Stepaniants (Apache-2.0); reviewed by clemens-admin.

Available to match against in: Lean v4.33.1 with Mathlib v4.33.1.

Resolving this problem in Lean

Add the problems package as a dependency, import this problem's module, and prove the constant. Any published revision works.

In lakefile.toml:

[[require]]
name = "RegistryProblems"
git = "https://github.com/cthalhammer/registry-problems"
rev = "753bebc58e3fee845f4fffec7d24e7c8cc2a689a"

In your proof:

import RegistryProblems.OP_00110

theorem resolution : RegistryProblems.Problem_OP_00110 := by
  sorry

In preprint.toml, mapping the claim to the declaration that establishes it:

[[statements]]
label = "Theorem 1"
lean = "resolution"
latex = "..."
problem = "OP-00110"
claim = "full"

To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:

theorem disproof : ¬ RegistryProblems.Problem_OP_00110 := by
  sorry

You can also write the statement out in full; the verifier checks it matches up to definitional equality. Partial results and reductions are not matched against this statement.

Resolution claims

NM-04: the complete Rowland–Wu polynomial identity for rectangular Sinkhorn scaling v1 GitHub ↗

George Stepaniants

Complete Lean verification of the original Rowland-Wu coefficient identity for every strictly positive real rectangular matrix, including positive scaling existence and uniqueness, empty and singular minors, and all transition signs.

Full resolution · verified · canonical statement matched · posted on GitHub 17 Sep 2026

A null vector for the Rowland–Wu determinant identity v1 GitHub ↗

Matthew J. Colbrook

We prove the Rowland–Wu polynomial identity for every positive rectangular matrix. The principal-minor coefficient sum is a single determinant. For a matrix already scaled to row sums one and column sums $m/n$, that determinant has an explicit null vector whose coordinate on a minor of order $k$ is $(n/m)^k$. The proof is an elementary identity among minors of a Schur …

Full resolution · not verified · fidelity not established · posted on GitHub 11 Sep 2026

Status history

When	Change	By	Reason
2026-10-05	Needs verification → Lean verified	—	Verified here: OpenProblemsInNLA @ e375a6f, NM-04/lean/.

Citing this problem

This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.

OP-00110, "The Rowland–Wu polynomial identity for Sinkhorn limits", clopen.solutions.