The smallest-multiplier rule for nearest unit-absolute-determinant matrices
For $n \ge 2$ let $\mathcal G_n = \{X \in \mathbb{R}^{n \times n} : \det X \in \{-1, 1\}\}$, both signs allowed, and let $\|\cdot\|_F$ be the Frobenius norm. For a real data matrix $U \in \mathbb{R}^{n \times n}$, the real stationary pairs are $$\mathcal C(U) = \{(X, c) \in \mathcal G_n \times \mathbb{R} : X^{\mathsf T}(U - X) = cI_n\};$$ a nearest point of $\mathcal G_n$ to $U$ satisfies these critical equations for some $c$. Generic means outside a proper real algebraic subset of $\mathbb{R}^{n \times n}$; a generic $U$ is invertible with distinct squared singular values, and $\mathcal C(U)$ is finite. Baaijens and Draisma give an algorithm that finds the real stationary pairs through the real roots $c$ of an elimination polynomial, and in their experiments the root of smallest absolute value appeared to give the nearest point.
Problem. For every $n \ge 2$ and generic $U \in \mathbb{R}^{n \times n}$, choose $(X_*, c_*) \in \mathcal C(U)$ with $|c_*|$ minimal. Does $$\|U - X_*\|_F = \min_{X \in \mathcal G_n} \|U - X\|_F$$ hold? If several pairs attain the minimal $|c|$, the question may be restricted to the generic $U$ for which the choice is unique.
Source: Baaijens and Draisma (2015), Problem 4.3, stated there through the real roots of an elimination polynomial; in this form, OpenProblemsInNLA.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- AG, OC
- Keywords
- Euclidean distance degree, matrix nearness problems, OpenProblemsInNLA
References
@article{baaijens2015,
author = {Baaijens, Jasmijn A. and Draisma, Jan},
title = {Euclidean distance degrees of real algebraic groups},
journal = {Linear Algebra Appl.},
volume = {467},
year = {2015},
pages = {174--187},
doi = {10.1016/j.laa.2014.11.012},
eprint = {1405.0422},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-sp04,
author = {Townsend, Alex},
title = {{SP-04}: The smallest-multiplier rule for nearest unit-absolute-determinant matrices},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/eigenvalues-and-inverse-problems/SP-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_00119.
namespace RegistryProblems.OP_00119
noncomputable section
open scoped BigOperators Matrix
abbrev Mat (n : ℕ) := Matrix (Fin n) (Fin n) ℝ
/-- Both determinant signs, exactly as in the canonical problem. -/
def Feasible {n : ℕ} (X : Mat n) : Prop := |X.det| = 1
/-- The actual sum-of-squares Frobenius norm, with its nonnegative square root. -/
def frobeniusSq {n : ℕ} (X : Mat n) : ℝ := ∑ i, ∑ j, (X i j) ^ 2
def frobeniusNorm {n : ℕ} (X : Mat n) : ℝ := Real.sqrt (frobeniusSq X)
/-- Every real stationary matrix and its real multiplier, without diagonal restrictions. -/
def Stationary {n : ℕ} (U X : Mat n) (c : ℝ) : Prop :=
Feasible X ∧ Xᵀ * (U - X) = c • (1 : Mat n)
def stationaryPairs {n : ℕ} (U : Mat n) : Set (Mat n × ℝ) :=
{p | Stationary U p.1 p.2}
/-- Unique minimizing pair, compared with the entire real stationary set. -/
def UniqueLeastStationary {n : ℕ} (U X : Mat n) (c : ℝ) : Prop :=
Stationary U X c ∧ ∀ Y d, Stationary U Y d →
|c| ≤ |d| ∧ (|c| = |d| → Y = X ∧ d = c)
/-- Actual global nearestness, including attainment at the displayed feasible matrix. -/
def IsNearest {n : ℕ} (U X : Mat n) : Prop :=
Feasible X ∧ ∀ Y, Feasible Y → frobeniusNorm (U - X) ≤ frobeniusNorm (U - Y)
/-- Invertibility and distinct squared singular values: the real Gram polynomial has no repeated roots. -/
def RegularData {n : ℕ} (U : Mat n) : Prop :=
U.det ≠ 0 ∧ (Uᵀ * U).charpoly.roots.Nodup
/-- The complete selection claim outside one arbitrary proper real algebraic exception.
The finite and regular premises retain the stated generic domain. -/
def GenericSelectionRule (n : ℕ) : Prop :=
∃ p : MvPolynomial (Fin n × Fin n) ℝ, p ≠ 0 ∧
∀ U : Mat n, MvPolynomial.eval (fun ij => U ij.1 ij.2) p ≠ 0 →
RegularData U → (stationaryPairs U).Finite →
∀ X c, UniqueLeastStationary U X c → IsNearest U X
/-- OP-00119: The smallest-multiplier rule for nearest unit-absolute-determinant matrices -/
def _root_.RegistryProblems.Problem_OP_00119 : Prop :=
∀ n : ℕ, 2 ≤ n → GenericSelectionRule n
end
end RegistryProblems.OP_00119
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_00119 theorem resolution : RegistryProblems.Problem_OP_00119 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00119" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00119 := 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 original generic selection rule refuted: a nonempty open family of real 3×3 data matrices has invertibility, distinct squared singular values, a finite full stationary set, a unique least-absolute-multiplier pair and a strictly closer feasible matrix in the actual Frobenius norm.
For real data $U$, consider the real stationary pairs $(X,c)$ with $|\det X|=1$ and $X^{T}(U-X)=cI$, and the rule that selects a pair with smallest $|c|$ as the nearest such matrix in Frobenius norm. The rule fails for every diagonal $U=\operatorname{diag}(s_1,s_2,s_3)$ with $7/4<s_1<s_2<s_3<44/25$. Every stationary matrix is then diagonal, no stationary pair has $0\le c\le 13/25$, and a monotonicity comparison of …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, SP-04/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00119, "The smallest-multiplier rule for nearest unit-absolute-determinant matrices", clopen.solutions.