Polynomial-size vertex test for inverse M-matrix intervals
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\}$, its entries varying independently and $L_{ij} = U_{ij}$ allowed, and let $C = (L+U)/2$ and $R = (U-L)/2$. Let $D_i$ be the diagonal matrix with $-1$ in position $i$ and $1$ in the other diagonal positions. An inverse M-matrix is the inverse of a nonsingular M-matrix. Johnson and Smith showed that every member of $\mathcal A$ is an inverse M-matrix if and only if every vertex matrix (every member with each entry equal to $L_{ij}$ or $U_{ij}$) is, and Garloff, Al-Saafin and Adm reduced this test to at most $2^{n-1}$ vertex matrices.
Problem. For every $n \ge 1$ and all such $L$ and $U$, is every member of $\mathcal A$ an inverse M-matrix if and only if $C + sD_iRD_j$ is an inverse M-matrix for all $i, j \in \{1, \dots, n\}$ and $s \in \{-1, 1\}$?
Source: Hladík (2020), Conjecture 1; first posted as arXiv:1711.08732 (2017).
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- RA
- Keywords
- interval matrices, inverse M-matrices, OpenProblemsInNLA
References
@incollection{hladik2020,
author = {Hlad{\'\i}k, Milan},
title = {An Overview of Polynomially Computable Characteristics of Special Interval Matrices},
booktitle = {Beyond Traditional Probabilistic Data Processing Techniques: Interval, Fuzzy etc. Methods and Their Applications},
editor = {Kosheleva, Olga and Shary, Sergey P. and Xiang, Gang and Zapatrin, Roman},
series = {Stud. Comput. Intell.},
volume = {835},
publisher = {Springer},
address = {Cham},
year = {2020},
pages = {295--310},
doi = {10.1007/978-3-030-31041-7_16},
eprint = {1711.08732},
archivePrefix = {arXiv},
}
@article{johnson2002,
author = {Johnson, Charles R. and Smith, Ronald L.},
title = {Intervals of inverse {M}-matrices},
journal = {Reliab. Comput.},
volume = {8},
number = {3},
year = {2002},
pages = {239--243},
doi = {10.1023/A:1015517430475},
}
@article{garloff2021,
author = {Garloff, J{\"u}rgen and Al-Saafin, Doaa and Adm, Mohammad},
title = {Further matrix classes possessing the interval property},
journal = {Reliab. Comput.},
volume = {28},
year = {2021},
pages = {56--70},
url = {https://reliable-computing.org/reliable-computing-28-pp-056-070.pdf},
}
@misc{openproblemsinnla-iv03,
author = {Townsend, Alex},
title = {{IV-03}: Polynomial-size vertex test for inverse M-matrix intervals},
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-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_00087.
namespace RegistryProblems.OP_00087
noncomputable section
abbrev Mat (n : ℕ) := Matrix (Fin n) (Fin n) ℝ
/-- An actual nonsingular, entrywise nonnegative matrix whose inverse has
nonpositive off-diagonal entries. No regularity of a whole interval is assumed. -/
def IsInverseM {n : ℕ} (A : Mat n) : Prop :=
IsUnit A ∧ (∀ i j, 0 ≤ A i j) ∧ ∀ i j, i ≠ j → A⁻¹ i j ≤ 0
def OrderedEndpoints {n : ℕ} (L U : Mat n) : Prop := ∀ i j, L i j ≤ U i j
def intervalFamily {n : ℕ} (L U : Mat n) : Set (Mat n) :=
{A | ∀ i j, L i j ≤ A i j ∧ A i j ≤ U i j}
def center {n : ℕ} (L U : Mat n) : Mat n := fun i j => (L i j + U i j) / 2
def radius {n : ℕ} (L U : Mat n) : Mat n := fun i j => (U i j - L i j) / 2
def signVector {n : ℕ} (i : Fin n) (k : Fin n) : ℝ := if k = i then -1 else 1
/-- Entrywise expression for C+s D_i R D_j, with the exact original D_i. -/
def vertex {n : ℕ} (L U : Mat n) (s : ℝ) (i j : Fin n) : Mat n :=
fun k l => center L U k l + s * signVector i k * radius L U k l * signVector j l
/-- OP-00087: Polynomial-size vertex test for inverse M-matrix intervals -/
def _root_.RegistryProblems.Problem_OP_00087 : Prop :=
∀ n : ℕ, 1 ≤ n → ∀ L U : Mat n, OrderedEndpoints L U →
((∀ A ∈ intervalFamily L U, IsInverseM A) ↔
∀ i j : Fin n, ∀ s ∈ ({(-1 : ℝ), 1} : Set ℝ), IsInverseM (vertex L U s i j))
end
end RegistryProblems.OP_00087
Formalised by Sidney Holden (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_00087 theorem resolution : RegistryProblems.Problem_OP_00087 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00087" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00087 := 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 all-dimensional inverse-M interval characterization by n-squared negative-sign vertices, implying the full original two-sign criterion without a regularity premise.
An interval matrix $[C-R,C+R]$ consists entirely of inverse-M matrices if and only if the $n^2$ vertices $C-D_iRD_j$ are inverse-M matrices, where $D_i$ is the diagonal matrix with $-1$ in position $i$ and $1$ elsewhere. This implies the conjectured $2n^2$-vertex criterion, which also tests $C+D_iRD_j$, and shows that half of those tests are unnecessary. The proof combines induction on principal submatrices, …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, IV-03/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00087, "Polynomial-size vertex test for inverse M-matrix intervals", clopen.solutions.