ExampleConstruction: AI-adaptedVerification: AI-generatedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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 one-dimensional Allen–Cahn double-well front

Example

For $κ, ε > 0$ , on the real line set $u_{ε} (x) = \tanh ⁣ (\frac{x}{\sqrt{2 κ} ε}) .$ This is a stationary finite-energy heteroclinic profile for the one-dimensional Allen–Cahn Euler–Lagrange equation $- κ u^{''} + f_{ε} (u) = 0$ . It is a profile example on $R$ , not a boundary-value solution on a bounded no-flux interval.

Facts & Assumptions

Given: The double-well potential and Allen–Cahn variational derivative in Allen–Cahn and Cahn–Hilliard double-well gradient flows, with fixed $κ, ε > 0$ .

[F1]

Allen–Cahn and Cahn–Hilliard double-well gradient flows: $f_{ε} (s) = (s^{3} - s) / ε^{2}$ and the stationary Allen–Cahn equation is $- κ u^{''} + f_{ε} (u) = 0$ .

Verification

1.1F1algebra

Put $a = (\sqrt{2 κ} ε)^{- 1}$ . Differentiation gives $u_{ε}^{'} = a (1 - u_{ε}^{2})$ and $u_{ε}^{''} = - 2 a^{2} u_{ε} (1 - u_{ε}^{2}) = 2 a^{2} (u_{ε}^{3} - u_{ε})$ . Since $2 κ a^{2} = ε^{- 2}$ , $- κ u_{ε}^{''} + f_{ε} (u_{ε}) = 0$ by [F1].

2.1givenstep 1.1algebra∎

The limits of $u_{ε}$ at $\pm \infty$ are $\pm 1$ . Also $1 - u_{ε}^{2} = {sech}^{2} (a x)$ , so the energy density is $\frac{1}{2 ε^{2}} {sech}^{4} (a x)$ , which is integrable because it decays exponentially at both ends. Hence the profile has finite energy and joins the two wells.

Depends on

Allen–Cahn and Cahn–Hilliard double-well gradient flows

Used by

Interface width and a grid that misses the transition Example

Dependency tree · two levels

6 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

Jie Shen and Xiaofeng Yang, Numerical approximations of Allen-Cahn and Cahn-Hilliard equations, Discrete and Continuous Dynamical Systems A 28 (2010), 1669–1691 (standard reference, not scraped)