Alphabeta Math
LemmaStatement: AI-adaptedProof: 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.

The safeguarded PR+ direction has a uniform angle bound

Statement

Let g≠0 and let dcand be the PR+ candidate direction from Fletcher–Reeves and safeguarded Polak–Ribière nonlinear conjugate gradients. The safeguarded procedure either keeps dcand when gTdcand≤−σ∥g∥22,∥dcand∥2≤C∥g∥2, or restarts to d=−g, where σ,C>0. The resulting direction is strictly descending and its angle θ with −g satisfies cos⁡θ≥δPR:=min⁡{1,σ/C}>0, using the angle convention of Wolfe and strong Wolfe line-search conditions.

Facts & Assumptions

Given: g≠0, σ,C>0, the PR+ candidate, and the safeguard in the Statement.

[F1]

Fletcher–Reeves and safeguarded Polak–Ribière nonlinear conjugate gradients: the PR+ safeguard keeps a candidate only if gTd≤−σ∥g∥22 and ∥d∥2≤C∥g∥2; otherwise it sets d=−g.

[F2]

Wolfe and strong Wolfe line-search conditions: cos⁡θ=−gTd/(∥g∥2∥d∥2) for a descent direction.

Proof

Given: The hypotheses and notation in the Statement.

1.1givenF1F2algebra

If the candidate is kept, then gTd≤−σ∥g∥22<0, so it is descending. Using the norm test and [F2], cos⁡θ=−gTd∥g∥2∥d∥2≥σC.

2.1givenF1F3step 1.1algebra∎

In the kept branch, [F3] also gives cos⁡θ≤1, so necessarily σ/C≤1 and the bound in step 1.1 implies cos⁡θ≥δPR. If the candidate is reset, then d=−g, whence gTd=−∥g∥22<0 and cos⁡θ=1≥δPR. Both branches prove the claim.

Depends on

Used by

Dependency tree · two levels

28 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