ExampleConstruction: Literature-sourcedVerification: AI-generatedPipeline-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.

A strict saddle of a quadratic Stiefel objective

Example

For $A = diag (0, 1, 2)$ , minimize $f (x) = x^{T} A x$ on $St (3, 1) = S^{2}$ . The point $e_{2}$ is critical, but one unit-speed tangent curve decreases $f$ and another increases it. Thus it is a strict saddle, not a local minimum.

Facts & Assumptions

Given: The unit sphere, the symmetric matrix $A$ and the objective in the Example.

[F1]

The Riemannian gradient of a smooth ambient objective is its Euclidean gradient projected onto the Stiefel tangent (Projected Euclidean gradients are the Stiefel and Grassmann gradients).

[F2]

At a unit frame $x$ , the tangent space is ${z : x^{T} z = 0}$ (Tangent spaces and Frobenius projections on Stiefel and Grassmann).

Proof

technique · compute the projected gradient and the objective along two feasible curves

1.1F1givenalgebra

The ambient gradient is $\nabla f (x) = 2 A x$ , so $\nabla f (e_{2}) = 2 e_{2}$ . Its Stiefel projection is $2 e_{2} - e_{2} (e_{2}^{T} 2 e_{2}) = 0$ by [F1]; hence $e_{2}$ is critical.

2.1F2givenalgebra∎

Both $e_{1}$ and $e_{3}$ are tangent at $e_{2}$ by [F2]. The curves $x_{-} (t) = \cos (t) e_{2} + \sin (t) e_{1}$ and $x_{+} (t) = \cos (t) e_{2} + \sin (t) e_{3}$ stay on the unit sphere and have initial velocities $e_{1}, e_{3}$ . Their objective values are $f (x_{-} (t)) = \cos^{2} t < 1$ and $f (x_{+} (t)) = \cos^{2} t + 2 \sin^{2} t = 1 + \sin^{2} t > 1$ for all sufficiently small nonzero $t$ . Thus arbitrarily nearby feasible points have smaller and larger values, proving strict saddle behavior.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

11 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 3 (2008) (standard reference, not scraped)
Nicolas Boumal, An Introduction to Optimization on Smooth Manifolds (2023 prepublication) (standard reference, not scraped)