A sharp subset bound for worst-case normal GMRES
For a finite nonempty set $S \subset \mathbb{C} \setminus \{0\}$ and $k \ge 1$ let $$M_k(S) = \min_{p \in \mathbb{C}[z],\ \deg p \le k,\ p(0) = 1} \ \max_{z \in S} |p(z)|.$$ For a normal matrix with spectrum $L$, $M_k(L)$ is the largest relative residual norm that GMRES can have at step $k$. When $|S| = k + 1$, $M_k(S) = \bigl(\sum_{z \in S} |\ell_z(0)|\bigr)^{-1}$, where the $\ell_z$ are the Lagrange basis polynomials of $S$. One has $M_k(L) \ge \max_{S \subseteq L,\ |S| = k+1} M_k(S)$, with equality when all points of $L$ are real (a classical result of approximation theory; see Liesen and Tichý), and Liesen and Tichý showed that the constant $4/\pi$ below cannot be replaced by a smaller one.
Problem. Is $$M_k(L) \le \frac{4}{\pi} \max_{S \subseteq L,\ |S| = k+1} M_k(S)$$ for every set $L \subset \mathbb{C} \setminus \{0\}$ of $n \ge 3$ distinct points and every $1 \le k \le n - 2$?
Source: Liesen and Tichý (2004), conjecture (3.16) with the constant C = 4/π of their Section 4.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Secondary
- CA
- Keywords
- GMRES, normal matrices, OpenProblemsInNLA, polynomial approximation
References
@article{liesen2004,
author = {Liesen, J{\"o}rg and Tich{\'y}, Petr},
title = {The worst-case {GMRES} for normal matrices},
journal = {BIT Numer. Math.},
volume = {44},
number = {1},
year = {2004},
pages = {79--98},
doi = {10.1023/B:BITN.0000025083.59864.bd},
}
@misc{openproblemsinnla-ie16,
author = {Townsend, Alex},
title = {{IE-16}: A sharp subset bound for worst-case normal GMRES},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/linear-systems-and-elimination/IE-16/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00080.
namespace RegistryProblems.OP_00080
noncomputable section
open scoped BigOperators Classical
abbrev Poly := Polynomial ℂ
/- The finite maximum is totalized at the empty set. All occurrences in the
canonical target have nonempty sets, since k >= 1 and |L| >= 3. -/
def maxModulus (L : Finset ℂ) (p : Poly) : ℝ :=
if hL : L.Nonempty then L.sup' hL (fun z => ‖p.eval z‖) else 0
def feasible (L : Finset ℂ) (k : ℕ) (p : Poly) : Prop :=
p.natDegree ≤ k ∧ p.eval 0 = 1
def feasibleValues (L : Finset ℂ) (k : ℕ) : Set ℝ :=
{r | ∃ p : Poly, feasible L k p ∧ maxModulus L p = r}
/- This is exactly M_k(L), with the finite maximum above and the infimum over
all complex polynomials of degree at most k normalized by p(0)=1. -/
def M (L : Finset ℂ) (k : ℕ) : ℝ := sInf (feasibleValues L k)
def subsetFamily (L : Finset ℂ) (k : ℕ) : Finset (Finset ℂ) :=
L.powerset.filter (fun S => S.card = k + 1)
/- This is B_k(L) = max_{S subset L, |S|=k+1} M_k(S). The empty-family
branch is irrelevant under the canonical admissibility hypotheses. -/
def subsetMax (L : Finset ℂ) (k : ℕ) : ℝ :=
if hS : (subsetFamily L k).Nonempty then
(subsetFamily L k).sup' hS (fun S => M S k)
else 0
def admissible (L : Finset ℂ) (n : ℕ) : Prop :=
L.card = n ∧ ∀ z ∈ L, z ≠ 0
/-- OP-00080: A sharp subset bound for worst-case normal GMRES -/
def _root_.RegistryProblems.Problem_OP_00080 : Prop :=
∀ n : ℕ, 3 ≤ n → ∀ L : Finset ℂ, admissible L n →
∀ k : ℕ, 1 ≤ k → k ≤ n - 2 →
M L k ≤ (4 / Real.pi) * subsetMax L k
end
end RegistryProblems.OP_00080
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_00080 theorem resolution : RegistryProblems.Problem_OP_00080 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00080" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00080 := 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 resolution of the original IE-16 universal inequality from Sidney Holden’s exact nine-point, degree-four counterexample. All fifteen independently reviewed contracts passed actual non-root Linux Comparator, standard axiom checks and default-kernel replay.
The conjectured $4/\pi$ subset bound is false. Let $\omega=e^{2\pi i/3}$ and $L=\{\omega^a+10^{-3}\omega^b:0\le a,b\le2\}$. At degree $k=4$, this nine-point set satisfies $M_4(L)/\max_{S\subset L,\ |S|=5}M_4(S)>13/10>4/\pi$. The proof is analytic and covers every subset by its cluster occupancy. An additional exact-arithmetic certificate checks all 126 subsets and proves optimality of the full-set polynomial by positive weighted orthogonality. The actual ratio is approximately $1.33299891979475829424$. …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, IE-16/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00080, "A sharp subset bound for worst-case normal GMRES", clopen.solutions.