ExampleConstruction: AI-generatedVerification: 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.

One accepted Rosenbrock step gives different FR and PR+ coefficients

Example

For the Rosenbrock function $f (x, y) = (1 - x)^{2} + 100 (y - x^{2})^{2}$ , take $x_{0} = (- 6 / 5, 1)$ and $d_{0} = - g_{0}$ . With $c_{1} = 1 / 1000$ , $c_{2} = 49 / 100$ , bounded search budgets $E \geq 1$ , $Z \geq 10$ , and outer budget $K \geq 2$ , the first accepted step is $t_{0} = 1 / 1024$ . Its FR and PR+ coefficients differ. The PR+ candidate ascends, so the safeguarded method restarts; for definiteness take $σ = 1 / 2$ and $C = 2$ .

Facts & Assumptions

Given: The function, start and parameters in the Example, with exact arithmetic.

[F1]

Fletcher–Reeves and safeguarded Polak–Ribière nonlinear conjugate gradients: $d_{0} = - g_{0}$ ; FR uses $β_{0}^{F R} = ∥ g_{1} ∥_{2}^{2} / ∥ g_{0} ∥_{2}^{2}$ , whereas the PR+ candidate uses $β_{0}^{P R +} = \max {0, g_{1}^{T} (g_{1} - g_{0}) / ∥ g_{0} ∥_{2}^{2}}$ ; a failed descent or norm test resets it to $- g_{1}$ .

[F2]

Wolfe and strong Wolfe line-search conditions: strong Wolfe requires Armijo decrease and $∣ ϕ^{'} (t) ∣ \leq c_{2} ∣ ϕ^{'} (0) ∣$ .

[F3]

Finite-budget bracketing and zoom for a strong Wolfe step: the first expansion trial is $1$ ; an Armijo failure calls zoom with endpoints $(0, 1)$ , whose midpoint trials halve the positive endpoint while the same failure persists.

Verification

Given: The objective, initial point and budgets of the Example.

1.1givenF1algebra

Differentiation gives $g_{0} = (- 1078 / 5, - 88)$ , $d_{0} = (1078 / 5, 88)$ , $f (x_{0}) = 121 / 5$ , and $ϕ^{'} (0) = - G_{0}$ with $G_{0} = 1,355,684 / 25 = 54,227.36$ . At a parameter $t$ , write $u = - 6 / 5 + (1078 / 5) t$ , $v = 1 + 88 t$ , and $r = v - u^{2}$ . Then $ϕ (t) = (1 - u)^{2} + 100 r^{2}$ and $ϕ^{'} (t) = (- 400 u r + 2 (u - 1)) (1078 / 5) + 200 r (88)$ .

2.1givenF3step 1.1algebra

Exact substitution into step 1.1 gives integer lower bounds for $ϕ (2^{- j})$ , in order $j = 0, \dots, 9$ : $210482437168$ , $12810991198$ , $758614013$ , $42388850$ , $2078788$ , $72456$ , $543$ , $211$ , $149$ , and $35$ . Each lower bound exceeds $121 / 5$ , whereas every positive-trial Armijo right side is below $121 / 5$ . Thus the initial trial fails Armijo and the first nine zoom trials fail it as well. By [F3], $a = 0$ remains fixed and the tenth zoom trial is $t_{0} = 2^{- 10} = 1 / 1024$ .

3.1givenF2F3step 1.1step 2.1algebra

At this trial, $x_{1} = (- 2533 / 2560, 139 / 128)$ and $r = 700711 / 6553600$ . Exactly, $f (x_{1}) = \frac{438182241277}{85899345920} < \frac{511}{100}, g_{1} = (\frac{1608013539}{41943040}, \frac{700711}{32768}), h : = g_{1}^{T} d_{0} = \frac{1064039515121}{104857600} .$ The Armijo right side is $121 / 5 - G_{0} / (1000 \cdot 1024) > 24$ , so Armijo holds. Also $0 < h < 10148 < 26571 < (49 / 100) G_{0} = 26571.4064$ , so strong curvature holds. The search therefore returns this tenth midpoint.

4.1givenF1step 3.1algebra

Put $G_{1} = ∥ g_{1} ∥_{2}^{2} = 3390155233212910921 / 1759218604441600$ . Because $g_{0} = - d_{0}$ and $h > 0$ , the coefficients are $β_{0}^{F R} = G_{1} / G_{0}$ and $β_{0}^{P R +} = (G_{1} + h) / G_{0} > β_{0}^{F R}$ . The FR direction is $- g_{1} + (G_{1} / G_{0}) d_{0}$ ; the PR+ candidate is $d_{1}^{c a n d} = - g_{1} + ((G_{1} + h) / G_{0}) d_{0}$ . Exact values in step 3.1 give $1927 < G_{1} < 1928$ , $10147 < h < 10148$ , and $54227 < G_{0} < 54228$ . Hence $g_{1}^{T} d_{1}^{c a n d} = - G_{1} + \frac{(G_{1} + h) h}{G_{0}} > - 1928 + \frac{(1927 + 10147) 10147}{54228} > 331 > 0.$ It fails the descent safeguard for every $σ > 0$ . Thus the actual selected PR+ direction is $d_{1} = - g_{1}$ and its restart flag is true; the ascending candidate is not the selected direction.

5.1givenF1F2step 1.1algebra∎

For comparison, the originally displayed trial $\hat{t} = 1 / 1000$ is also a mathematically valid strong Wolfe step, but is not an output of this dyadic search. It gives $\hat{x} = (- 2461 / 2500, 136 / 125)$ , $\hat{r} = 743479 / 6250000$ , $f (\hat{x}) = 5.35291158000896$ , $\hat{g} = (42.8715665664, 23.791328)$ , and $\hat{h} = {\hat{g}}^{T} d_{0} = 11336.74661571584$ . Its Armijo bound is $24.14577264$ and $∣ \hat{h} ∣ < 11400 < 26571.4064$ , verifying both inequalities directly. With $\hat{G} = ∥ \hat{g} ∥_{2}^{2}$ , its distinct coefficients are $\hat{G} / G_{0}$ and $(\hat{G} + \hat{h}) / G_{0}$ ; these describe the hypothetical accepted update at $\hat{t}$ , rather than the actual bounded-search trace above.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

23 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.