TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-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.

Armijo gradient descent has an explicit global linear rate

Statement

Let $U \subseteq R^{d}$ be open and convex, and let $f \in C^{2} (U, R)$ have an attained global minimum $f^{*} = f (x^{*})$ at $x^{*} \in U$ . Fix $x_{0} \in U$ and suppose $K : = {y \in U : f (y) \leq f (x_{0})}$ is compact. Let $V \subseteq U$ be convex and open, contain $K$ and every backtracking trial segment under consideration, and satisfy

$m I ⪯ H_{f} (y) ⪯ M I (y \in V)$

for $0 < m \leq M$ . Run Gradient descent in backtracking mode with Armijo parameter $a \in (0, 1 / 2)$ and shrink factor $b \in (0, 1)$ . For every accepted update at a nonstationary iterate $x_{k}$ , the accepted step satisfies

$t_{k} \geq τ : = \min {1, \frac{2 b (1 - a)}{M}},$

and

$f (x_{k + 1}) - f^{*} \leq (1 - 2 a m τ) (f (x_{k}) - f^{*}) .$

Consequently, for every generated $k \geq 1$ ,

$f (x_{k}) - f^{*} \leq (1 - 2 a m τ)^{k} (f (x_{0}) - f^{*}) .$

The factor lies in $(0, 1)$ . If the algorithm's caller-stop predicate fires, no later iterate is asserted. These are objective-gap bounds, not iterate-error bounds.

Facts & Assumptions

Given: The hypotheses of the Statement and a generated nonstationary iterate $x \in K$ whose backtracking line search is reached.

[F1]

Gradient descent: in backtracking mode it uses $p = - \nabla f (x)$ , starts at $t = 1$ , repeatedly multiplies a rejected step by its factor in $(0, 1)$ , and accepts the Armijo inequality.

[F2]

Armijo backtracking terminates for strict descent directions: on an open domain, a differentiable objective and a strict descent direction make this backtracking loop accept after finitely many reductions.

[F3]

For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ : if $0 < b < 1$ , then $b^{j} \to 0$ as $j \to \infty$ .

[F4]

A Hessian lower bound gives strong convexity and gradient-gap bounds: the Hessian lower bound implies $∥ \nabla f (x) ∥_{2}^{2} \geq 2 m (f (x) - f^{*})$ on the convex neighborhood containing $x$ and $x^{*}$ .

[F5]

Multivariable Taylor formula with a Lagrange remainder along a line segment: a $C^{2}$ function on a segment has its second-order Taylor remainder given by a Hessian quadratic form at an interior point of that segment.

[F6]

The Hessian matrix and critical points of a scalar field and The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case: the Hessian is the matrix of second partial derivatives and the gradient is the vector of first partial derivatives.

Proof

1.1F1F2F3F6givenchoose

At a nonstationary iterate, $g : = \nabla f (x) \neq 0$ , so [F1] uses the strict descent direction $p = - g$ and [F2] guarantees finite acceptance. Let $T : = 2 (1 - a) / M$ . If $T \geq 1$ , the initial trial $t = 1$ satisfies $t \leq T$ . If $T < 1$ , [F3] gives an index $j$ with $b^{j} \leq T$ ; choose the least such $j$ , so $b^{j - 1} > T$ and $b^{j} > b T$ .

2.1F1F5step 1.1algebra

For any trial $0 < t \leq T$ on the assumed segment, [F5] and $H_{f} ⪯ M I$ give $f (x - t g) \leq f (x) - t ∥ g ∥_{2}^{2} + (M / 2) t^{2} ∥ g ∥_{2}^{2} \leq f (x) - a t ∥ g ∥_{2}^{2}$ . Thus the initial trial is accepted when $T \geq 1$ ; when $T < 1$ , the candidate $b^{j}$ from step 1.1 passes, so the actual accepted step is at least $b^{j} > b T$ . Both cases give $t_{k} \geq \min {1, b T} = τ$ .

3.1F1F4step 2.1givenalgebra

Armijo acceptance and step 2.1 imply $f (x_{k + 1}) \leq f (x_{k}) - a τ ∥ \nabla f (x_{k}) ∥_{2}^{2}$ . Apply [F4] to obtain $f (x_{k + 1}) - f^{*} \leq (1 - 2 a m τ) (f (x_{k}) - f^{*})$ . The factor is positive because $τ \leq 2 b (1 - a) / M$ gives $2 a m τ \leq 4 a b (1 - a) m / M < 1$ , and it is below one because $a, m, τ > 0$ .

4.1F1step 3.1givenalgebradischarge-induction∎

Every accepted step decreases $f$ , so all generated iterates remain in $K$ . Repeatedly apply step 3.1 along the generated updates; induction gives the asserted $k$ -step bound, and a stopping status creates no later iterate.

Depends on

Used by

Exact and Armijo rates on an anisotropic quadratic Example

Dependency tree · two levels

40 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

Stephen Boyd and Lieven Vandenberghe, Convex Optimization (standard reference, not scraped)
Philip E. Gill and Margaret H. Wright, Math 171B Numerical Optimization Class Notes (standard reference, not scraped)