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.

The straight chord misses the curved double-well minimum-energy path

Example

Let D=(−π/4,π/4)×(−1/4,1/4), X(s,n)=(1+n)(cos⁡s,sin⁡s), and U=X(D). Put a=π/6, W(s)=(s2−a2)2, and V(X(s,n))=W(s)+n2/2 on U. The endpoints of the circular MEP are (cos⁡a,−sin⁡a) and (cos⁡a,sin⁡a). Their straight chord is the vertical segment C(y)=(cos⁡a,y) for −sin⁡a≤y≤sin⁡a. The chord lies inside the annular sector, but it is not a MEP.

Facts & Assumptions

Given: The sector chart and potential above, with a=π/6.

[F1]

Regular minimum-energy paths on a declared collision-free tube: a regular path is a MEP only if its gradient component normal to the path tangent vanishes at every point.

[F2]

Finite-budget improved-tangent NEB with a climbing image: the NEB tangent is constructed from adjacent image differences; an energy-selected tangent does not change the continuous MEP equation.

[F3]

The chain rule for total derivatives: D(g∘f)(a)=Dg(f(a))∘Df(a): the chart-coordinate derivative in the n direction equals the ambient gradient paired with N.

Proof

Given: The chord and potential in the Example.

1.1givenalgebra

Along C, the first coordinate is cos⁡a>0, and ∣y∣/cos⁡a≤tan⁡a<1, so the polar angle lies in [−a,a]⊂(−π/4,π/4). Its radius is between cos⁡a=3/2>3/4 and 1<5/4. Thus the whole chord is in the declared sector.

1.2F3givenalgebra

The chord's tangent is e2=(0,1). At its midpoint x0=(cos⁡a,0)=X(0,n0) with n0=cos⁡a−1≠0. In the chart Xs=(1+n)T and Xn=N, where T(0)=e2 and N(0)=e1. The coordinate derivatives of V there are ∂sV=W′(0)=0 and ∂nV=n0, so by [F3] ∇V(x0)⋅e1=n0≠0.

2.1F1F2step 1.2∎

Since e1 is perpendicular to the chord tangent e2, step 1.2 gives a nonzero normal component of the gradient at the chord midpoint. This violates the MEP condition in [F1], proving the chord is not the circular MEP. The improved tangent rule in [F2] only changes the discrete force direction; it does not make this straight segment satisfy the continuous normal-gradient equation.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

9 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