TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generatedjudge pass (gpt-6-luna)

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.

Retraction Armijo reaches an epsilon-gradient iterate in finite budget

Statement

Under the hypotheses of Uniform pullback smoothness guarantees an Armijo step, assume $f$ is bounded below by $f_{\inf}$ and every nonstationary call's finite budget reaches the stated $δ$ . For $N \geq 1$ accepted updates $x_{0}, \dots, x_{N}$ , $\min_{0 \leq k < N} ∥ grad f (x_{k}) ∥^{2} \leq \frac{f (x_{0}) - f_{\inf}}{a β δ N} .$ In particular, for every $ϵ > 0$ , after more than $(f (x_{0}) - f_{\inf}) / (a β δ ϵ^{2})$ accepted updates, some iterate among the pre-update points has gradient norm at most $ϵ$ . The order is $O (ϵ^{- 2})$ with the displayed constants fixed. This counts accepted updates; it does not assert an evaluation bound independent of the finite backtracking budgets.

Facts & Assumptions

Given: The Armijo acceptance and step bound, lower bound $f_{\inf}$ , constants $a, β, δ > 0$ , and $N$ accepted updates.

[F1]

Every nonstationary call accepts a step $t_{k} \geq β δ$ (Uniform pullback smoothness guarantees an Armijo step).

[F2]

An accepted Armijo update satisfies $f (x_{k + 1}) \leq f (x_{k}) - a t_{k} ∥ grad f (x_{k}) ∥^{2}$ (Finite-budget retraction Armijo backtracking).

Proof

technique · telescope the sufficient decreases

1.1F1F2givenalgebra

For every accepted update, [F1] and [F2] imply $f (x_{k}) - f (x_{k + 1}) \geq a β δ ∥ grad f (x_{k}) ∥^{2}$ . Summing for $k = 0, \dots, N - 1$ telescopes to $a β δ \sum_{k = 0}^{N - 1} ∥ grad f (x_{k}) ∥^{2} \leq f (x_{0}) - f (x_{N}) \leq f (x_{0}) - f_{\inf} .$ At least one of the $N$ nonnegative terms is no greater than their average, giving the stated bound.

2.1step 1.1givencontradiction∎

If every pre-update gradient norm were greater than $ϵ$ , the sum in step 1.1 would exceed $N ϵ^{2}$ . This contradicts its upper bound whenever $N > (f (x_{0}) - f_{\inf}) / (a β δ ϵ^{2})$ , proving the finite accepted-update claim.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

P.-A. Absil, R. Mahony, and R. Sepulchre, Optimization Algorithms on Matrix Manifolds, Chapter 4 (2008) (standard reference, not scraped)
Nicolas Boumal, An Introduction to Optimization on Smooth Manifolds (2023 prepublication) (standard reference, not scraped)
Nicolas Boumal, P.-A. Absil, and Coralia Cartis, Global rates of convergence for nonconvex optimization on manifolds (2018), arXiv v2 (standard reference, not scraped)