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 and let be the PR+ candidate direction from Fletcher–Reeves and safeguarded Polak–Ribière nonlinear conjugate gradients. The safeguarded procedure either keeps when or restarts to , where . The resulting direction is strictly descending and its angle with satisfies using the angle convention of Wolfe and strong Wolfe line-search conditions.
Facts & Assumptions
Given: , , the PR+ candidate, and the safeguard in the Statement.
Fletcher–Reeves and safeguarded Polak–Ribière nonlinear conjugate gradients: the PR+ safeguard keeps a candidate only if and ; otherwise it sets .
Wolfe and strong Wolfe line-search conditions: for a descent direction.
Proof
Given: The hypotheses and notation in the Statement.
If the candidate is kept, then , so it is descending. Using the norm test and [F2],
In the kept branch, [F3] also gives , so necessarily and the bound in step 1.1 implies . If the candidate is reset, then , whence and . Both branches prove the claim.
Depends on
- Fletcher–Reeves and safeguarded Polak–Ribière nonlinear conjugate gradients
- Wolfe and strong Wolfe line-search conditions
- The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case
- The Euclidean inner product $\langle x,y\rangle = \sum_{k<n} x_k y_k$ on $\mathbb{R}^n$
- Cauchy-Schwarz $\lvert\langle x,y\rangle\rvert \le \lVert x\rVert_2\lVert y\rVert_2$ with its equality case, the triangle inequality for $\lVert\cdot\rVert_2$, the parallelogram law and polarisation
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
- Jorge Nocedal and Stephen J. Wright, Numerical Optimization, second edition (standard reference, not scraped)
- Jean Charles Gilbert and Jorge Nocedal, Global Convergence Properties of Conjugate Gradient Methods for Optimization, SIAM Journal on Optimization 2(1), 21–42 (1992), DOI 10.1137/0802003 (standard reference, not scraped)