LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

Powell damping gives a strictly positive curvature pair

Statement

Let $B$ be SPD, let $s \neq 0$ , and put $c : = s^{T} B s > 0$ and $q : = s^{T} y$ for an arbitrary $y$ . Define $\tilde{y}$ by Powell damping in Bfgs curvature pairs and Hessian/inverse updates. Then $s^{T} \tilde{y} \geq 0.2 c > 0$ . In the damped branch, the coefficient $θ$ is strictly between $0$ and $1$ and $s^{T} \tilde{y} = 0.2 c$ .

Facts & Assumptions

Given: $B, s, y, c, q$ and the damping rule in the Statement.

[F1]

Bfgs curvature pairs and Hessian/inverse updates: if $q < 0.2 c$ , then $θ = 0.8 c / (c - q)$ and $\tilde{y} = θ y + (1 - θ) B s$ ; otherwise $\tilde{y} = y$ .

Proof

Given: $B, s, y, c, q$ and the damping rule in the Statement.

[F1] Bfgs curvature pairs and Hessian/inverse updates: if $q < 0.2 c$ , then $θ = 0.8 c / (c - q)$ and $\tilde{y} = θ y + (1 - θ) B s$ ; otherwise $\tilde{y} = y$ .

1.1givenF1algebra

In the damped branch, $q < 0.2 c$ gives $c - q > 0.8 c > 0$ . Therefore $θ > 0$ and $θ < 1$ .

2.1givenF1step 1.1algebra∎

In that branch, $s^{T} \tilde{y} = θ q + (1 - θ) c = c - θ (c - q) = c - 0.8 c = 0.2 c > 0.$ In the other branch, $\tilde{y} = y$ and $q \geq 0.2 c$ , so $s^{T} \tilde{y} = q \geq 0.2 c > 0$ .

Depends on

Bfgs curvature pairs and Hessian/inverse updates

Used by

Powell damping repairs a negative-curvature trial pair Example

Dependency tree · two levels

3 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)