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.

Uniform pullback smoothness guarantees an Armijo step

Statement

Let $M = St (n, r)$ or $Gr (r, n)$ be compact, let $f : M \to R$ be smooth, and let $R$ be a QR or polar retraction with the first-order property of The QR and polar maps are first-order Stiefel and Grassmann retractions. Write ${\hat{f}}_{x} (η) = f (R_{x} (η))$ . Assume a uniform bound $∥ grad f (x) ∥ \leq G$ and a constant $L_{R} \geq 0$ such that, for every $x$ and $∥ η ∥ \leq 1$ , $∥ grad {\hat{f}}_{x} (η) - grad {\hat{f}}_{x} (0) ∥ \leq L_{R} ∥ η ∥ .$ For $a \in (0, 1)$ and a nonstationary iterate, set $δ = \min {1, (2 G)^{- 1}, 2 (1 - a) / L_{R}},$ where a reciprocal of zero is interpreted as $+ \infty$ . If the finite backtracking budget tests some $t_{j} = β^{j} \leq δ$ , then it accepts a step; the first accepted step obeys $t \geq β δ$ . For $0 < t \leq δ$ , the bound $t ∥ grad f (x) ∥ \leq 1 / 2$ keeps the pullback argument inside its assumed unit tangent ball; an earlier accepted trial may be larger.

Facts & Assumptions

Given: The compact manifold, smooth objective, first-order retraction, constants $G, L_{R}, a, β$ , and finite budget reaching $δ$ .

[F1]

The retraction pullback has derivative at zero equal to the original tangent direction (The QR and polar maps are first-order Stiefel and Grassmann retractions).

[F2]

The Riemannian gradient represents the differential in the chosen metric (The Riemannian gradient is the metric dual of the differential).

[F3]

The finite Armijo search tests $t_{j} = β^{j}$ and accepts only the sufficient-decrease inequality (Finite-budget retraction Armijo backtracking).

[F4]

The Euclidean inner product obeys Cauchy–Schwarz (Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation).

Proof

technique · integrate the Lipschitz pullback-gradient bound along the negative-gradient segment

1.1givenalgebra

Since $g \neq 0$ and $∥ g ∥ \leq G$ , we have $G > 0$ . For $0 < t \leq δ$ , $η = - t g$ has norm $t ∥ g ∥ \leq t G \leq 1 / 2$ , so the entire segment $s η$ , $0 \leq s \leq 1$ , lies in the unit ball.

2.1F1F2F3F4givenstep 1.1algebra

By [F1] and [F2], $D {\hat{f}}_{x} (0) [η] = ⟨ g, η ⟩ = - t ∥ g ∥^{2}$ . The fundamental theorem of calculus along $s \mapsto s η$ and the assumed Lipschitz bound give ${\hat{f}}_{x} (η) \leq f (x) - t ∥ g ∥^{2} + \int_{0}^{1} L_{R} s ∥ η ∥^{2} d s = f (x) - t ∥ g ∥^{2} + \frac{1}{2} L_{R} t^{2} ∥ g ∥^{2} .$ The integral bound uses [F4] to estimate the inner product of the gradient difference with $η$ . If $L_{R} = 0$ the last error is zero; otherwise $t \leq 2 (1 - a) / L_{R}$ makes the right side at most $f (x) - a t ∥ g ∥^{2}$ . Thus every tested $t \leq δ$ satisfies the Armijo test in [F3].

3.1F3givenstep 2.1algebra∎

Let $j$ be the first tested index with $β^{j} \leq δ$ . By step 2.1 this trial passes, so the algorithm stops no later than $j$ . If $j = 0$ , then $t = 1 \geq β δ$ because $δ \leq 1$ . If $j > 0$ , minimality gives $β^{j - 1} > δ$ , hence $β^{j} > β δ$ . Any earlier accepted grid point is larger still.

Depends on

Used by

Retraction Armijo reaches an epsilon-gradient iterate in finite budget Theorem

Dependency tree · two levels

25 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)