TheoremStatement: AI-adaptedProof: 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 gap-controlled dimer mode gives a local saddle-translation error recurrence

Statement

Let $d \geq 2$ , let $V \in C^{4} (U, R)$ on an open $U \subseteq R^{d}$ using the convention of $C^{k}$ maps and multi-index derivative notation in Euclidean space, and let $x_{*}$ be a critical point with Hessian $H_{*} : = \nabla^{2} V (x_{*})$ ordered as $λ_{1} (H_{*}) \leq \dots \leq λ_{d} (H_{*})$ . Suppose

$λ_{1} (H_{*}) \leq - 2 γ, λ_{j} (H_{*}) \geq 2 γ (j \geq 2), ∥ H_{*} u ∥_{2} \leq Λ ∥ u ∥_{2} (u \in R^{d})$

for $γ > 0$ and $Λ \geq 2 γ$ . Let the closed ball ${\overline{B}}_{2} (x_{*}, r)$ lie in $U$ , and suppose the Hessian satisfies $∥ (H (x) - H (y)) u ∥_{2} \leq L ∥ x - y ∥_{2} ∥ u ∥_{2} (x, y \in {\overline{B}}_{2} (x_{*}, r), u \in R^{d})$ with $L r \leq γ$ . At every iterate $x$ in this ball, suppose a validated Hessian enclosure gives $λ_{1} (H (x)) \leq - γ$ and $λ_{j} (H (x)) \geq γ$ for $j \geq 2$ , and accepted dimer data satisfy the hypotheses of A separated dimer mode gives a local inexact saddle error bound with uniform rotation residual $τ_{r o t}$ and HVP error bound $δ \leq γ / 4$ . Define

$α : = \frac{4 (τ_{r o t} + δ)}{5 γ}, q : = \max {∣ 1 + σ λ_{1} (H_{*}) ∣, \max_{2 \leq j \leq d} ∣ 1 - σ λ_{j} (H_{*}) ∣},$

where $0 < σ < 2 / Λ$ . Suppose the finite dimer saddle translation of Finite-budget dimer rotation and saddle translation uses a unit direction $v$ from those accepted data and a computed gradient $\hat{g} (x)$ with $∥ \hat{g} (x) - \nabla V (x) ∥_{2} \leq η$ . Put

$κ : = q + \frac{σ L r}{2} + 2 σ (α + \frac{L r}{3 γ}) (Λ + \frac{L r}{2}) .$

If $κ < 1$ and $σ η \leq (1 - κ) r$ , then every attempted translation starting at $∥ x_{0} - x_{*} ∥_{2} \leq r$ remains in the ball and obeys

$∥ x_{k + 1} - x_{*} ∥_{2} \leq κ ∥ x_{k} - x_{*} ∥_{2} + σ η,$

and consequently

$∥ x_{k} - x_{*} ∥_{2} \leq κ^{k} ∥ x_{0} - x_{*} ∥_{2} + \frac{σ η (1 - κ^{k})}{1 - κ} .$

Thus exact translation gradients give local contraction, while a fixed bounded translation-force error gives the stated finite noise floor. The conclusion is conditional on a validated gap and accepted dimer mode at every attempted iterate; a finite rotation cap or missing spectral enclosure gives no such guarantee.

Facts & Assumptions

Given: The critical point, Hessian gap and norm bound, Hessian-Lipschitz ball, validated enclosures, accepted dimer data, translation step size, and gradient-evaluation error bound in the Statement.

[A1]

At $x_{*}$ , $λ_{1} (H_{*}) \leq - 2 γ$ , all other eigenvalues are at least $2 γ$ , and $∥ H_{*} u ∥_{2} \leq Λ ∥ u ∥_{2}$ for every $u$ .

[A2]

On $B_{2} (x_{*}, r)$ , $∥ (H (x) - H (y)) u ∥_{2} \leq L ∥ x - y ∥_{2} ∥ u ∥_{2}$ for all $x, y$ and $u$ , $L r \leq γ$ , and each attempted point has the stated validated index-one enclosure.

[A3]

As assumed in the Statement, at each attempted point the whole finite-difference segment lies in $U$ , the paired gradient errors and coordinate third-derivative bounds define the uniform HVP error $δ$ as in the cited mode theorem, and the accepted dimer data have $∥ (I - v v^{T}) D_{ϵ} ∥_{2} \leq τ_{r o t}$ , $v^{T} D_{ϵ} \leq - γ / 2$ , and HVP error at most $δ \leq γ / 4$ .

[A4]

Each translation uses step $σ$ and a computed gradient with error at most $η$ ; $κ < 1$ and $σ η \leq (1 - κ) r$ .

[F1]

A separated dimer mode gives a local inexact saddle error bound: the full mode-bound hypotheses in [A3], together with the validated enclosures in [A2], give $\sin ∠ (v, q_{x}) \leq α$ for a unit lowest-eigenvalue eigenvector $q_{x}$ of $H (x)$ .

[F3]

Vector Newton remainder under a Lipschitz Jacobian: if $\nabla V (x_{*}) = 0$ and the Hessian is $L$ -Lipschitz on a convex ball, then $∥ \nabla V (x) - H_{*} (x - x_{*}) ∥_{2} \leq (L / 2) ∥ x - x_{*} ∥_{2}^{2}$ .

[F4]

Finite-budget dimer rotation and saddle translation: the saddle translation is $x^{+} = x + σ [- \hat{g} + 2 ({\hat{g}}^{T} v) v]$ when the finite rotation and force branches permit an update.

[F5]

$C^{k}$ maps and multi-index derivative notation in Euclidean space, The Hessian matrix and critical points of a scalar field, and The Jacobian matrix of partial derivatives and the gradient in the scalar-valued case fix the derivative conventions. The continuous coordinate partials supplied by $V \in C^{4}$ make $\nabla V$ totally differentiable with continuous derivative by If all partial derivatives exist on a neighbourhood and are continuous at a point, then the map is totally differentiable there with Jacobian derivative. A total derivative computes every directional derivative, and its matrix is the Jacobian identifies the matrix of $D (\nabla V)$ with the gradient Jacobian; The Hessian of a $C^{2}$ scalar field is symmetric makes those entries agree with $H = \nabla^{2} V$ .

[F6]

Since $V \in C^{4}$ , it is $C^{2}$ , and The Hessian of a $C^{2}$ scalar field is symmetric makes each Hessian in the proof symmetric. The standard Euclidean inner product then makes the corresponding endomorphism self-adjoint, so Real spectral theorem: a self-adjoint endomorphism of a finite-dimensional real inner product space has an orthonormal eigenbasis gives an orthonormal eigenbasis.

[F7]

Courant-Fischer min-max principle for self-adjoint endomorphisms on finite-dimensional real inner product spaces: eigenvalues of symmetric operators are characterized by Rayleigh quotients and subspace extrema. Cauchy-Schwarz $∣ ⟨ x, y ⟩ ∣ \leq ∥ x ∥_{2} ∥ y ∥_{2}$ with its equality case, the triangle inequality for $∥ \cdot ∥_{2}$ , the parallelogram law and polarisation bounds each quadratic perturbation $∣ u^{T} E u ∣$ by $∥ E u ∥_{2}$ for unit $u$ .

[F8]

Every Euclidean linear map has a unique matrix and satisfies $∥ L h ∥_{2} \leq K ∥ h ∥_{2}$ for some $K \geq 0$ gives a finite bound for each matrix acting on $R^{d}$ ; because $d \geq 2$ , its unit sphere is nonempty. The Cauchy-sequence reals have the least-upper-bound property supplies the real supremum. Thus the operator-norm supremum in [F3] is defined, and the vectorwise Hessian-Lipschitz assumption in [A2] bounds it by $L ∥ x - y ∥_{2}$ .

Proof

technique · direct perturbation and error recurrence

1.1A1A2F6F7F8givenalgebra

By [F6], choose an orthonormal eigenbasis $q_{*}, q_{2}, \dots, q_{d}$ for $H_{*}$ , with $q_{*}$ corresponding to $λ_{1} (H_{*})$ . Put $A = - H_{*}$ , $E = - (H (x) - H_{*})$ , and $ε = L ∥ e ∥_{2}$ for $e = x - x_{*}$ . By [A2], $∥ E u ∥_{2} \leq ε ∥ u ∥_{2}$ for every $u$ , and [F8] makes the operator-norm supremum well-defined with $∥ E ∥_{o p} \leq ε \leq L r \leq γ$ . The leading eigenvalue gap of $A$ is $g_{*} : = λ_{2} (H_{*}) - λ_{1} (H_{*}) \geq 4 γ$ . For every unit $u$ , [F7] gives $∣ u^{T} E u ∣ \leq ε$ . Evaluating the Rayleigh quotient of $A + E$ at $q_{*}$ gives ${\tilde{λ}}_{1} \geq λ_{1} (A) - ε$ , while the min-max formula on $q_{*}^{⊥}$ gives ${\tilde{λ}}_{2} \leq λ_{2} (A) + ε$ . Hence the leading eigenvalue of $A + E = - H (x)$ is simple, since ${\tilde{λ}}_{1} - {\tilde{λ}}_{2} \geq g_{*} - 2 ε \geq 2 γ > 0$ . If $q_{x}$ is its unit leading eigenvector, projecting $(A + E) q_{x} = {\tilde{λ}}_{1} q_{x}$ onto $q_{*}^{⊥}$ and expanding in $q_{2}, \dots, q_{d}$ gives $\sin^{2} ∠ (q_{x}, q_{*}) = \sum_{j = 2}^{d} ∣ q_{j}^{T} q_{x} ∣^{2} \leq ∥ E q_{x} ∥_{2}^{2} / (g_{*} - ε)^{2} \leq (L r)^{2} / (3 γ)^{2}$ . Thus $\sin ∠ (q_{x}, q_{*}) \leq L r / (3 γ)$ . The vector $q_{x}$ is a lowest-eigenvalue eigenvector of $H (x)$ .

1.2A1F6givenalgebra

Set $P_{*} = q_{*} q_{*}^{T}$ and $A_{*} = - I + 2 P_{*}$ . Orthogonal decomposition into $span (q_{*})$ and its complement shows $∥ A_{*} u ∥_{2} = ∥ u ∥_{2}$ for every $u$ . In the eigenbasis from [F6], the map $I + σ A_{*} H_{*}$ scales the $q_{*}$ coordinate by $1 + σ λ_{1} (H_{*})$ and each other eigen-coordinate by $1 - σ λ_{j} (H_{*})$ . Therefore $∥ (I + σ A_{*} H_{*}) e ∥_{2} \leq q ∥ e ∥_{2}$ for every $e$ . Because every $∣ λ_{j} (H_{*}) ∣ \in [2 γ, Λ]$ by [A1] and $0 < σ < 2 / Λ$ , each factor has absolute value strictly less than one, so $q < 1$ .

2.1A2A3F1step 1.1algebra

For unit vectors $u, w$ , choose the sign of $w$ so $u^{T} w \geq 0$ and write $w = (\cos θ) u + (\sin θ) z$ with $z ⊥ u$ unit. On $span {u, z}$ , the matrix of $u u^{T} - w w^{T}$ squares to $\sin^{2} θ I$ , and it vanishes on the orthogonal complement. Hence $∥ (u u^{T} - w w^{T}) y ∥_{2} \leq \sin θ ∥ y ∥_{2}$ for every $y$ . Apply this bound twice and use the triangle inequality through $q_{x}$ ; [F1] and step 1.1 give $∥ (v v^{T} - q_{*} q_{*}^{T}) y ∥_{2} \leq (α + L r / (3 γ)) ∥ y ∥_{2}$ for every $y$ .

2.2A1A2F3F5step 1.2algebra

By [F3], $\nabla V (x) = H_{*} e + r_{x}$ with $∥ r_{x} ∥_{2} \leq (L / 2) ∥ e ∥_{2}^{2}$ . Therefore the exact-mode translation satisfies $∥ x + σ A_{*} \nabla V (x) - x_{*} ∥_{2} \leq q ∥ e ∥_{2} + \frac{σ L}{2} ∥ e ∥_{2}^{2} \leq (q + \frac{σ L r}{2}) ∥ e ∥_{2}$ . Also [A1] gives $∥ H_{*} e ∥_{2} \leq Λ ∥ e ∥_{2}$ , so $∥ \nabla V (x) ∥_{2} \leq (Λ + L r / 2) ∥ e ∥_{2}$ .

3.1A2A4F4step 2.1step 2.2algebra

For the accepted dimer direction set $A_{v} = - I + 2 v v^{T}$ , another orthogonal reflection. By [F4], the actual update is $x^{+} = x + σ A_{v} \hat{g} (x)$ . Step 2.1 gives $∥ (A_{v} - A_{*}) \nabla V (x) ∥_{2} \leq 2 (α + L r / (3 γ)) ∥ \nabla V (x) ∥_{2}$ . Since $A_{v}$ preserves Euclidean norm and $∥ \hat{g} (x) - \nabla V (x) ∥_{2} \leq η$ , the remaining force discrepancy has norm at most $η$ . Combining with step 2.2 proves $∥ x^{+} - x_{*} ∥_{2} \leq κ ∥ e ∥_{2} + σ η$ .

4.1A4step 3.1inductionalgebra∎

If $∥ e ∥_{2} \leq r$ , step 3.1 and [A4] give $∥ x^{+} - x_{*} ∥_{2} \leq κ r + σ η \leq r$ , so each attempted update stays in the ball and the recurrence can be iterated. Induction on $k$ yields $∥ x_{k} - x_{*} ∥_{2} \leq κ^{k} ∥ x_{0} - x_{*} ∥_{2} + σ η \sum_{j = 0}^{k - 1} κ^{j}$ . Since $0 \leq κ < 1$ , the finite geometric sum is $(1 - κ^{k}) / (1 - κ)$ , giving the stated error bound.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

69 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

Graeme Henkelman and Hannes Jónsson, A dimer method for finding saddle points on high dimensional potential surfaces using only first derivatives (standard reference, not scraped)
E. Hairer and G. Wanner, Solving Ordinary Differential Equations II, Chapter VI: Iterative Methods—Nonlinear Equations (standard reference, not scraped)