Connectedness of minimal positive semidefinite factorization orbits
Let $\mathbb S^k_+$ be the cone of real symmetric positive semidefinite $k \times k$ matrices and $\operatorname{rank}_{\mathrm{psd}}$ the positive semidefinite rank. For an entrywise nonnegative $M \in \mathbb{R}^{p \times q}$, let $\mathcal F_k(M)$ be the set of tuples $(A_1, \dots, A_p, B_1, \dots, B_q) \in (\mathbb S^k_+)^{p+q}$ with $\operatorname{tr}(A_i B_j) = M_{ij}$ for all $i, j$, with the Euclidean subspace topology. The group $GL(k, \mathbb{R})$ acts on it by $$A_i \mapsto S^{\mathsf T} A_i S, \qquad B_j \mapsto S^{-1} B_j S^{-\mathsf T},$$ and $\mathcal F_k(M)/GL(k, \mathbb{R})$ carries the quotient topology. Fawzi, Gouveia, Parrilo, Robinson and Thomas proved that $\mathcal F_2(M)/GL(2, \mathbb{R})$ is connected whenever $\operatorname{rank}(M) = 3$ and $\operatorname{rank}_{\mathrm{psd}}(M) = 2$.
Problem. For all $k \ge 3$ and $p, q \ge 1$, is $\mathcal F_k(M)/GL(k, \mathbb{R})$ connected for every entrywise nonnegative $M \in \mathbb{R}^{p \times q}$ with $\operatorname{rank}(M) = k(k+1)/2$ and $\operatorname{rank}_{\mathrm{psd}}(M) = k$?
Source: Fawzi, Gouveia, Parrilo, Robinson and Thomas (2015), Problem 9.4; stated for k ≥ 3 by OpenProblemsInNLA.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- AG, OC
- Keywords
- matrix factorizations, OpenProblemsInNLA, positive semidefinite rank
References
@article{fawzi2015,
author = {Fawzi, Hamza and Gouveia, Jo{\~a}o and Parrilo, Pablo A. and Robinson, Richard Z. and Thomas, Rekha R.},
title = {Positive semidefinite rank},
journal = {Math. Program.},
volume = {153},
number = {1},
year = {2015},
pages = {133--177},
doi = {10.1007/s10107-015-0922-1},
eprint = {1407.4095},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-pf02,
author = {Townsend, Alex},
title = {{PF-02}: Connectedness of minimal positive semidefinite factorization orbits},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/nonnegative-and-positive-factorizations/PF-02/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00113.
namespace RegistryProblems.OP_00113
noncomputable section
open Matrix
abbrev Mat (m n : ℕ) := Matrix (Fin m) (Fin n) ℝ
abbrev FactorTuple (p q k : ℕ) := (Fin p → Mat k k) × (Fin q → Mat k k)
/-- Every row and column factor is genuinely real positive semidefinite. -/
def IsFactorization {p q k : ℕ} (M : Mat p q) (F : FactorTuple p q k) : Prop :=
(∀ i, (F.1 i).PosSemidef) ∧ (∀ j, (F.2 j).PosSemidef) ∧
∀ i j, Matrix.trace (F.1 i * F.2 j) = M i j
/-- The full factorization space with its inherited finite-dimensional Euclidean topology. -/
abbrev Factorization {p q : ℕ} (M : Mat p q) (k : ℕ) :=
{F : FactorTuple p q k // IsFactorization M F}
/-- The actual minimum among all positive integer factor sizes, including attainment. -/
def IsPSDRank {p q : ℕ} (M : Mat p q) (k : ℕ) : Prop :=
IsLeast {ℓ : ℕ | 1 ≤ ℓ ∧ Nonempty (Factorization M ℓ)} k
/-- A single genuine invertible change of basis, on all row and column factors. -/
def Congruent {p q k : ℕ} {M : Mat p q} (F G : Factorization M k) : Prop :=
∃ S : (Mat k k)ˣ,
(∀ i, G.val.1 i = (↑S : Mat k k).transpose * F.val.1 i * ↑S) ∧
(∀ j, G.val.2 j = (↑(S⁻¹) : Mat k k) * F.val.2 j * (↑(S⁻¹) : Mat k k).transpose)
/-- Quotient topology on actual congruence orbits; the public orbit theorem checks exact equality. -/
abbrev OrbitSpace {p q : ℕ} (M : Mat p q) (k : ℕ) :=
Quot (@Congruent p q k M)
/-- OP-00113: Connectedness of minimal positive semidefinite factorization orbits -/
def _root_.RegistryProblems.Problem_OP_00113 : Prop :=
∀ (k p q : ℕ), 3 ≤ k → 1 ≤ p → 1 ≤ q → ∀ M : Mat p q,
(∀ i j, 0 ≤ M i j) → M.rank = k * (k + 1) / 2 → IsPSDRank M k →
IsConnected (Set.univ : Set (OrbitSpace M k))
end
end RegistryProblems.OP_00113
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_00113 theorem resolution : RegistryProblems.Problem_OP_00113 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00113" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00113 := 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 exact counterexample to the original universal connectedness question: a positive integer matrix of actual rank six and attained PSD rank three has a disconnected full real congruence quotient with its Euclidean quotient topology.
We give a positive integer $6\times6$ matrix of ordinary rank six and real positive semidefinite rank three whose space of minimal positive semidefinite factorizations, modulo real congruence, is disconnected. A continuous orientation sign is invariant under every size-three congruence and takes both values on explicit positive definite factorizations. This gives a negative answer to the connectedness question of Fawzi–Gouveia–Parrilo–Robinson–Thomas. An …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, PF-02/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00113, "Connectedness of minimal positive semidefinite factorization orbits", clopen.solutions.