ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck passjudge 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.

A gradient-descent path can be bounded below when the objective is not

Example

Let $F (x, y) = x^{2} - y^{2}$ on $R^{2}$ , start gradient descent at $w_{0} = (1, 0)$ , and use the fixed step $α = 1 / 4$ . The gradient is $(2 x, - 2 y)$ and is globally $2$ -Lipschitz. The iterates are $w_{t} = (2^{- t}, 0)$ , so $F (w_{t}) = 4^{- t} \geq 0$ and $w_{t} \to (0, 0)$ , even though $F$ is unbounded below on $R^{2}$ . The limit is stationary but is neither a local minimum nor a local maximum.

Facts & Assumptions

Given: $F (x, y) = x^{2} - y^{2}$ , $w_{0} = (1, 0)$ , and fixed step $α = 1 / 4$ .

[F1]

The total (Fréchet) derivative $D f (a)$ as the linear first-order approximation with $o (∥ h ∥_{2})$ remainder: a derivative is a linear map whose remainder is at most $ε ∥ h ∥_{2}$ for all sufficiently small increments, for every $ε > 0$ .

[F2]

Directional derivatives and partial derivatives of a map $U \subseteq R^{m} \to R^{n}$ : a coordinate partial derivative is the limit of the difference quotient in that coordinate direction.

[F3]

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

[F4]

The Euclidean inner product $⟨ x, y ⟩ = \sum_{k < n} x_{k} y_{k}$ on $R^{n}$ : $∥ (u, v) ∥_{2}^{2} = u^{2} + v^{2}$ on $R^{2}$ .

[F5]

Gradient descent: in fixed-step mode the update is $w_{t + 1} = w_{t} - α \nabla F (w_{t})$ .

[F6]

Gradient descent has vanishing gradients when the objective is bounded below along its iterates: a continuously differentiable objective on $R^{n}$ with globally $L$ -Lipschitz gradient for $L > 0$ , fixed $0 < α \leq 1 / L$ , and a lower bound along its iterates has gradient norms tending to zero along those iterates.

[F7]

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

Verification

1.1givenF1F2F3F4algebra

For $z = (x, y)$ and $v = (h, k)$ , expansion gives $F (z + v) - F (z) - (2 x h - 2 y k) = h^{2} - k^{2}$ , whose absolute value is at most $h^{2} + k^{2} = ∥ v ∥_{2}^{2}$ . For every $ε > 0$ , this is at most $ε ∥ v ∥_{2}$ when $∥ v ∥_{2} < ε$ , so [F1] gives the total derivative. The coordinate difference quotients are $2 x + h$ and $- 2 y - k$ , so [F2, F3] give $\nabla F (x, y) = (2 x, - 2 y)$ . Therefore $∥ \nabla F (z) - \nabla F (z^{'}) ∥_{2}^{2} = 4 ∥ z - z^{'} ∥_{2}^{2}$ , so $F$ is continuously differentiable and its gradient is globally $2$ -Lipschitz.

2.1givenF5step 1.1algebrainduction

By [F5] and the gradient formula in step 1.1, $w_{t + 1} = (x_{t} / 2, 3 y_{t} / 2)$ . Starting from $(1, 0)$ , induction gives $y_{t} = 0$ and $x_{t} = 2^{- t}$ for every $t \geq 0$ .

3.1givenF6step 1.1step 2.1F7algebra∎

Step 2.1 gives $F (w_{t}) = 4^{- t} \geq 0$ and $w_{t} \to (0, 0)$ by [F7], while $F (0, s) = - s^{2}$ is unbounded below as $∣ s ∣ \to \infty$ . The gradient at the limit is zero, but $F (h, 0) = h^{2} > F (0, 0)$ and $F (0, h) = - h^{2} < F (0, 0)$ for every $h \neq 0$ , so the limit is neither a local minimum nor a local maximum. Finally $α = 1 / 4 \leq 1 / 2 = 1 / L$ and the iterates have lower bound $0$ , so [F6] applies and gives vanishing gradient norms along this path.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

44 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.