Where a symmetric stochastic matrix can be spectrally unique
For $n \ge 4$ let $\mathcal{S}_n$ be the convex polytope of real symmetric, entrywise nonnegative $n \times n$ matrices with all row sums $1$ (the symmetric doubly stochastic matrices), and let $C_n = (\mathbf{1}\mathbf{1}^T - I)/(n-1)$. A matrix $A \in \mathcal{S}_n$ is spectrally unique if every $B \in \mathcal{S}_n$ with the same eigenvalues, counted with multiplicity, is $R^TAR$ for some permutation matrix $R$. Write $[X, Y]$ for the segment $\{(1-t)X + tY : 0 \le t \le 1\}$, and $\operatorname{vert}(\mathcal{S}_n)$ for the set of vertices (extreme points) of $\mathcal{S}_n$, which need not be permutation matrices. Mourad and Abbas determined the spectrally unique matrices for $n = 3$.
Problem. For every $n \ge 4$, does every spectrally unique $A \in \mathcal{S}_n$ with $\operatorname{tr} A > 0$ lie in $$[I, C_n] \cup \bigcup_{V \in \operatorname{vert}(\mathcal{S}_n)} \bigl([I, V] \cup [C_n, V]\bigr)?$$
Source: Mourad and Abbas (2013 preprint, Conjecture 5.1; Linear Multilinear Algebra 2015), read as a necessary condition; stated for n ≥ 4 by OpenProblemsInNLA, the case n = 3 being solved there.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- CO, SP
- Keywords
- doubly stochastic matrices, inverse eigenvalue problems, OpenProblemsInNLA
References
@article{mourad2015,
author = {Mourad, Bassam and Abbas, Hassan},
title = {On the symmetric doubly stochastic matrices that are determined by their spectra and their connection with spectral graph theory},
journal = {Linear Multilinear Algebra},
volume = {63},
number = {5},
year = {2015},
pages = {869--881},
doi = {10.1080/03081087.2014.903590},
eprint = {1310.1273},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-is02,
author = {Townsend, Alex},
title = {{IS-02}: Where a symmetric stochastic matrix can be spectrally unique},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/eigenvalues-and-inverse-problems/IS-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_00085.
namespace RegistryProblems.OP_00085
noncomputable section
open scoped BigOperators
abbrev Mat (n : ℕ) := Matrix (Fin n) (Fin n) ℝ
def symmetric {n : ℕ} (A : Mat n) : Prop := ∀ i j, A i j = A j i
def entrywiseNonnegative {n : ℕ} (A : Mat n) : Prop := ∀ i j, 0 ≤ A i j
def stochastic {n : ℕ} (A : Mat n) : Prop :=
∀ i, (∑ j : Fin n, A i j) = 1
def symmetricStochastic (n : ℕ) : Set (Mat n) :=
{A | symmetric A ∧ entrywiseNonnegative A ∧ stochastic A}
def trace {n : ℕ} (A : Mat n) : ℝ := ∑ i : Fin n, A i i
def permute {n : ℕ} (σ : Equiv.Perm (Fin n)) (A : Mat n) : Mat n :=
fun i j => A (σ i) (σ j)
def permutationSimilar {n : ℕ} (A B : Mat n) : Prop :=
∃ σ : Equiv.Perm (Fin n), B = permute σ A
/-- For real symmetric matrices, characteristic-polynomial equality is the
exact finite-dimensional encoding of equality of eigenvalues with
multiplicities used by the source theorem. The explicit bridge contract below
must connect this encoding to the real root multiset. -/
def sameSpectrum {n : ℕ} (A B : Mat n) : Prop :=
Matrix.charpoly A = Matrix.charpoly B
def spectrallyUnique {n : ℕ} (A : Mat n) : Prop :=
∀ B, B ∈ symmetricStochastic n → sameSpectrum A B → permutationSimilar A B
def segment {n : ℕ} (X Y : Mat n) : Set (Mat n) :=
{Z | ∃ t : ℝ, 0 ≤ t ∧ t ≤ 1 ∧ Z = (1 - t) • X + t • Y}
def vertex (n : ℕ) (V : Mat n) : Prop :=
V ∈ symmetricStochastic n ∧
∀ U W, U ∈ symmetricStochastic n → W ∈ symmetricStochastic n →
∀ t : ℝ, 0 ≤ t → t ≤ 1 →
V = (1 - t) • U + t • W → t = 0 ∨ t = 1 ∨ U = W
def flatMatrix (n : ℕ) : Mat n :=
fun i j => if i = j then 0 else (1 : ℝ) / ((n - 1 : ℕ) : ℝ)
def assertedLocus (n : ℕ) : Set (Mat n) :=
segment (1 : Mat n) (flatMatrix n) ∪
{A | ∃ V, vertex n V ∧ (A ∈ segment (1 : Mat n) V ∨
A ∈ segment (flatMatrix n) V)}
/-- OP-00085: Where a symmetric stochastic matrix can be spectrally unique -/
def _root_.RegistryProblems.Problem_OP_00085 : Prop :=
∀ n, 4 ≤ n → ∀ A : Mat n,
A ∈ symmetricStochastic n → 0 < trace A →
spectrallyUnique A → A ∈ assertedLocus n
end
end RegistryProblems.OP_00085
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_00085 theorem resolution : RegistryProblems.Problem_OP_00085 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00085" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00085 := 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 order-four counterexample to the original spectral-uniqueness locus condition, independently reviewed and verified by the actual non-root Linux sandbox, Comparator, permitted-axiom audit and default kernel.
Let $A=\operatorname{diag}(S,\tfrac12 J)$, where $S$ is the $2\times2$ swap matrix and $J$ the $2\times2$ all-ones matrix. It is a real symmetric, entrywise nonnegative, stochastic $4\times4$ matrix with spectrum $\{1,1,0,-1\}$ and trace one, and it is spectrally unique up to permutation. For a symmetric stochastic $B$ with this spectrum, the multiplicity of the eigenvalue one equals the number of connected components …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, IS-02/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00085, "Where a symmetric stochastic matrix can be spectrally unique", clopen.solutions.