The exact four-step amplification of restarted Anderson acceleration
Let $n \ge 2$ and let $M \in \mathbb{R}^{n \times n}$ be nonzero and symmetric, with eigenvalues $m_1, \dots, m_n$, none equal to $1$; put $A = I - M$. Two steps of restarted Anderson acceleration with memory one, applied to $x = Mx + b$, propagate the residual by the positively homogeneous map $$R(v) = M\Bigl(v - \frac{v^TAv}{\|Av\|_2^2}\,Av\Bigr) \quad (v \ne 0), \qquad R(0) = 0.$$ In the maximum over $i \ne j$ below, a term with zero denominator is $0$; under these assumptions that happens only when $m_i = m_j = 0$. Krzysik, De Sterck and Smith showed that if $v \ne 0$ is a combination of two orthogonal eigenvectors of $M$, with eigenvalues $m_i \ne m_j$, then $R(R(v))$ is a multiple of $v$, and that the largest such multiple is the $(i, j)$ term on the right below. For $n = 2$ the identity therefore holds.
Problem. Is $$\max_{v \ne 0} \frac{\|R(R(v))\|_2}{\|v\|_2} = \max_{i \ne j} \left(\frac{m_i m_j (m_j - m_i)}{|m_i(m_i - 1)| + |m_j(m_j - 1)|}\right)^2$$ for every such $n$ and $M$?
Source: Krzysik, De Sterck and Smith (2025), Conjecture 10, stated there through two-eigenvector nonlinear eigenvalues; in this form, OpenProblemsInNLA.
Imported from github.com/ajt60gaibb/OpenProblemsInNLA.
Classification
- Primary
- NA — Numerical Analysis
- Keywords
- Anderson acceleration, convergence factors, fixed-point iterations, OpenProblemsInNLA
References
@article{krzysik2025,
author = {Krzysik, Oliver A. and De Sterck, Hans and Smith, Adam},
title = {Asymptotic convergence of restarted {A}nderson acceleration for certain normal linear systems},
journal = {SIAM J. Sci. Comput.},
volume = {47},
year = {2025},
pages = {S135--S160},
doi = {10.1137/24M1672262},
eprint = {2312.04776},
archivePrefix = {arXiv},
}
@misc{openproblemsinnla-ie18,
author = {Townsend, Alex},
title = {{IE-18}: The exact four-step amplification of restarted Anderson acceleration},
howpublished = {Open Problems in Numerical Linear Algebra, GitHub repository},
year = {2026},
url = {https://github.com/ajt60gaibb/OpenProblemsInNLA/blob/main/linear-systems-and-elimination/IE-18/README.md},
note = {Read at commit e375a6f, 2026-09-30},
}
Canonical Lean statement
A submission resolves this problem by proving the constant Problem_OP_00082.
namespace RegistryProblems.OP_00082
noncomputable section
open scoped BigOperators NNReal Classical
/-- The sum of coordinate squares, rather than the default norm on a Pi type. -/
def squaredNorm {n : ℕ} (v : Fin n → ℝ) : ℝ := ∑ i : Fin n, v i ^ 2
/-- The actual Euclidean norm of a real coordinate vector. -/
def euclideanNorm {n : ℕ} (v : Fin n → ℝ) : ℝ := Real.sqrt (squaredNorm v)
/-- The scalar coefficient in the canonical residual map, using `A=I-M`.
At zero it is totalized by real division; `residualMap` handles zero explicitly. -/
def residualCoefficient {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ)
(v : Fin n → ℝ) : ℝ :=
dotProduct v ((1 - M).mulVec v) / squaredNorm ((1 - M).mulVec v)
/-- Two original Anderson steps. The canonical map explicitly sends zero to zero. -/
def residualMap {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ)
(v : Fin n → ℝ) : Fin n → ℝ :=
if v = 0 then 0
else M.mulVec (v - residualCoefficient M v • (1 - M).mulVec v)
/-- Four original Anderson steps, namely two applications of the residual map. -/
def fourStepResidual {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ)
(v : Fin n → ℝ) : Fin n → ℝ := residualMap M (residualMap M v)
/-- The unsquared Euclidean norm amplification appearing in IE-18. -/
def amplification {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ)
(v : Fin n → ℝ) : ℝ :=
euclideanNorm (fourStepResidual M v) / euclideanNorm v
/-- Actual amplifications at every nonzero vector, with no default maximum. -/
def amplificationSet {n : ℕ} (M : Matrix (Fin n) (Fin n) ℝ) : Set ℝ :=
{r | ∃ v : Fin n → ℝ, v ≠ 0 ∧ r = amplification M v}
/-- The pairwise quotient. Real division gives zero if the denominator is zero,
which implements the canonical zero-denominator convention. -/
def pairQuotient (a b : ℝ) : ℝ :=
a * b * (b - a) / (|a * (a - 1)| + |b * (b - 1)|)
/-- The maximum over distinct eigenvalue indices, retaining multiplicity.
The NNReal square equals the real square in `pairValue`; its finite supremum
is a true maximum for `n≥2`. The empty-index convention is outside that domain. -/
def pairListMaximum {n : ℕ} (μ : Fin n → ℝ) : ℝ :=
(((Finset.univ : Finset (Fin n × Fin n)).filter (fun ij => ij.1 ≠ ij.2)).sup
(fun ij => ‖pairQuotient (μ ij.1) (μ ij.2)‖₊ ^ 2) : ℝ≥0)
/-- The proposed factor using Mathlib's actual full eigenvalue list.
No user-supplied spectral certificate or diagonalization is assumed. -/
def pairMaximum {n : ℕ} {M : Matrix (Fin n) (Fin n) ℝ}
(hM : M.IsHermitian) : ℝ := pairListMaximum hM.eigenvalues
/-- OP-00082: The exact four-step amplification of restarted Anderson acceleration -/
def _root_.RegistryProblems.Problem_OP_00082 : Prop :=
∀ n : ℕ, 2 ≤ n → ∀ M : Matrix (Fin n) (Fin n) ℝ, M ≠ 0 →
∀ hM : M.IsHermitian, (1 : ℝ) ∉ spectrum ℝ M →
IsGreatest (amplificationSet M) (pairMaximum hM)
end
end RegistryProblems.OP_00082
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_00082 theorem resolution : RegistryProblems.Problem_OP_00082 := by sorry
In preprint.toml, mapping the claim to the declaration that establishes it:
[[statements]] label = "Theorem 1" lean = "resolution" latex = "..." problem = "OP-00082" claim = "full"
To disprove it instead, prove the negation and claim "disproof", or "counterexample" if the proof exhibits one:
theorem disproof : ¬ RegistryProblems.Problem_OP_00082 := 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
Derives the actual two residual-map executions and the maximum over the genuine Hermitian eigenvalue list, then refutes the complete original universal maximum identity by an admissible strict counterexample.
Exact diagonal examples refute a conjectured pairwise formula for four-step residual amplification in restarted Anderson acceleration. With $A=I-M$, $\alpha(v)=v^TAv/v^TA^2v$ and $R(v)=M[I-\alpha(v)A]v$, the residual after four steps is $R(R(v))$. For $M=\mathrm{diag}(1/10,1/2,3/5)$, where both $M$ and $I-M$ are positive definite, and $v=(1,1,1)^T$, exact rational substitution gives $\|R(R(v))\|_2^2/\|v\|_2^2=1920682/21289638243>1/14641$, the square of the conjectured maximum $1/121$. A positive-definite one-parameter family gives an unbounded ratio …
In this work, we analyze the asymptotic convergence factor of minimal residual iteration (MRI) (or GMRES(1)) for solving linear systems $Ax=b$ based on vector-dependent nonlinear eigenvalue problems. The worst-case root-convergence factor is derived for linear systems with $A$ being symmetric or $I-A$ being skew-symmetric. When $A$ is symmetric, the asymptotic convergence factor highly depends on the initial guess. While $M=I-A$ …
Status history
| When | Change | By | Reason |
|---|---|---|---|
| 2026-10-05 | Needs verification → Lean verified | — | Verified here: OpenProblemsInNLA @ e375a6f, IE-18/lean/. |
Citing this problem
This identifier is permanent. It will not change if the problem is solved, reclassified or withdrawn.
OP-00082, "The exact four-step amplification of restarted Anderson acceleration", clopen.solutions.