ExampleConstruction: AI-adaptedVerification: 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 curved double well has an exact circular minimum-energy path

Example

Prescribe $C_{b a d} = {(0, 0)}$ . Let $D = (- π / 4, π / 4) \times (- 1 / 4, 1 / 4)$ and define

$X (s, n) = (1 + n) (\cos s, \sin s), U : = X (D) .$

The domain satisfies $U \subseteq R^{2} ∖ C_{b a d}$ . Indeed, it is an open annular sector: its points have radius $3 / 4 < ∥ x ∥_{2} < 5 / 4$ , positive first coordinate, and angular coordinate in $(- π / 4, π / 4)$ . The displayed polar map is one-to-one on $D$ with smooth inverse $s = \arctan (y / x)$ and $n = \sqrt{x^{2} + y^{2}} - 1$ . Let $a = π / 6$ , $W (s) = (s^{2} - a^{2})^{2}$ , and define $V (X (s, n)) = W (s) + n^{2} / 2$ on $U$ . The curve $R (t) = X (- a + 2 a t, 0)$ , $0 \leq t \leq 1$ , is a regular MEP joining the two minima $X (- a, 0)$ and $X (a, 0)$ . Its image is the circular arc of radius one. The point $X (0, 0)$ is an index-one saddle.

Facts & Assumptions

Given: The chart, potential, $a = π / 6$ , and path in the Example.

[F1]

Regular minimum-energy paths on a declared collision-free tube: a regular MEP has zero gradient component normal to its unit tangent, and the endpoints are fixed data.

[F2]

The Hessian matrix and critical points of a scalar field: at a critical point the Hessian is the matrix of second partial derivatives and its negative-eigenvalue count is the Morse index used here. Since $V$ is $C^{2}$ , The Hessian of a $C^{2}$ scalar field is symmetric makes that Hessian symmetric.

[F3]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : derivatives of a scalar field in the displayed chart equal its ambient gradient paired with the chart tangent vectors.

[F4]

Since $U$ is open, a sufficiently small convex open ball centered at $X (0, 0)$ has its closure in $U$ . The potential is $C^{\infty}$ on that ball, so Multivariable Taylor formula with a Lagrange remainder along a line segment applies there; bounded third derivatives on the compact closure give a quadratic expansion with remainder $O (∥ x - X (0, 0) ∥_{2}^{3}) = o (∥ x - X (0, 0) ∥_{2}^{2})$ .

Given: The data above.

Proof

1.1F1F3givenalgebra

Write $T (s) = (- \sin s, \cos s)$ and $N (s) = (\cos s, \sin s)$ . Then $X_{s} = (1 + n) T (s)$ and $X_{n} = N (s)$ are orthogonal, with lengths $1 + n > 0$ and $1$ . By [F3], $\nabla V (X (s, n)) \cdot T (s) = W^{'} (s) / (1 + n)$ and $\nabla V (X (s, n)) \cdot N (s) = n$ . At $n = 0$ , the path tangent is $T (s)$ and its unit normal is $N (s)$ , so the normal gradient component vanishes. The path is regular because $∥ R^{'} (t) ∥_{2} = 2 a > 0$ ; hence it is a regular MEP by [F1].

1.2givenalgebra

Since $W (s) \geq 0$ and $n^{2} / 2 \geq 0$ , the potential is nonnegative and equals zero exactly at $(s, n) = (- a, 0)$ and $(a, 0)$ . Thus both specified endpoints are global minima on $U$ .

2.1F2F4step 1.1givenalgebra

At $(s, n) = (0, 0)$ , $W^{'} (0) = 0$ and $n = 0$ , so step 1.1 gives $\nabla V (X (0, 0)) = 0$ . The coordinate Hessian of $V \circ X = W (s) + n^{2} / 2$ is $diag (W^{''} (0), 1) = diag (- 4 a^{2}, 1)$ . By [F4], the quadratic Taylor term of $V$ at $X (0, 0)$ is $\frac{1}{2} v^{T} (D^{2} V) v + o (∥ v ∥_{2}^{2})$ . Substituting $v = X (s, n) - X (0, 0) = D X (0, 0) (s, n) + O (s^{2} + n^{2})$ shows the coordinate quadratic form is $D X (0, 0)^{T} (D^{2} V) D X (0, 0)$ ; the linear term vanishes because the point is critical. Since $D X (0, 0) = [T (0), N (0)]$ is orthogonal, this is an orthogonal representation of the ambient Hessian. By [F2] it has exactly one negative eigenvalue, making the point an index-one saddle.

3.1givenstep 2.1∎

The fixed-endpoint finite-image string of Finite-image projected-gradient string with arc-length redistribution can sample and redistribute this arc, but that finite procedure alone does not imply convergence to it from arbitrary initial images.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

18 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

Weinan E, Weiqing Ren, and Eric Vanden-Eijnden, String method for the study of rare events (standard reference, not scraped)
Graeme Henkelman, Blas P. Uberuaga, and Hannes Jónsson, A climbing image nudged elastic band method for finding saddle points and minimum energy paths (standard reference, not scraped)