Number of components of a real interval eigenvalue set
For $L, U \in \mathbb{R}^{n \times n}$ with $L \le U$ entrywise, let $\mathcal A = \{A \in \mathbb{R}^{n \times n} : L \le A \le U\}$, each entry varying independently in its closed interval (singletons allowed), and let $$\Lambda_{\mathbb R}(\mathcal A) = \{\lambda \in \mathbb{R} : Ax = \lambda x \text{ for some } A \in \mathcal A \text{ and } x \in \mathbb{R}^n \setminus \{0\}\}$$ be the set of real eigenvalues of its members. No symmetry is assumed. Hladík, Daney and Tsigaridas note that $\Lambda_{\mathbb R}(\mathcal A)$ is compact, and that deciding whether $0 \in \Lambda_{\mathbb R}(\mathcal A)$ is NP-hard, since it amounts to checking regularity of the interval matrix.
Problem. For every $n \ge 1$ and all such $L$ and $U$, must $\Lambda_{\mathbb R}(\mathcal A)$ have at most $n$ connected components? Equivalently, is it the union of at most $n$ closed bounded intervals, a single point counting as an interval and the empty set as the union of none?
Source: Hladík, Daney and Tsigaridas (2011), §1; posed already in their INRIA report RR-6680 (2008).
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- SP
- Keywords
- interval matrices, OpenProblemsInNLA, real eigenvalues
References
@article{hladik2011,
author = {Hlad{\'\i}k, Milan and Daney, David and Tsigaridas, Elias P.},
title = {An algorithm for addressing the real interval eigenvalue problem},
journal = {J. Comput. Appl. Math.},
volume = {235},
number = {8},
year = {2011},
pages = {2715--2730},
doi = {10.1016/j.cam.2010.11.022},
}
@techreport{hladik2008,
author = {Hlad{\'\i}k, Milan and Daney, David and Tsigaridas, Elias P.},
title = {An algorithm for the real interval eigenvalue problem},
institution = {INRIA},
type = {Research Report},
number = {RR-6680},
year = {2008},
url = {https://inria.hal.science/inria-00329714},
}
@misc{openproblemsinnla-iv06,
author = {Townsend, Alex},
title = {{IV-06}: Number of components of a real interval eigenvalue set},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/intervals-and-absolute-value-equations/IV-06/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00088.
namespace RegistryProblems.OP_00088
noncomputable section
abbrev RealMatrix (n : ℕ) := Matrix (Fin n) (Fin n) ℝ
/-- Entrywise order, without imposing symmetry or coupling distinct entries. -/
def EntrywiseLE {n : ℕ} (L U : RealMatrix n) : Prop :=
∀ i j, L i j ≤ U i j
/-- The entire independent-entry closed interval family; fixed entries are allowed. -/
def InIntervalFamily {n : ℕ} (L U A : RealMatrix n) : Prop :=
EntrywiseLE L A ∧ EntrywiseLE A U
/-- A real eigenvalue means an actual nonzero real eigenvector. -/
def HasRealEigenvalue {n : ℕ} (A : RealMatrix n) (lam : ℝ) : Prop :=
∃ v : Fin n → ℝ, v ≠ 0 ∧ A.mulVec v = lam • v
/-- The union of the real eigenvalues of every admissible matrix. -/
def realEigenvalueSet {n : ℕ} (L U : RealMatrix n) : Set ℝ :=
{lam | ∃ A : RealMatrix n, InIntervalFamily L U A ∧ HasRealEigenvalue A lam}
/-- Cardinality is used, so infinite component spaces cannot count as zero. -/
def componentCard (S : Set ℝ) : Cardinal :=
Cardinal.mk (ConnectedComponents S)
/-- OP-00088: Number of components of a real interval eigenvalue set -/
def _root_.RegistryProblems.Problem_OP_00088 : Prop :=
∀ (n : ℕ), 1 ≤ n → ∀ (L U : RealMatrix n),
EntrywiseLE L U → componentCard (realEigenvalueSet L U) ≤ (n : Cardinal)
end
end RegistryProblems.OP_00088
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_00088 theorem resolution : RegistryProblems.Problem_OP_00088 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00088" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00088 := 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 answer to the original universal at-most-dimension bound for connected components of the real eigenvalue union of an independent-entry interval matrix.
A two-parameter $3\times3$ interval matrix with integer endpoints has at least four connected components in its real eigenvalue set. The matrix has rows $(25,a,b)$, $(1,-1,0)$ and $(1,0,1)$, with $a\in[-166,-16]$ and $b\in[9,159]$ varying independently. Its characteristic polynomial is affine in each parameter, with no mixed term. So for each real $\lambda$ its exact range over the box is an explicit interval, …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, IV-06/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00088, "Number of components of a real interval eigenvalue set", clopen.solutions.