Finitely many unitary classes with prescribed shifted singular values
For $A \in \mathbb{C}^{N \times N}$ let $s_1(A) \ge \dots \ge s_N(A)$ be its singular values. Two matrices $A, B \in \mathbb{C}^{N \times N}$ have super-identical pseudospectra if $s_j(A - zI) = s_j(B - zI)$ for all $z \in \mathbb{C}$ and $1 \le j \le N$. Unitarily similar matrices have super-identical pseudospectra, but not conversely, already for $N = 3$: a matrix and its transpose always have super-identical pseudospectra, and some $3 \times 3$ matrices are not unitarily similar to their transposes. Fortier Bourque and Ransford proved that for each $N$ there are an integer $m$ and a closed set $E \subset \mathbb{C}^{N \times N}$ of measure zero such that every class of matrices with super-identical pseudospectra is either contained in $E$ or a union of at most $m$ unitary similarity classes.
Problem. Is there, for every $N \ge 1$, an integer $M_N \ge 1$ such that any $A_1, \dots, A_{M_N+1} \in \mathbb{C}^{N \times N}$ with pairwise super-identical pseudospectra include a pair with $A_j = U^* A_i U$ for some $i < j$ and some unitary $U$? Equivalently, is every class of matrices with super-identical pseudospectra a union of at most $M_N$ unitary similarity classes?
Source: Fortier Bourque and Ransford (2009), whose finiteness theorem excludes a closed null set; Ransford (2010), after Theorem 5.4, asks whether it can be removed. In this form, OpenProblemsInNLA.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- RA, SP
- Keywords
- OpenProblemsInNLA, pseudospectra, unitary similarity
References
@article{fortierbourque2009,
author = {Fortier Bourque, Maxime and Ransford, Thomas},
title = {Super-identical pseudospectra},
journal = {J. London Math. Soc. (2)},
volume = {79},
number = {2},
year = {2009},
pages = {511--528},
doi = {10.1112/jlms/jdn085},
}
@article{ransford2010,
author = {Ransford, Thomas},
title = {Pseudospectra and matrix behaviour},
journal = {Banach Center Publ.},
volume = {91},
year = {2010},
pages = {327--338},
doi = {10.4064/bc91-0-19},
}
@misc{openproblemsinnla-sp15,
author = {Townsend, Alex},
title = {{SP-15}: Finitely many unitary classes with prescribed shifted singular values},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/eigenvalues-and-inverse-problems/SP-15/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00122.
namespace RegistryProblems.OP_00122
noncomputable section
open scoped BigOperators Matrix MatrixOrder Matrix.Norms.L2Operator Topology
abbrev Square (n : ℕ) := Matrix (Fin n) (Fin n) ℂ
/-- Mathlib's genuine decreasing Euclidean singular values, zero extended. -/
def singularValue {n : ℕ} (A : Square n) (k : ℕ) : ℝ :=
(Matrix.toEuclideanLin A).singularValues k
/-- The original all-complex-shift, every-ordered-singular-value relation. -/
def SuperIdentical {n : ℕ} (A B : Square n) : Prop :=
∀ (z : ℂ) (k : Fin n),
singularValue (A - z • (1 : Square n)) k.val =
singularValue (B - z • (1 : Square n)) k.val
/-- Exactly the one-sided unitary condition in the canonical question. -/
def UnitarySimilar {n : ℕ} (A B : Square n) : Prop :=
∃ U : Square n, U.conjTranspose * U = 1 ∧ B = U.conjTranspose * A * U
/-- OP-00122: Finitely many unitary classes with prescribed shifted singular values -/
def _root_.RegistryProblems.Problem_OP_00122 : Prop :=
∀ n : ℕ, 1 ≤ n → ∃ M : ℕ, 1 ≤ M ∧
∀ A : Fin (M + 1) → Square n,
(∀ i j, SuperIdentical (A i) (A j)) →
∃ i j : Fin (M + 1), i < j ∧ UnitarySimilar (A i) (A j)
end
end RegistryProblems.OP_00122
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_00122 theorem resolution : RegistryProblems.Problem_OP_00122 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00122" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00122 := 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
The original finite-unitary-class assertion is false: for every M there are M+1 complex 9-by-9 matrices with every ordered singular value equal for every complex shift, and no unitarily similar pair.
There is a nonconstant smooth one-parameter family of complex $9\times9$ matrices whose members have the same singular values for every complex scalar shift, while no two distinct members are unitarily similar; each member is nilpotent with Jordan type $(3,3,3)$. Consequently no uniform finite bound on the number of unitary similarity classes with prescribed shifted singular values exists in dimension nine. …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, SP-15/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00122, "Finitely many unitary classes with prescribed shifted singular values", clopen.solutions.