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.
An exact Bfgs secant update on a two-variable quadratic
Example
Let and on . Start at with . The exact steepest-descent BFGS direction is . Take the exact line-search step and form the Hessian BFGS update.
Facts & Assumptions
Given: The objective, start, initial matrices, direction, and step in the Example.
Bfgs curvature pairs and Hessian/inverse updates: , , and when .
Full-memory Bfgs with Wolfe search, descent reset, and Powell damping: an exact full-memory iteration uses and accepts a positive strong Wolfe step before updating.
Bfgs updates preserve the secant equations, symmetry, and positive definiteness: an SPD BFGS update with positive curvature satisfies and remains SPD.
Verification
Given: The objective, start, initial matrices, direction, and step in the Example.
[F1] Bfgs curvature pairs and Hessian/inverse updates: , , and when .
[F2] Full-memory Bfgs with Wolfe search, descent reset, and Powell damping: an exact full-memory iteration uses and accepts a positive strong Wolfe step before updating.
[F3] Bfgs updates preserve the secant equations, symmetry, and positive definiteness: an SPD BFGS update with positive curvature satisfies and remains SPD.
The gradient is , so and the direction in [F2] is . Along this ray, , so the exact minimizer is .
At this step , which satisfies the strong curvature test for . The quadratic identity gives , so the strong Wolfe Armijo test also holds.
The step and gradient change are and . Hence and .
Substitution in [F1] gives Multiplication yields . The positive curvature from step 1.3 and [F3] also imply is SPD.
Remarks
This verifies one exact strong-Wolfe input to the BFGS recurrence. A finite-budget bracketing search may return a different acceptable step or a failure status; this example does not claim that the search returns exactly .
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
- Jorge Nocedal and Stephen J. Wright, Numerical Optimization, 2nd ed. (standard reference, not scraped)
- Manuel Carreira-Perpiñán, Lecture Notes on Numerical Optimization (standard reference, not scraped)