← All papers
First page of Exact (Non-)Accelerations of Heavy-Ball Discretizations

Exact (Non-)Accelerations of Heavy-Ball Discretizations

Dmitry Pasechnyuk-Vilensky, Martin Takáč

math.OC Nov 10, 2026 · v1 math.NA
The authors state that the article's mathematical results on heavy-ball momentum convergence rates have formal proofs in Lean.
Momentum methods with the same slow dynamics can have different worst-case rates on smooth strongly convex functions. We identify a half-step phase barrier in the gradient query that governs this difference. For momentum with extrapolation $τ_κ\toτ$, $β=1-θ/\sqrtκ+o(κ^{-1/2})$ and $hL\to y$, where $κ=L/μ$ and $θ,y>0$, the exact uniform distance factor is $1-c/\sqrtκ+o(κ^{-1/2})$, with $c=\min\{θ/3,c_Q(θ,y)\}$, when $τ>1/2$ and $y(1+2τ)<4$; $c_Q$ is the slowest quadratic decay exponent. Quadratically accelerated families with $\limsupτ_κ<1/2$ have divergent trajectories on the full function class. Upper bounds use finite-lag certificates: nonnegative combinations of inequalities for values and gradients at finitely separated query points, together with comparisons to the minimizer. For any prescribed accuracy, spiral mixtures or quadratic trajectories of one finite-dimensional objective give matching lower bounds at all iteration horizons. We resolve the parameter layer near $τ=1/2$ and classify all tunings of this family attaining the optimal leading constant 1. The flow also bounds the leading constant of every second-order stationary linear family with the same slow parameters $(θ,y)$ and fixed finite memory.

Momentum methods that share the same continuous-time heavy-ball limit can have different worst-case rates on smooth strongly convex functions. The goal is to find the exact leading rate constant for accelerated tunings of the extrapolated heavy-ball family and to explain when acceleration holds on the full function class.

The heavy-ball flow is analyzed with a Lyapunov identity to get its exact worst decay exponent min{θ/3, c_Q}. Upper bounds for discrete methods come from finite-lag certificates, which are nonnegative combinations of interpolation inequalities, analyzed through a spectral closure for stationary linear methods. Matching lower bounds come from spiral mixtures or quadratic trajectories of a single finite-dimensional objective, using Azagra–Mudarra C^{1,1} extension. The results are stated to be formally proved in Lean.

The exact uniform distance factor is 1 − c/√κ with c = min{θ/3, c_Q(θ,y)} when τ > 1/2 and y(1+2τ) < 4. Families with limsup τ < 1/2 diverge on the full class, which identifies a half-step wall at τ = 1/2. The paper also classifies all tunings that attain the optimal constant 1, as triple momentum does, and gives exact convergence thresholds at finite condition numbers.