Critical-point counts for symmetric rank-two approximation with diagonal zeros
For $s \in \{1, 2, 3, 4\}$ and $n \ge \max\{3, s\}$ let $W_{n,s}$ be the variety of complex symmetric $n \times n$ matrices $X$ of rank at most $2$ with $x_{11} = \cdots = x_{ss} = 0$. Let $e_{n,s}$ be its Euclidean distance degree for the Frobenius metric on symmetric matrices: the number of complex critical points, on the smooth locus of $W_{n,s}$, of $$d_U(X) = \sum_i (x_{ii} - u_{ii})^2 + 2 \sum_{i < j} (x_{ij} - u_{ij})^2$$ for a generic symmetric $U \in \mathbb{C}^{n \times n}$, that is, for $U$ outside a proper algebraic subset. The distance is bilinear, without complex conjugation.
Problem. Is $$e_{n,s} = \begin{cases} 3(n - 1) - 2, & s = 1, \\ 9(n - 2) - 2, & s = 2, \\ 27(n - 3) + 4, & s = 3, \\ 81(n - 4) + 28, & s = 4, \end{cases}$$ for all $s \in \{1, 2, 3, 4\}$ and $n \ge \max\{3, s\}$?
Source: Kubjas, Sodomaco and Tsigaridas (2022), Conjecture 5.6, stated there without a range of n; OpenProblemsInNLA requires n ≥ max{3, s}.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- AG — Algebraic Geometry
- Secondary
- NA, OC
- Keywords
- Euclidean distance degrees, low-rank approximations, OpenProblemsInNLA, symmetric matrices
References
@article{kubjas2022,
author = {Kubjas, Kaie and Sodomaco, Luca and Tsigaridas, Elias},
title = {Exact solutions in low-rank approximation with zeros},
journal = {Linear Algebra Appl.},
volume = {641},
year = {2022},
pages = {67--97},
doi = {10.1016/j.laa.2022.01.021},
eprint = {2010.15636},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-ra20,
author = {Townsend, Alex},
title = {{RA-20}: Critical-point counts for symmetric rank-two approximation with diagonal zeros},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/randomized-and-low-rank-approximation/RA-20/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00118.
namespace RegistryProblems.OP_00118
noncomputable section
open scoped BigOperators
abbrev Mat (n : ℕ) := Matrix (Fin n) (Fin n) ℂ
abbrev Variables (n : ℕ) := Fin n × Fin n
abbrev Poly (n : ℕ) := MvPolynomial (Variables n) ℂ
def coordinates {n : ℕ} (X : Mat n) : Variables n → ℂ :=
fun ij => X ij.1 ij.2
def matrixOfCoordinates {n : ℕ} (x : Variables n → ℂ) : Mat n :=
fun i j => x (i, j)
/-- The actual symmetric rank-at-most-two variety, with the first `s` diagonal
entries zero. The canonical parameter range is imposed by the conjecture. -/
def variety (n s : ℕ) : Set (Mat n) :=
{X | X.IsSymm ∧ X.rank ≤ 2 ∧ ∀ i : Fin n, i.val < s → X i i = 0}
def coordinateVariety (n s : ℕ) : Set (Variables n → ℂ) :=
{x | matrixOfCoordinates x ∈ variety n s}
/-- Taking all polynomials vanishing on the actual point set gives its reduced
coordinate ring, independently of any proposed equations or chosen generators. -/
def definingIdeal (n s : ℕ) : Ideal (Poly n) :=
MvPolynomial.vanishingIdeal ℂ (coordinateVariety n s)
abbrev CoordinateRing (n s : ℕ) := Poly n ⧸ definingIdeal n s
/-- A point is smooth precisely when its point prime in the reduced coordinate
ring lies in Mathlib's smooth locus over `ℂ`. The prime is specified by its
pullback, so no prime, chart, dimension or Jacobian-rank assumption is supplied. -/
def SmoothPoint (n s : ℕ) (X : Mat n) : Prop :=
X ∈ variety n s ∧
∃ p : PrimeSpectrum (CoordinateRing n s),
PrimeSpectrum.comap (Ideal.Quotient.mk (definingIdeal n s)) p =
MvPolynomial.pointToPoint (coordinates X) ∧
p ∈ Algebra.smoothLocus ℂ (CoordinateRing n s)
/-- The Zariski tangent directions annihilate the differentials of every
polynomial in the reduced defining ideal. -/
def TangentVector (n s : ℕ) (X Z : Mat n) : Prop :=
∀ p ∈ definingIdeal n s,
(∑ ij : Variables n,
MvPolynomial.eval (coordinates X) (MvPolynomial.pderiv ij p) *
coordinates Z ij) = 0
/-- The complex bilinear extension of the full Frobenius squared distance.
On symmetric matrices, each off-diagonal term occurs twice. -/
def fullFrobeniusDistance {n : ℕ} (U X : Mat n) : ℂ :=
∑ i, ∑ j, (X i j - U i j) ^ 2
def SmoothCriticalPoint (n s : ℕ) (U X : Mat n) : Prop :=
SmoothPoint n s X ∧
∀ Z : Mat n, TangentVector n s X Z →
fderiv ℂ (fullFrobeniusDistance U) X Z = 0
def criticalSet (n s : ℕ) (U : Mat n) : Set (Mat n) :=
{X | SmoothCriticalPoint n s U X}
/-- A cardinal equality, so an infinite critical set is never silently assigned
the finite count zero. -/
def HasCriticalCount (n s : ℕ) (U : Mat n) (m : ℕ) : Prop :=
Cardinal.mk {X : Mat n // X ∈ criticalSet n s U} = (m : Cardinal)
/-- A genuine generic count: the exceptional polynomial need not be the one
used by the counterexample, and must not vanish identically on symmetric data.
Any nonempty Zariski-open set contains such a nonempty principal open set. -/
def HasGenericCriticalCount (n s m : ℕ) : Prop :=
∃ q : Poly n,
(∃ U : Mat n, U.IsSymm ∧ MvPolynomial.eval (coordinates U) q ≠ 0) ∧
∀ U : Mat n, U.IsSymm → MvPolynomial.eval (coordinates U) q ≠ 0 →
HasCriticalCount n s U m
def predictedCount (n s : ℕ) : ℕ :=
if s = 1 then 3 * (n - 1) - 2
else if s = 2 then 9 * (n - 2) - 2
else if s = 3 then 27 * (n - 3) + 4
else if s = 4 then 81 * (n - 4) + 28
else 0
/-- OP-00118: Critical-point counts for symmetric rank-two approximation with diagonal zeros -/
def _root_.RegistryProblems.Problem_OP_00118 : Prop :=
∀ n s : ℕ, 3 ≤ n → 1 ≤ s → s ≤ 4 → s ≤ n →
HasGenericCriticalCount n s (predictedCount n s)
end
end RegistryProblems.OP_00118
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_00118 theorem resolution : RegistryProblems.Problem_OP_00118 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00118" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00118 := 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 negative resolution of the original joint generic critical-count conjecture: the actual count at n=s=3 is three, whereas its formula predicts four.
Every hollow symmetric complex $3\times3$ matrix has the form $X(a,b,c)$ with off-diagonal entries $a,b,c$ and determinant $2abc$, so the variety of such matrices of rank at most two is the union of the three coordinate planes, and its smooth locus consists of the points with exactly one zero coordinate. For symmetric data with nonzero off-diagonal entries $\alpha,\beta,\gamma$, the bilinear full-Frobenius …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, RA-20/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00118, "Critical-point counts for symmetric rank-two approximation with diagonal zeros", clopen.solutions.