The nonnegative rank of the nine-point distance matrix
Let $D \in \mathbb{R}^{9 \times 9}$ have entries $D_{ij} = (i - j)^2$ for $1 \le i, j \le 9$, and let $\operatorname{rank}_+$ be the nonnegative rank over $\mathbb{R}$. The matrix $D$ has rank $3$; Gillis and Glineur's lower bound gives $\operatorname{rank}_+(D) \ge 6$, and an inequality of Hrubeš gives $\operatorname{rank}_+(D) \le 7$ (Baeckelant, Vandaele and Gillis).
Problem. Does there exist an exact factorization $D = WH$ with $W \in \mathbb{R}_{\ge 0}^{9 \times 6}$ and $H \in \mathbb{R}_{\ge 0}^{6 \times 9}$? Equivalently, is $\operatorname{rank}_+(D) = 6$ rather than $7$?
Source: Stated by OpenProblemsInNLA, after Baeckelant, Vandaele and Gillis (2026), Appendix A.1; the bounds 6 and 7 are Gillis and Glineur's (2012) and Hrubeš's (2012).
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- OC
- Keywords
- Euclidean distance matrices, nonnegative rank, OpenProblemsInNLA
References
@misc{baeckelant2026,
author = {Baeckelant, Timothy and Vandaele, Arnaud and Gillis, Nicolas},
title = {Computing Lower Bounds on the Nonnegative Rank via Non-Convex Optimization Solvers},
year = {2026},
eprint = {2605.14058},
archivePrefix = {arXiv},
}
@article{gillis2012,
author = {Gillis, Nicolas and Glineur, Fran{\c{c}}ois},
title = {On the geometric interpretation of the nonnegative rank},
journal = {Linear Algebra Appl.},
volume = {437},
number = {11},
year = {2012},
pages = {2685--2712},
doi = {10.1016/j.laa.2012.06.038},
eprint = {1009.0880},
archivePrefix = {arXiv},
}
@article{hrubes2012,
author = {Hrube{\v{s}}, Pavel},
title = {On the nonnegative rank of distance matrices},
journal = {Inform. Process. Lett.},
volume = {112},
number = {11},
year = {2012},
pages = {457--461},
doi = {10.1016/j.ipl.2012.02.009},
}
@misc{openproblemsinnla-nr04,
author = {Townsend, Alex},
title = {{NR-04}: The nonnegative rank of the nine-point distance matrix},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/nonnegative-and-positive-factorizations/NR-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_00112.
namespace RegistryProblems.OP_00112
noncomputable section
/-- The canonical nine-point squared-distance matrix, with zero-based indices. -/
def distanceNine : Matrix (Fin 9) (Fin 9) ℝ :=
fun i j => ((i.val : ℝ) - (j.val : ℝ)) ^ 2
/-- OP-00112: The nonnegative rank of the nine-point distance matrix -/
def _root_.RegistryProblems.Problem_OP_00112 : Prop :=
∃ W : Matrix (Fin 9) (Fin 6) ℝ,
∃ H : Matrix (Fin 6) (Fin 9) ℝ,
(∀ i j, 0 ≤ W i j) ∧ (∀ i j, 0 ≤ H i j) ∧
W * H = distanceNine
end
end RegistryProblems.OP_00112
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_00112 theorem resolution : RegistryProblems.Problem_OP_00112 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00112" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00112 := 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
The real nine-point squared distance matrix has nonnegative rank seven, including arbitrary real factors and zero or degenerate factor columns. Local serial Lean, two nonauthor final reviews and two published-source Linux verification runs pass.
We prove that the matrix $D_9=((i-j)^2)_{i,j=1}^9$ has nonnegative rank seven. The lower bound combines the polygon-section interpretation of restricted nonnegative rank with Sylvester's rank inequality applied to both factors. In a factorization with at most six terms, each factor would have ordinary rank at least five; their product would then have rank at least four, a contradiction. The known seven-term …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, NR-04/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00112, "The nonnegative rank of the nine-point distance matrix", clopen.solutions.