Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-generatedPipeline-generatedprecheck pass
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.

Fletcher–Reeves descent and direction-growth bound

Statement

Let gk=∇f(xk)≠0 and let the Fletcher–Reeves directions be d0=−g0,dk=−gk+βk−1dk−1,βk−1=∥gk∥22∥gk−1∥22(k≥1). Suppose every accepted step along dk−1 satisfies the strong Wolfe curvature inequality with constant 0<c2<1/2. Define qk=−gkTdk∥gk∥22,δ=1−2c21−c2,C3=1+c21−c2,Sk=∑j=0k1∥gj∥22. Then, for every k, δ≤qk≤11−c2,∥dk∥22≤C3∥gk∥24Sk. In particular every direction is strictly descending, and its normalized directional derivative has a uniform positive lower bound.

Facts & Assumptions

Given: The nonzero gradients, Fletcher–Reeves recurrence, and strong Wolfe curvature hypotheses in the Statement.

[F1]

Fletcher–Reeves and safeguarded Polak–Ribière nonlinear conjugate gradients: FR uses d0=−g0, dk=−gk+βk−1dk−1, and βk−1=∥gk∥22/∥gk−1∥22.

[F2]

Wolfe and strong Wolfe line-search conditions: a strong Wolfe step along dk−1 satisfies ∣gkTdk−1∣≤c2∣gk−1Tdk−1∣, with 0<c2<1/2.

Proof

Given: The hypotheses and notation in the Statement.

1.1givenF1algebra

From d0=−g0, we have q0=1.

1.2F1algebra

For k≥1, the recurrence and the definition of βk−1 give qk=1−gkTdk−1∥gk−1∥22.

2.1givenF2step 1.1step 1.2inductionalgebra

If 0<qk−1≤(1−c2)−1, then [F2] and step 1.2 imply 1−c2qk−1≤qk≤1+c2qk−1. Induction from step 1.1 gives qk≤∑j=0kc2j≤(1−c2)−1, and then qk≥1−c2/(1−c2)=δ>0.

3.1F1F2step 2.1algebra

Expanding dk=−gk+βk−1dk−1, applying [F2], and using step 2.1 yields ∥dk∥22≤∥gk∥22+2βk−1∣gkTdk−1∣+βk−12∥dk−1∥22≤C3∥gk∥22+∥gk∥24∥gk−1∥24∥dk−1∥22, because ∣gkTdk−1∣≤c2qk−1∥gk−1∥22 and qk−1≤(1−c2)−1.

4.1step 3.1inductionalgebra∎

For k=0, ∥d0∥22=∥g0∥22≤C3∥g0∥24S0. If the claimed bound holds at k−1, step 3.1 gives ∥dk∥22≤C3∥gk∥22+C3∥gk∥24Sk−1=C3∥gk∥24Sk. Thus induction proves the direction-growth bound.

Remarks

The first bound is on −gkTdk/∥gk∥22, not on the cosine of the angle. It does not by itself give a uniform angle bound.

Depends on

Used by

Dependency tree · two levels

23 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