ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generated

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.

A damped Newton step precedes the local quadratic phase

Example

The strongly convex objective $f (x) = \frac{1}{2} x^{2} + 10 \sqrt{1 + x^{2}}$ makes a Newton step from $x_{0} = 2$ increase the objective, while its half-step passes Armijo. With a small positive decrement tolerance, the global-to-local theorem then ensures a finite damped phase followed by unit Newton steps whenever the decrement test continues to permit updates.

Facts & Assumptions

Given: $f (x) = \frac{1}{2} x^{2} + 10 \sqrt{1 + x^{2}}$ on $R$ , $x_{0} = 2$ , Armijo parameter $a = 1 / 100$ , shrink factor $b = 1 / 2$ , and decrement tolerance $ε = 10^{- 16}$ .

[F1]

Damped Newton reaches its local quadratic phase in finitely many continued updates: with global bounds $m, M$ , local radius $ρ$ , and $ε < m^{2} ρ^{2} / (2 M)$ , the method reaches the local ball in finitely many updates; later attempted steps are unit and quadratic.

[F2]

Damped Newton method: the method computes $p = - H (x)^{- 1} \nabla f (x)$ and $λ^{2} = \nabla f (x)^{T} H (x)^{- 1} \nabla f (x)$ , stops before line search when $λ^{2} / 2 \leq ε$ , and otherwise starts backtracking at $t = 1$ .

[F3]

Newton's method has local quadratic convergence under a Lipschitz Hessian: with a positive-definite critical Hessian and a Lipschitz Hessian on a ball, there are local constants such that every generated iterate stays in the ball and every attempted Newton update not stopped by the decrement test accepts a unit step with a quadratic error bound.

[F4]

The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ : a differentiable scalar function whose derivative is bounded in absolute value by $L$ on an interval is $L$ -Lipschitz there.

[F5]

Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line: a closed and bounded subset of the real line is compact.

[F6]

The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case and The Hessian matrix and critical points of a scalar field: the gradient is the first derivative and the Hessian is the second derivative in the one-dimensional coordinate.

[F7]

Multivariable Taylor formula with a Lagrange remainder along a line segment: on a segment in an open convex domain, the second-order Taylor remainder is one half the Hessian at an interior point times the squared step.

Verification

1.1F4F5F6givenalgebra

Differentiation gives $g (x) = x + 10 x / \sqrt{1 + x^{2}}$ , $H (x) = 1 + 10 / (1 + x^{2})^{3 / 2}$ , and $H^{'} (x) = - 30 x / (1 + x^{2})^{5 / 2}$ . Thus $1 \leq H (x) \leq 11$ , $g (x)$ has the sign of $x$ , and $x^{*} = 0$ is the unique minimizer. Also $∣ H^{'} (x) ∣ \leq 30$ , since $∣ x ∣ \leq 1 + x^{2} \leq (1 + x^{2})^{5 / 2}$ ; [F4] makes $H$ globally $30$ -Lipschitz. The initial sublevel set is closed by continuity and bounded because $f (x) \geq x^{2} / 2$ , hence compact by [F5].

1.2F2F6givenalgebra

At $x_{0} = 2$ , $g = 2 + 4 \sqrt{5}$ , $H = 1 + 2 / \sqrt{5}$ , and the Newton direction is $p = - g / H = 30 - 16 \sqrt{5}$ . Its decrement is $λ^{2} = g^{2} / H = 260 - 88 \sqrt{5} > 62$ , since $5 < 81 / 16$ gives $\sqrt{5} < 9 / 4$ ; hence the positive tolerance test does not stop before the first line search.

2.1F3F4F7givenstep 1.1algebrachoose

Step 1.1 gives $g (0) = 0$ , $H (0) = 11 > 0$ , and a $30$ -Lipschitz Hessian on $B (0, 1)$ , so [F3] applies there; we directly verify the local radius $ρ = 10^{- 6}$ and constant $C = 10$ . For $0 < ∣ x ∣ \leq ρ$ , $H (x) \geq 1$ and $∣ g (x) ∣ \leq 11 ∣ x ∣$ , so the Newton direction $p = - g (x) / H (x)$ satisfies $∣ p ∣ \leq 11 ∣ x ∣$ . Every point $ξ$ between $x$ and $x + p$ therefore satisfies $∣ H (ξ) - H (x) ∣ \leq 30 ∣ p ∣ \leq 330 ρ$ . Since $330 ρ = 33 / 100000 < 49 / 50 = 1 - 2 a$ and $H (x) \geq 1$ , we have $H (ξ) \leq H (x) + 330 ρ \leq 2 (1 - a) H (x)$ . Taylor's formula [F7] and $g (x) p = - H (x) p^{2}$ now give $f (x + p) - f (x) - a g (x) p = - (1 - a) H (x) p^{2} + H (ξ) p^{2} / 2 \leq 0$ , so the full step passes Armijo. Also $x + p = (x H (x) - g (x)) / H (x) = - 10 x^{3} / ((1 + x^{2})^{3 / 2} H (x))$ , hence $∣ x + p ∣ \leq 10 ∣ x ∣^{3} \leq 10 ∣ x ∣^{2}$ because $∣ x ∣ \leq ρ < 1$ , and $∣ x + p ∣ \leq 10 ρ^{2} ∣ x ∣ < ρ$ since $10 ρ^{2} = 10^{- 11} < 1$ . Thus $C = 10$ and this $ρ$ give a directly verified invariant local ball and quadratic bound whenever the decrement test permits an update.

2.2F2step 1.2algebra

The full-step point is $x_{1} = 32 - 16 \sqrt{5}$ , whose absolute value exceeds $2$ because $289 / 64 < 5$ gives $\sqrt{5} > 17 / 8$ . The objective is even and strictly increasing as a function of $∣ x ∣ > 0$ , so $f (x_{1}) > f (2)$ ; its Armijo threshold $f (2) + a g p = f (2) - a λ^{2}$ is smaller than $f (2)$ , and the unit step fails.

2.3F2step 1.2algebra

The half-step point is $x_{1 / 2} = 17 - 8 \sqrt{5} = - r$ , where $0 < r = 8 \sqrt{5} - 17 < 1$ : indeed $289 / 64 < 5 < 324 / 64$ implies $17 / 8 < \sqrt{5} < 9 / 4$ . Thus $f (x_{1 / 2}) = r^{2} / 2 + 10 \sqrt{1 + r^{2}} < 1 / 2 + 10 \sqrt{2} < 31 / 2$ , using $2 < 9 / 4$ and so $\sqrt{2} < 3 / 2$ , while $f (2) = 2 + 10 \sqrt{5} > 22$ because $\sqrt{5} > 2$ . The objective drop exceeds $13 / 2$ . The half-step Armijo decrease required is $q / 200$ , where $q = λ^{2} < 84$ because $\sqrt{5} > 2$ , so $q / 200 < 21 / 50 < 13 / 2$ . Hence $t = 1 / 2$ passes, and it is accepted after the failed unit trial.

3.1F1step 2.3step 2.1givenalgebra∎

Choose $V = R$ , which contains every trial segment and $B (0, 1)$ . By step 1.1 the global Hessian bounds are $m = 1$ , $M = 11$ , and the decrement threshold in [F1] is $m^{2} ρ^{2} / (2 M) = 10^{- 12} / 22$ . The chosen $ε = 10^{- 16}$ is smaller, since $22 < 10^{4}$ gives $10^{- 16} < 10^{- 12} / 22$ , so the decrement test cannot stop outside $B (0, ρ)$ . The first accepted step was the damped half-step in step 2.3; [F1] now gives finite entry into the local ball, followed by unit quadratic updates whenever the decrement test does not stop.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

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