Full nonnegative rank of the quadratic correlation matrix
For $n \ge 3$ let $C_n$ be the $2^n \times 2^n$ matrix indexed by $a, b \in \{0,1\}^n$ with $C_n(a, b) = (1 - a^{\mathsf T} b)^2$; every entry is given by this formula, including those with $a^{\mathsf T} b > 1$. Let $\operatorname{rank}_+$ be the nonnegative rank over $\mathbb{R}$. The matrix $C_n$ has rank $1 + n(n+1)/2$ (Gillis), and Kaibel and Weltge's rectangle-covering bound gives $\operatorname{rank}_+(C_n) \ge (3/2)^n$. It is a submatrix of a slack matrix of the correlation polytope, so the equality below would give that slack matrix nonnegative rank at least $2^n$ (Vandaele, Gillis, Glineur and Tuyttens).
Problem. Is $\operatorname{rank}_+(C_n) = 2^n$ for every $n \ge 3$?
Source: Vandaele, Gillis, Glineur and Tuyttens (2016), Conjecture 4; stated for n ≥ 3 by OpenProblemsInNLA.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- CO, OC
- Keywords
- extended formulations, nonnegative rank, OpenProblemsInNLA, unique-disjointness matrices
References
@article{vandaele2016,
author = {Vandaele, Arnaud and Gillis, Nicolas and Glineur, Fran{\c{c}}ois and Tuyttens, Daniel},
title = {Heuristics for exact nonnegative matrix factorization},
journal = {J. Global Optim.},
volume = {65},
number = {2},
year = {2016},
pages = {369--400},
doi = {10.1007/s10898-015-0350-z},
eprint = {1411.7245},
archivePrefix = {arXiv},
}
@book{gillis2020,
author = {Gillis, Nicolas},
title = {Nonnegative Matrix Factorization},
publisher = {SIAM},
address = {Philadelphia, PA},
year = {2020},
doi = {10.1137/1.9781611976410},
note = {Section 3.7 and Remark 3.4},
}
@article{kaibel2015,
author = {Kaibel, Volker and Weltge, Stefan},
title = {A short proof that the extension complexity of the correlation polytope grows exponentially},
journal = {Discrete Comput. Geom.},
volume = {53},
number = {2},
year = {2015},
pages = {397--401},
doi = {10.1007/s00454-014-9655-9},
eprint = {1307.3543},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-nr03,
author = {Townsend, Alex},
title = {{NR-03}: Full nonnegative rank of the quadratic correlation 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-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_00111.
namespace RegistryProblems.OP_00111
noncomputable section
open scoped BigOperators Matrix
/-- A Boolean vector with exactly `n` coordinates. -/
abbrev BoolVec (n : ℕ) := Fin n → Bool
/-- The real value represented by one Boolean coordinate. -/
def boolToReal (b : Bool) : ℝ := if b = true then 1 else 0
/-- The ordinary real dot product of two Boolean vectors. -/
def boolDot {n : ℕ} (a b : BoolVec n) : ℝ :=
∑ i : Fin n, boolToReal (a i) * boolToReal (b i)
/-- The complete prescribed quadratic correlation matrix. The subtraction is
over `ℝ`, so entries with dot product greater than one are retained exactly. -/
def cMatrix (n : ℕ) : Matrix (BoolVec n) (BoolVec n) ℝ :=
fun a b => (1 - boolDot a b) ^ 2
/-- Entrywise nonnegativity of a real matrix. -/
def EntrywiseNonnegative {ι κ : Type} (X : Matrix ι κ ℝ) : Prop :=
∀ i j, 0 ≤ X i j
/-- A genuine real nonnegative factorization of a matrix through `Fin r`. -/
def FactorizationData {ι κ : Type} [Fintype ι] [Fintype κ]
(X : Matrix ι κ ℝ) (r : ℕ)
(W : Matrix ι (Fin r) ℝ) (H : Matrix (Fin r) κ ℝ) : Prop :=
EntrywiseNonnegative W ∧ EntrywiseNonnegative H ∧ W * H = X
/-- Existence of a real entrywise-nonnegative factorization of width `r`. -/
def HasNonnegativeFactorization {ι κ : Type} [Fintype ι] [Fintype κ]
(X : Matrix ι κ ℝ) (r : ℕ) : Prop :=
∃ W : Matrix ι (Fin r) ℝ, ∃ H : Matrix (Fin r) κ ℝ,
FactorizationData X r W H
/-- The actual minimum width whenever at least one finite factorization exists.
The value `0` in the impossible branch is only a totalization; all rank
claims below carry the explicit existence premise or establish it first. -/
def nonnegativeRank {ι κ : Type} [Fintype ι] [Fintype κ]
(X : Matrix ι κ ℝ) : ℕ :=
by
classical
exact if h : ∃ r : ℕ, HasNonnegativeFactorization X r then Nat.find h else 0
/-- OP-00111: Full nonnegative rank of the quadratic correlation matrix -/
def _root_.RegistryProblems.Problem_OP_00111 : Prop :=
∀ n : ℕ, 3 ≤ n → nonnegativeRank (cMatrix n) = 2 ^ n
end
end RegistryProblems.OP_00111
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_00111 theorem resolution : RegistryProblems.Problem_OP_00111 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00111" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00111 := 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 n = 7 counterexample to the prescribed real Boolean matrix nonnegative-rank equality, with ten Comparator-boundary exports and the full source correspondence retained.
For subsets $a,b\subseteq[n]$, let $C_n(a,b)=(1-|a\cap b|)^2$, with every entry prescribed. We construct nonnegative rational factors proving $$\operatorname{rank}_+(C_n)\le 2^{n-1}+n+\binom n2+\binom n4.$$ At $n=7$ this gives $\operatorname{rank}_+(C_7)\le127<128$, disproving the universal full-rank conjecture. In fact the displayed bound is strictly below $2^n$ for every $n\ge7$. The construction separates the matrix into a component invariant under complementing its row index and three nonnegative correction …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, NR-03/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00111, "Full nonnegative rank of the quadratic correlation matrix", clopen.solutions.