Rational factors for rational completely positive boundary matrices
A real symmetric matrix is completely positive if it equals $BB^{\mathsf T}$ for an entrywise nonnegative real matrix $B$ with finitely many columns. Let $\mathcal{CP}_n$ be the cone of completely positive $n \times n$ matrices, and $\partial \mathcal{CP}_n$ its boundary in the space of real symmetric $n \times n$ matrices. Dutour Sikirić, Schürmann and Vallentin proved that every rational matrix in the interior of $\mathcal{CP}_n$ is $BB^{\mathsf T}$ for some entrywise nonnegative rational $B$; Shaked-Monderer, Dür and Berman proved the same for rational completely positive matrices of rank at most $2$, and for those whose graph has no odd cycle of length greater than $3$.
Problem. For every $n \ge 5$ and every rational $A \in \partial \mathcal{CP}_n$, is there a finite $m \ge 1$ and an entrywise nonnegative $B \in \mathbb{Q}^{n \times m}$ with $A = BB^{\mathsf T}$? The width $m$ is unrestricted.
Source: Shaked-Monderer, Dür and Berman (2018), Conjecture 1, which they reduce to the boundary of the completely positive cone; posed for the boundary as an Open Problem by Berman and Shaked-Monderer (2025), §2; after a question of Berman, Dür and Shaked-Monderer (2015), §4.1. Stated for n ≥ 5 by OpenProblemsInNLA.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- OC
- Keywords
- completely positive matrices, OpenProblemsInNLA, rational factorizations
References
@article{berman2025,
author = {Berman, Abraham and Shaked-Monderer, Naomi},
title = {Completely positive matrices over sets},
journal = {Commun. Optim. Theory},
volume = {2025},
year = {2025},
pages = {Paper No. 23},
doi = {10.23952/cot.2025.23},
}
@article{berman2015,
author = {Berman, Abraham and D{\"u}r, Mirjam and Shaked-Monderer, Naomi},
title = {Open problems in the theory of completely positive and copositive matrices},
journal = {Electron. J. Linear Algebra},
volume = {29},
year = {2015},
pages = {46--58},
doi = {10.13001/1081-3810.2943},
}
@article{dutoursikiric2017,
author = {Dutour Sikiri{\'c}, Mathieu and Sch{\"u}rmann, Achill and Vallentin, Frank},
title = {Rational factorizations of completely positive matrices},
journal = {Linear Algebra Appl.},
volume = {523},
year = {2017},
pages = {46--51},
doi = {10.1016/j.laa.2017.02.017},
eprint = {1701.03148},
archivePrefix = {arXiv},
}
@article{shakedmonderer2018,
author = {Shaked-Monderer, Naomi and D{\"u}r, Mirjam and Berman, Abraham},
title = {Complete positivity over the rationals},
journal = {Pure Appl. Funct. Anal.},
volume = {3},
number = {4},
year = {2018},
pages = {681--691},
}
@misc{openproblemsinnla-pf03,
author = {Townsend, Alex},
title = {{PF-03}: Rational factors for rational completely positive boundary matrices},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/nonnegative-and-positive-factorizations/PF-03/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00114.
namespace RegistryProblems.OP_00114
noncomputable section
open scoped BigOperators Classical Matrix
abbrev QMat (m n : ℕ) := Matrix (Fin m) (Fin n) ℚ
abbrev RMat (m n : ℕ) := Matrix (Fin m) (Fin n) ℝ
/-- The actual symmetric-matrix subspace, with its inherited subtype topology. -/
abbrev SymMatrix (F : Type) (n : ℕ) :=
{A : Matrix (Fin n) (Fin n) F // A.IsSymm}
def castMatrix {m n : ℕ} (A : QMat m n) : RMat m n :=
A.map (fun q : ℚ => (q : ℝ))
/-- Only the already proved generic map-symmetry fact constructs the subtype. -/
def realCast {n : ℕ} (A : SymMatrix ℚ n) : SymMatrix ℝ n :=
⟨castMatrix A.val, A.property.map (fun q : ℚ => (q : ℝ))⟩
def CompletelyPositive {n : ℕ} (A : SymMatrix ℝ n) : Prop :=
∃ m : ℕ, 1 ≤ m ∧ ∃ B : RMat n m,
(∀ i j, 0 ≤ B i j) ∧ A.val = B * Bᵀ
def CPSet (n : ℕ) : Set (SymMatrix ℝ n) :=
{A | CompletelyPositive A}
def RationalFactor {n : ℕ} (A : SymMatrix ℚ n) : Prop :=
∃ m : ℕ, 1 ≤ m ∧ ∃ B : QMat n m,
(∀ i j, 0 ≤ B i j) ∧ A.val = B * Bᵀ
/-- OP-00114: Rational factors for rational completely positive boundary matrices -/
def _root_.RegistryProblems.Problem_OP_00114 : Prop :=
∀ n : ℕ, 5 ≤ n → ∀ A : SymMatrix ℚ n,
realCast A ∈ frontier (CPSet n) → RationalFactor A
end
end RegistryProblems.OP_00114
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_00114 theorem resolution : RegistryProblems.Problem_OP_00114 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00114" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00114 := 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
Complete Lean formalization of the negative answer to the original PF-03 universal question, with arbitrary positive finite factor widths and frontier in the real symmetric-matrix subtype. Local serial Lean, two independent nonauthor final reviews and two published-source Linux Comparator/kernel/sandbox runs pass.
An explicit integer matrix of order $444$ and rank seven is constructed that is completely positive over the reals but has no nonnegative rational Gram factor of any finite width. All its entries are strictly positive, and its real cp-rank is seven. The construction gives a negative answer to the universal boundary-factorization question. The obstruction is a rational polyhedral cone …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, PF-03/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00114, "Rational factors for rational completely positive boundary matrices", clopen.solutions.