Johnson's derivative-realizability conjecture
For a real square matrix $A$ let $p_A(z) = \det(zI - A)$. A list of $n$ complex numbers is realizable if it is the spectrum of an entrywise nonnegative $n \times n$ matrix. The problem below is Johnson's conjecture that the critical points of a realizable list, the zeros of the derivative of its characteristic polynomial counted with multiplicity, are again realizable. Hoover, McCormick, Paparella and Thrall record that Cronin and Laffey settled it for $n \le 4$, and for $n \le 6$ when $\operatorname{tr} A = 0$.
Problem. For every integer $n \ge 5$ and every entrywise nonnegative $A \in \mathbb{R}^{n \times n}$, is there an entrywise nonnegative $B \in \mathbb{R}^{(n-1) \times (n-1)}$ with $$\det(zI - B) = \frac{1}{n}\, p_A'(z)$$ as polynomials in $z$? Neither $A$ nor $B$ need be symmetric or diagonalizable, and $B$ must have order exactly $n - 1$: appending zero eigenvalues is not allowed.
Source: Johnson (personal communication, 2015), recorded as Conjecture 1.2 by Hoover, McCormick, Paparella and Thrall (2018); Monov (2008) had asked the weaker question that allows extra zero eigenvalues. Stated for n ≥ 5 by OpenProblemsInNLA.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- SP
- Keywords
- critical points, inverse eigenvalue problems, nonnegative matrices, OpenProblemsInNLA
References
@article{hoover2018,
author = {Hoover, Sarah L. and McCormick, Daniel A. and Paparella, Pietro and Thrall, Amber R.},
title = {On the realizability of the critical points of a realizable list},
journal = {Linear Algebra Appl.},
volume = {555},
year = {2018},
pages = {301--313},
doi = {10.1016/j.laa.2018.06.024},
eprint = {1712.05454},
archivePrefix = {arXiv},
}
@article{monov2008,
author = {Monov, Vladimir V.},
title = {A family of symmetric polynomials of the eigenvalues of a matrix},
journal = {Linear Algebra Appl.},
volume = {429},
number = {8-9},
year = {2008},
pages = {2199--2208},
doi = {10.1016/j.laa.2008.06.014},
}
@article{cronin2014,
author = {Cronin, Anthony G. and Laffey, Thomas J.},
title = {Perturbations on constructible lists preserving realizability in the {NIEP} and questions of {M}onov},
journal = {Linear Algebra Appl.},
volume = {445},
year = {2014},
pages = {206--222},
doi = {10.1016/j.laa.2013.12.003},
}
@misc{openproblemsinnla-is03,
author = {Townsend, Alex},
title = {{IS-03}: Johnson's derivative-realizability conjecture},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/eigenvalues-and-inverse-problems/IS-03/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00086.
namespace RegistryProblems.OP_00086
noncomputable section
open Matrix Polynomial
open scoped Matrix
/-- Actual real square matrices of the indicated finite order. -/
abbrev RealMatrix (n : ℕ) := Matrix (Fin n) (Fin n) ℝ
/-- Entrywise nonnegativity; it is not positive-semidefinite order. -/
def EntrywiseNonnegative {n : ℕ} (A : RealMatrix n) : Prop :=
∀ i j, 0 ≤ A i j
/-- The actual formal derivative, scaled by the reciprocal of the matrix order. -/
def normalizedDerivative (n : ℕ) (p : ℝ[X]) : ℝ[X] :=
((n : ℝ)⁻¹) • p.derivative
/-- OP-00086: Johnson's derivative-realizability conjecture -/
def _root_.RegistryProblems.Problem_OP_00086 : Prop :=
∀ n : ℕ, 5 ≤ n → ∀ A : RealMatrix n, EntrywiseNonnegative A →
∃ B : RealMatrix (n - 1), EntrywiseNonnegative B ∧
B.charpoly = normalizedDerivative n A.charpoly
end
end RegistryProblems.OP_00086
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_00086 theorem resolution : RegistryProblems.Problem_OP_00086 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00086" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00086 := 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 Johnson's original universal normalized-characteristic-polynomial derivative realizability conjecture, with genuine arbitrary-matrix trace certificates and the unchanged order-seven source witness.
Let $C_k$ be the permutation matrix of a directed $k$-cycle, and let $A=\operatorname{diag}(\tfrac12,C_2,C_4)$. This is an entrywise nonnegative real $7\times7$ matrix with characteristic polynomial $p(z)=(z-\tfrac12)(z^2-1)(z^4-1)$. The normalized derivative $q=p'/7$ is not the characteristic polynomial of any entrywise nonnegative real $6\times6$ matrix. Newton's identities give the power sums $s_k$ of the roots of $q$ as exact rationals, and $s_7=-8593/823543<0$. If a …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, IS-03/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00086, "Johnson's derivative-realizability conjecture", clopen.solutions.