Pipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Momentum and quadratic acceleration

1 · Prerequisites

2 · Logical flowchart

3 · Definitions, theorems and proofs

AlgorithmAlgorithm: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Heavy-ball momentum

Definition

Let $d \geq 1$ be an integer and let $F : R^{d} \to R$ be continuously Fréchet differentiable: at every $w$ , $D F (w)$ is a linear first-order approximation with normwise remainder tending to zero, and $w \mapsto D F (w)$ is continuous. Write its coordinate gradient as $\nabla F (w) = (\partial_{j} F (w))_{0 \leq j < d}$ . Given an initial vector $w_{i n i t} \in R^{d}$ , a constant step size $α > 0$ , a constant momentum parameter $β \geq 0$ , and an integer horizon $T \geq 1$ , initialize $w_{0} = w_{1} = w_{i n i t}$ . For each integer $t = 1, \dots, T - 1$ , set

$w_{t + 1} : = w_{t} - α \nabla F (w_{t}) + β (w_{t} - w_{t - 1}) .$

Output $(w_{0}, w_{1}, \dots, w_{T})$ . The gradient is evaluated at the current iterate $w_{t}$ . When $β = 0$ , every update is the fixed-step gradient-descent update with step size $α$ .

Definition references

Gradient descent

The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder

The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case

AlgorithmAlgorithm: Literature-sourcedProof: Not applicablejudge pass (gpt-6-luna)Open item page →

Nesterov accelerated gradient

Definition

Let $d \geq 1$ be an integer and let $F : R^{d} \to R$ be continuously Fréchet differentiable: at every $w$ , $D F (w)$ is a linear first-order approximation with normwise remainder tending to zero, and $w \mapsto D F (w)$ is continuous. Write its coordinate gradient as $\nabla F (w) = (\partial_{j} F (w))_{0 \leq j < d}$ . Given an initial vector $w_{i n i t} \in R^{d}$ , an integer horizon $T \geq 1$ , and prescribed real parameter sequences $(α_{t})_{1 \leq t < T}$ with $α_{t} > 0$ and $(β_{t})_{1 \leq t < T}$ , initialize $w_{0} = w_{1} = w_{i n i t}$ . For each integer $t = 1, \dots, T - 1$ , first set the look-ahead point

${\tilde{w}}_{t} : = w_{t} + β_{t} (w_{t} - w_{t - 1}),$

then set

$w_{t + 1} : = {\tilde{w}}_{t} - α_{t} \nabla F ({\tilde{w}}_{t}) .$

Output $(w_{0}, w_{1}, \dots, w_{T})$ . The gradient is evaluated after the look-ahead displacement. When $β_{t} = 0$ , that update is the fixed-step gradient-descent update at $w_{t}$ with step size $α_{t}$ .

Definition references

Gradient descent

The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder

The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case

TheoremStatement: Literature-sourcedProof: AI-adaptedjudge pass (gpt-6-luna)Open item page →

Tuned heavy-ball has the minimax root factor on positive-definite quadratics

Statement

Let $d \geq 1$ , let $0 < c \leq L$ , and let $A \in R^{d \times d}$ satisfy $A^{T} = A$ and $x^{T} A x > 0$ for every nonzero $x \in R^{d}$ . An eigenvalue of $A$ is a real number $λ$ such that $A v = λ v$ for some nonzero $v$ ; assume every eigenvalue lies in $[c, L]$ . For a fixed center $w^{⋆} \in R^{d}$ , define $F (w) = \frac{1}{2} (w - w^{⋆})^{T} A (w - w^{⋆})$ . Then $w^{⋆}$ is the unique minimizer of $F$ . Put $κ = L / c$ and define

$q : = \frac{\sqrt{L} - \sqrt{c}}{\sqrt{L} + \sqrt{c}} = \frac{\sqrt{κ} - 1}{\sqrt{κ} + 1} .$

Here $\nabla F (w) = (\partial_{j} F (w))_{0 \leq j < d}$ is the vector of coordinate partial derivatives.

For any constant parameters $α > 0$ and $β \geq 0$ , finite horizon $T \geq 1$ , and initial vector $w_{i n i t} \in R^{d}$ , define the heavy-ball sequence by $w_{0} = w_{1} = w_{i n i t}$ and

$w_{t + 1} = w_{t} - α \nabla F (w_{t}) + β (w_{t} - w_{t - 1}), 1 \leq t < T .$

For each scalar $λ \in [c, L]$ , the associated scalar recurrence is $x_{t + 1} = (1 + β - α λ) x_{t} - β x_{t - 1}$ . Define its characteristic polynomial and root factor by

$p_{λ} (r; α, β) : = r^{2} - (1 + β - α λ) r + β, ρ_{λ} (α, β) : = \max {∣ r ∣ : p_{λ} (r; α, β) = 0} .$

This factor is the largest modulus of the two characteristic roots in $C$ of the scalar recurrence for eigenvalue $λ$ , not a one-step Euclidean norm contraction. The tuned parameters are

$α = \frac{4}{(\sqrt{L} + \sqrt{c})^{2}}, β = q^{2} .$

For this choice, $ρ_{λ} (α, β) = q$ for every $λ \in [c, L]$ . If $c < L$ , then $p_{c} (r; α, β) = (r - q)^{2}$ and $p_{L} (r; α, β) = (r + q)^{2}$ ; if $c = L$ , the only modal polynomial is $r^{2}$ and its root factor is $0$ .

For gradient descent with step $γ = 2 / (L + c)$ , the modal multipliers are $1 - γ λ$ and their largest absolute value over $[c, L]$ is

$ρ_{G D} = \frac{L - c}{L + c} = \frac{κ - 1}{κ + 1} .$

Thus $ρ_{G D} > q$ when $c < L$ , and both factors are $0$ when $c = L$ . Moreover, among all constant heavy-ball parameters $α^{'} > 0$ and $β^{'} \geq 0$ , the supremum of their modal root factors over $λ \in [c, L]$ is at least $q$ . The tuned parameters therefore minimize that interval worst-case root factor. When $c < L$ , the repeated endpoint roots permit a linear polynomial prefactor multiplying $q^{t}$ or $(- q)^{t}$ ; the root factor does not assert a one-step norm contraction by $q$ .

Statement references

Heavy-ball momentum

Gradient descent

Matrix quadratic forms have the expected first derivative and Hessian

Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis

In an orthonormal basis, self-adjoint means conjugate-transpose symmetry and normal means commuting with the conjugate transpose

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$

The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case

In orthonormal bases, the matrix of the adjoint is the conjugate transpose of the matrix

Completeness of the real numbers

Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$

Bottou, Curtis, and Nocedal, Optimization Methods for Large-Scale Machine Learning

Chen, Lecture 9–10: Accelerated Gradient Descent

Vu, Convergence of Heavy-Ball Method and Nesterov’s Accelerated Gradient on Quadratic Optimization

Facts & Assumptions

Given: The integer $d \geq 1$ , constants $0 < c \leq L$ , a real symmetric matrix $A$ with $x^{T} A x > 0$ for nonzero $x$ and eigenvalues in $[c, L]$ , a center $w^{⋆}$ , an initial vector $w_{i n i t} \in R^{d}$ with $w_{0} = w_{1} = w_{i n i t}$ , and an arbitrary finite horizon $T \geq 1$ .

[F1]

Heavy-ball momentum: with a fixed $α > 0$ and $β \geq 0$ , the update is $w_{t + 1} = w_{t} - α \nabla F (w_{t}) + β (w_{t} - w_{t - 1})$ .

[F2]

Gradient descent: in fixed-step mode, the update is $x \mapsto x - t_{k} \nabla f (x)$ .

[F3]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : the standard inner product is $⟨ x, y ⟩ = \sum_{j < d} x_{j} y_{j}$ .

[F4]

In an orthonormal basis, self-adjoint means conjugate-transpose symmetry and normal means commuting with the conjugate transpose: in a real orthonormal basis, self-adjointness of an endomorphism is equivalent to symmetry of its matrix.

[F5]

Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis: a self-adjoint endomorphism of a finite-dimensional real inner-product space has an orthonormal eigenbasis.

[F6]

In orthonormal bases, the matrix of the adjoint is the conjugate transpose of the matrix: in orthonormal bases, a real matrix representing an adjoint is the transpose of the represented map.

[F7]

The reals are complete and Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ : with its usual order and field structure, $R$ is a complete ordered field, so every nonnegative real number has a unique nonnegative square root.

[F8]

Matrix quadratic forms have the expected first derivative and Hessian: for $ϕ (x) = \frac{1}{2} ∥ C x ∥_{2}^{2}$ , $D ϕ (x) [h] = Re ⟨ C^{*} C x, h ⟩$ , so its gradient is $C^{*} C x$ .

[F9]

The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case: for a scalar-valued function, the gradient is the vector of its coordinate partial derivatives.

Proof

1.1givenF3F4F5choose

For $0 \leq i < d$ , let $e_{i}$ be the standard coordinate vectors. By [F3], $⟨ e_{i}, e_{j} ⟩ = 1$ when $i = j$ and $0$ otherwise, so they form an orthonormal basis. Since $A^{T} = A$ , [F4] makes $x \mapsto A x$ self-adjoint; [F5] gives an orthonormal eigenbasis $u_{1}, \dots, u_{d}$ with eigenvalues $λ_{i} \in [c, L]$ . For the matrix $U$ with columns $u_{i}$ , $U^{T} U = I$ and $A = U diag (λ_{1}, \dots, λ_{d}) U^{T}$ .

1.2givenF7algebra

By [F7], write $u = \sqrt{L}$ , $v = \sqrt{c}$ , and $q = (u - v) / (u + v)$ . Set $α = 4 / (u + v)^{2}$ , $β = q^{2}$ , and $s_{λ} = 1 + q^{2} - α λ$ . Common denominators give $s_{c} = ((u + v)^{2} + (u - v)^{2} - 4 v^{2}) / (u + v)^{2} = 2 q$ and $s_{L} = ((u + v)^{2} + (u - v)^{2} - 4 u^{2}) / (u + v)^{2} = - 2 q$ ; since $s_{λ}$ is affine decreasing, $- 2 q \leq s_{λ} \leq 2 q$ on $[c, L]$ .

1.3givenalgebra

For any fixed $α^{'} > 0$ and $β^{'} \geq 0$ , the statement defines $p_{λ} (r; α^{'}, β^{'}) = r^{2} - (1 + β^{'} - α^{'} λ) r + β^{'}$ and $ρ_{λ}$ for each $λ \in [c, L]$ , whether or not $λ$ is an eigenvalue of $A$ . This interval supremum is finite: with $M = 1 + β^{'} + α^{'} L$ , every root $z$ satisfies $∣ z ∣^{2} \leq M ∣ z ∣ + β^{'}$ , hence $∣ z ∣ \leq \max {1, M + β^{'}}$ .

2.1givenF6F7step 1.1constructalgebra

By [F7], each $λ_{i} \geq c > 0$ has a positive square root. Set $C = diag (\sqrt{λ_{1}}, \dots, \sqrt{λ_{d}}) U^{T}$ . Its factors are invertible, so $C$ is invertible; [F6] gives $C^{*} = C^{T}$ , and multiplication gives $C^{*} C = U diag (λ_{1}, \dots, λ_{d}) U^{T} = A$ .

2.2givenF7step 1.2algebracases

For $c < L$ , we have $q > 0$ and step 1.2 gives $∣ s_{λ} ∣ < 2 q$ for $c < λ < L$ . The roots of $p_{λ}$ are $(s_{λ} \pm i \sqrt{4 q^{2} - s_{λ}^{2}}) / 2$ , whose squared modulus is $q^{2}$ ; at $c$ and $L$ the polynomials are $(r - q)^{2}$ and $(r + q)^{2}$ . If $c = L$ , then $q = 0$ , $α = 1 / c$ , $β = 0$ , and the only polynomial is $p_{c} (r) = r^{2}$ . Thus every tuned modal root factor is $q$ .

2.3givenstep 1.2step 1.3assume-casealgebra

Assume $c < L$ and fix arbitrary $α^{'} > 0$ , $β^{'} \geq 0$ . Let $R = \sup_{λ \in [c, L]} ρ_{λ} (α^{'}, β^{'})$ , finite by step 1.3. If $R \geq 1$ , then $R > q$ by step 1.2; if $R = 0$ , the endpoint polynomials force $β^{'} = 0$ and $α^{'} c = α^{'} L = 1$ , impossible since $c < L$ , so in the remaining case $0 < R < 1$ . The endpoint root products give $0 \leq β^{'} \leq R^{2}$ . For real endpoint roots in $[- R, R]$ , $p_{c} (R) = (R - r_{1}) (R - r_{2}) \geq 0$ and $p_{L} (- R) = (- R - r_{1}) (- R - r_{2}) \geq 0$ ; for conjugate roots these values are squared moduli.

3.1givenF8F9step 2.1algebra

The objective is $F (w) = ϕ (w - w^{⋆})$ for $ϕ (x) = \frac{1}{2} ∥ C x ∥_{2}^{2}$ . Applying [F8] to each increment $h$ gives $D F (w) [h] = Re ⟨ C^{*} C (w - w^{⋆}), h ⟩$ , so [F9] yields $\nabla F (w) = C^{*} C (w - w^{⋆}) = A (w - w^{⋆})$ . Since $C$ is invertible, $F (w) = \frac{1}{2} ∥ C (w - w^{⋆}) ∥_{2}^{2} \geq 0$ with equality exactly at $w = w^{⋆}$ , proving unique minimization.

3.2givenstep 2.2constructalgebra

For $c < L$ , at either endpoint the scalar recurrence has polynomial $(z - r)^{2}$ with $r = q$ or $r = - q$ , so $r \neq 0$ . For arbitrary real $a, b$ , substitution shows $x_{t} = (a + b t) r^{t}$ satisfies $x_{t + 1} - 2 r x_{t} + r^{2} x_{t - 1} = r^{t + 1} ((a + b (t + 1)) - 2 (a + b t) + (a + b (t - 1))) = 0$ ; choosing $a = x_{0}$ and $b = x_{1} / r - x_{0}$ matches any initial pair. Thus a repeated endpoint mode can contain $t r^{t}$ , which explains why the root factor alone is not a one-step norm contraction.

3.3givenF7step 2.3algebra

In the case $0 < R < 1$ of [2.3], expanding its endpoint inequalities gives $α^{'} c \geq (1 - R) (R - β^{'}) / R$ and $α^{'} L \leq (1 + R) (R + β^{'}) / R$ . Since $β^{'} \leq R^{2} < R$ , the first right-hand side is positive, so division yields $κ = L / c \leq (1 + R) (R + β^{'}) / ((1 - R) (R - β^{'}))$ . Also $(1 + R) (R - β^{'}) - (1 - R) (R + β^{'}) = 2 (R^{2} - β^{'}) \geq 0$ , hence $(R + β^{'}) / (R - β^{'}) \leq (1 + R) / (1 - R)$ and $κ \leq ((1 + R) / (1 - R))^{2}$ . By [F7], taking positive square roots and rearranging gives $R \geq (\sqrt{κ} - 1) / (\sqrt{κ} + 1) = q$ ; together with the $R \geq 1$ case, every admissible pair has $R \geq q$ .

4.1givenF1step 1.1step 3.1algebra

Let $e_{t} = w_{t} - w^{⋆}$ and $x_{i, t} = u_{i}^{T} e_{t}$ . By [F1] and step 3.1, $e_{t + 1} = (1 + β) e_{t} - α A e_{t} - β e_{t - 1}$ for $1 \leq t < T$ . Since $A u_{i} = λ_{i} u_{i}$ and $A^{T} = A$ , projection onto $u_{i}$ gives $x_{i, t + 1} = (1 + β - α λ_{i}) x_{i, t} - β x_{i, t - 1}$ , whose characteristic polynomial is $p_{λ_{i}} (r; α, β)$ .

4.2givenF2step 3.1algebra

For gradient descent with $γ = 2 / (L + c)$ , [F2] and step 3.1 give the scalar update $x_{i, t + 1} = (1 - γ λ_{i}) x_{i, t}$ . The affine multiplier decreases from $(L - c) / (L + c)$ at $c$ to $- (L - c) / (L + c)$ at $L$ , so its largest absolute value on $[c, L]$ is $ρ_{G D} = (L - c) / (L + c)$ .

5.1givenF7step 2.2step 4.2algebra

Put $s = \sqrt{κ}$ . By step 4.2, $ρ_{G D} = (κ - 1) / (κ + 1) = (s^{2} - 1) / (s^{2} + 1)$ , while $q = (s - 1) / (s + 1)$ by its definition. If $s > 1$ , subtraction gives $ρ_{G D} - q = 2 s (s - 1) / ((s^{2} + 1) (s + 1)) > 0$ ; if $s = 1$ , both factors are zero. This proves the claimed gradient-descent comparison.

6.1givenstep 2.2step 3.2step 3.3step 5.1algebra∎

If $c = L$ , step 2.2 gives tuned root factor $q = 0$ , which is minimal since root factors are nonnegative. If $c < L$ , step 2.2 gives tuned interval factor $q$ and step 3.3 gives the lower bound $R \geq q$ for every constant admissible pair, so the tuned parameters are minimax; step 5.1 gives the strict comparison with gradient descent, while step 3.2 records the repeated-root qualification.

4 · Examples, counterexamples and false statements

None yet.

Momentum and quadratic acceleration

2 · Logical flowchart

3 · Definitions, theorems and proofs

Heavy-ball momentum

Definition

Definition references

Nesterov accelerated gradient

Definition

Definition references

Tuned heavy-ball has the minimax root factor on positive-definite quadratics

Statement

Statement references

Facts & Assumptions

Proof

4 · Examples, counterexamples and false statements

Sources