Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-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 Wolfe step gives positive Bfgs curvature on a descent direction

Statement

Let f:D→R be C1 on an open D⊆Rn. At x∈D, let p≠0 be a strict descent direction, so gTp<0 for g:=∇f(x). Suppose α>0, x+αp∈D, and α satisfies the Wolfe curvature condition of Wolfe and strong Wolfe line-search conditions. With s:=αp and y:=∇f(x+αp)−∇f(x), one has sTy≥(1−c2)α∣gTp∣>0.

Facts & Assumptions

Given: f,x,p,α,g,s,y and the strict-descent and Wolfe hypotheses in the Statement.

[F1]

Wolfe and strong Wolfe line-search conditions: for ϕ(t)=f(x+tp), a Wolfe step satisfies ϕ′(α)≥c2ϕ′(0) with 0<c2<1; the chain rule gives ϕ′(t)=∇f(x+tp)Tp.

[F2]

Bfgs curvature pairs and Hessian/inverse updates: s=αp and y=∇f(x+αp)−∇f(x).

[F3]

The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn: uTv denotes the Euclidean inner product of u,v∈Rn.

Proof

1.1givenF1F2F3algebra

By [F1] and [F2], sTy=αpT(∇f(x+αp)−g)≥α(c2−1)gTp=(1−c2)α∣gTp∣. The last quantity is strictly positive because α>0, c2<1, and gTp<0.

2.1step 1.1F2∎

Thus sTy>0, so the curvature denominator used in the BFGS updates is positive and the pair meets the positive-curvature condition of Bfgs curvature pairs and Hessian/inverse updates.

Depends on

Used by

Dependency tree · two levels

22 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