Alphabeta Math
TheoremStatement: 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.

Finite-budget nonlinear conjugate gradient returns a status

Statement

Assume function and gradient evaluations at requested in-domain points return real values. For finite outer limit K and finite expansion and zoom limits E,Z, the procedure of Fletcher–Reeves and safeguarded Polak–Ribière nonlinear conjugate gradients terminates with one of stationary, search-failure, or iteration-limit. In bounded-strong-Wolfe mode it makes at most K line-search calls and at most K(E+Z) line-search trial evaluations, each of which evaluates the objective and directional derivative at one trial point. Separately, the outer iteration evaluates the gradient at most K+1 times: once initially and once after each accepted update. The theorem does not claim a total gradient-evaluation count, because the line search also evaluates directional derivatives. It gives no arithmetic-work or finite-precision error bound.

Facts & Assumptions

Given: The finite budgets, evaluation convention and algorithm in the Statement.

[F1]

Fletcher–Reeves and safeguarded Polak–Ribière nonlinear conjugate gradients: the outer loop ranges over k=0,…,K−1 and can accept at most one update per iteration.

[F2]

Bracketing and zoom terminate with a checked step or a failure: a bounded call uses at most E expansion trial evaluations.

[F3]

Bracketing and zoom terminate with a checked step or a failure: at most one zoom call occurs, with at most Z trial evaluations.

[F4]

Bracketing and zoom terminate with a checked step or a failure: each evaluated trial evaluates ϕ(t) and ϕ′(t), and a bounded call terminates with either a checked positive feasible strong Wolfe step or a failure status.

[F5]

Fletcher–Reeves and safeguarded Polak–Ribière nonlinear conjugate gradients: the algorithm evaluates the initial gradient once.

[F6]

Fletcher–Reeves and safeguarded Polak–Ribière nonlinear conjugate gradients: after each accepted update it evaluates one new iterate gradient and returns stationary if it is zero; when the loop ends with a nonzero last gradient, it returns iteration-limit.

Proof

Given: The hypotheses and budgets in the Statement.

1.1givenF2F3F4

By [F2] and [F3], each bounded strong Wolfe call uses at most E+Z trial evaluations; [F4] specifies that each trial evaluates ϕ(t) and ϕ′(t) and that the call returns a checked step or a failure. In exact-SPD-quadratic mode, the algorithm instead computes and checks its single formula step.

2.1F1F5F6step 1.1algebra∎

By [F1] and [F6], there are at most K outer iterations; each either returns a terminal status or accepts one step, and after the loop any nonzero last gradient yields iteration-limit. Thus bounded mode makes at most K line-search calls and K(E+Z) trial evaluations. By [F5] and [F6], the outer algorithm evaluates the initial gradient once and one new iterate gradient per accepted update, hence at most K+1 outer-iterate gradient evaluations.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

7 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