Counterexamples to the Kronecker-square lower bound for nonnegative rank

Dev D. Goyal

Counterexamples to the Kronecker-square lower bound for nonnegative rank

Dev D. Goyal · 2026 · Research preprint, not externally peer reviewed

Selected result in this collection

Problem and result

Problem: Vandaele–Gillis–Glineur–Tuyttens conjecture rank₊(M ⊗ M) ≥ rank₊(M) rank(M)
Posed in: Vandaele, Gillis, Glineur and Tuyttens, 'Heuristics for exact nonnegative matrix factorization', J. Global Optim. 65 (2016), 369–400, Conjecture 1 (Section 6.1)
Status: Disproved
Result: For every k ≥ 0 an explicit rational nonnegative matrix C of order k + 11, rank k + 10 and nonnegative rank k + 11 has rank₊(C ⊗ C) ≤ (k + 10)² + 9, at least k + 1 below the conjectured bound rank₊(C) rank(C).

Abstract

Vandaele, Gillis, Glineur and Tuyttens conjectured in 2016 that every nonnegative matrix M satisfies rank₊(M ⊗ M) ≥ rank₊(M) rank(M). For every k ≥ 0 an explicit rational nonnegative matrix C of order k + 11, rank k + 10 and nonnegative rank k + 11 has rank₊(C ⊗ C) ≤ (k + 10)² + 9, so the conjecture fails by at least k + 1. The matrix is the direct sum of a classical 4 × 4 matrix of rank three and nonnegative rank four with a small diagonal perturbation of an all-ones matrix; in the mixed Kronecker blocks a positive rank-one term absorbs a small real perturbation of rank q with only q + 1 nonnegative terms. At k = 0 an exact rational factorization of width 109 beats the conjectured bound 110.

Details

Year: 2026
Discipline: Mathematics
Area: Matrix theory
Subject: Matrix theory
Result type: Counterexample to a published conjecture and reproducible proof package
Formal proof: Standalone Lean package
Family: nonnegative-rank-kronecker
Keywords: nonnegative rank, nonnegative matrix factorization, exact NMF, Kronecker product, tensor product, Vandaele–Gillis–Glineur–Tuyttens conjecture

Statement and scope

Formal scope. The whole family is formalized in Lean, with nonnegative rank minimized over all real nonnegative factorizations, together with a literal negation of the conjecture over all finite rectangular nonnegative real matrices. The width-109 factorization of the order-11 witness is also checked in exact rational arithmetic. The exact nonnegative rank of the squares is not determined.

A Lean check establishes only the formal statement that is checked. It does not establish novelty, historical priority or a faithful transcription of an external source. Known gaps are listed in UNFINISHED.md; the authorship disclosure describes how the results were produced.

Manuscript

PDF on this site: manuscript.pdf 296 KB
PDF on GitHub: papers/mathematics/nonnegative-rank-kronecker/manuscript.pdf
LaTeX source: papers/mathematics/nonnegative-rank-kronecker/manuscript.tex

Formal proof

This result has a standalone Lean 4 package, separate from the shared library. Build it with the toolchain and instructions given in its README.

Proof package

papers/mathematics/nonnegative-rank-kronecker/

Lean project

papers/mathematics/nonnegative-rank-kronecker/lean/ 15 Lean files

Lakefile

papers/mathematics/nonnegative-rank-kronecker/lean/lakefile.toml

Toolchain

leanprover/lean4:v4.35.0-rc3

Library roots

Reproduce

The commands below are quoted from papers/mathematics/nonnegative-rank-kronecker/VERIFICATION.md, which gives their context and working directory.

Exact certificate

python3 certificate/exact_certificate.py --verify-only certificate/C11_NMF109.json
python3 certificate/check_factorization.py certificate/C11_NMF109.json

Lean

lake exe cache get
bash verify.sh

README: papers/mathematics/nonnegative-rank-kronecker/README.md
Verification guide: papers/mathematics/nonnegative-rank-kronecker/verification/README.md
Verification record: papers/mathematics/nonnegative-rank-kronecker/VERIFICATION.md
Authorship: papers/mathematics/nonnegative-rank-kronecker/AUTHORSHIP.md
Repository guide: verification/README.md
Unfinished proofs: UNFINISHED.md

Source and prior work

Prior work. Vandaele, Gillis, Glineur and Tuyttens, 2016.

Source. Vandaele, Gillis, Glineur and Tuyttens (J. Global Optim. 2016, Conjecture 1) proposed the bound; Chauhan and Choudhury (arXiv 2026) proved it for matrices with at most three rows or columns. The seed matrix is classical (Vandaele et al.; Bocci, Carlini and Rapallo) and direct-sum additivity is due to Qi, Comon and Lim. Historical priority is not certified.

Questions and answers

Is the bound rank₊(M ⊗ M) ≥ rank₊(M) rank(M) true for every nonnegative matrix?

No. For every k ≥ 0 this preprint gives a rational nonnegative matrix C of order k + 11 with rank k + 10 and nonnegative rank k + 11 for which rank₊(C ⊗ C) ≤ (k + 10)² + 9, so the conjectured bound fails by at least k + 1; at k = 0 an exact width-109 factorization beats the conjectured 110.

What remains open?

The exact nonnegative rank of the squares is not determined, nor is the least order of a counterexample. The witnesses are direct sums, so irreducible, symmetric or strictly positive counterexamples are not addressed; Chauhan and Choudhury (2026) proved the bound for matrices with at most three rows or columns.

Is the counterexample formally verified?

The whole family and a literal negation of the conjecture over all finite rectangular nonnegative real matrices are formalized in Lean 4, with nonnegative rank minimized over all real nonnegative factorizations; the width-109 factorization is also checked in exact rational arithmetic. Historical priority is not certified, and the paper is an unrefereed preprint.

Cite

Citation file papers/mathematics/nonnegative-rank-kronecker/CITATION.bib. For the whole collection, use CITATION.cff or CITATION.bib.

@misc{goyal2026nonnegativerankkronecker,
  author = {Goyal, Dev D.},
  title = {Counterexamples to the Kronecker-Square Lower Bound for Nonnegative Rank},
  year = {2026},
  month = oct,
  note = {Preprint. Fully autonomous agentic research; publication responsibility: Dev D. Goyal},
  url = {https://github.com/dvgyl/math-and-theory/tree/main/papers/mathematics/nonnegative-rank-kronecker}
}