Alphabeta Math
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.

Zero discrete force does not select a unique continuum path

Example

Prescribe Cbad=∅, and let U=R2 and V≡0. Every regular path from A=(0,0) to B=(1,0) satisfies the MEP equation, so there are infinitely many distinct continuum MEPs. For a finite string with M=2, both chains

R1(0)=(1/2,0),R1(1)=(1/2,1)

have equal adjacent segment lengths and zero projected force. The improved-tangent NEB ordinary force also vanishes for both. Thus their discrete residuals are exactly zero, although their interior images differ.

Facts & Assumptions

Given: The zero potential, fixed endpoints A,B, two finite chains, and the definitions of the string, NEB, and stable path comparison.

[F1]

Regular minimum-energy paths on a declared collision-free tube: a regular path is an MEP when the normal gradient vanishes; fixed endpoints are part of the path data.

[F2]

Finite-image projected-gradient string with arc-length redistribution: the string stops when the projected-force and equal-spacing residuals are both within tolerance.

[F3]

Finite-budget improved-tangent NEB with a climbing image: the ordinary NEB force is projected gradient plus a tangential spring term.

[F4]

A gauge-fixed stable discrete path lies within second order of a smooth MEP: a local path error conclusion requires an invertible residual Jacobian with a uniform inverse bound and other stated consistency/stability hypotheses.

Proof

Given: The potential, endpoints, and finite chains in the Example.

1.1F1givenalgebra

For each c∈R, Rc(t)=(t,csin⁡(πt)) on [0,1] is regular because its first coordinate derivative is 1, and it has endpoints A,B. Since ∇V=0, every normal gradient component is zero, so [F1] makes every Rc an MEP. Distinct c give distinct paths.

1.2F2F3givenalgebra

For M=2, each listed interior point is equidistant from A and B: the two distances are 1/2 when R1=(1/2,0) and both 5/2 when R1=(1/2,1). Thus the adjacent lengths agree. Since the gradient is zero, the string projected force is zero by [F2], and the ordinary NEB spring term is also zero by [F3]. Both chains therefore have exactly zero force and spacing residuals.

2.1F4step 1.1step 1.2algebra∎

The two chains differ in their interior image, and the continuum family in step 1.1 is nonunique. In this example the string residual map has no locally invertible Jacobian that can isolate a path: its force components vanish identically and its spacing equation alone cannot determine the two coordinates of the interior image. Thus the inverse/stability premise [F4] is absent. Independently of that missing premise, the two distinct MEPs and two zero-residual chains explicitly prove nonuniqueness. Each chain's midpoint lies on its corresponding exact MEP Rc, so this is not an assertion of inaccuracy relative to every MEP. Relative to the prescribed reference R0([0,1]), however, the second chain's midpoint has Euclidean distance 1 while its residual is zero. Therefore residual alone cannot select a unique continuum MEP or bound distance to that reference by an error bound that vanishes with the residual.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

10 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