TheoremStatement: AI-adaptedProof: 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.

First-order time error under smooth fixed-mesh solutions

Statement

Fix one finite-dimensional realization in No-flux finite-volume and conforming realizations for phase fields and $T > 0$ . Let $G_{c, h} (u) = κ A_{h} u + \nabla_{h} P_{c, h} (u)$ and $G_{e, h} (u) = \nabla_{h} P_{e, h} (u)$ . The exact semidiscrete Allen–Cahn trajectory is the solution of $y^{'} = - M (G_{c, h} (y) - G_{e, h} (y))$ ; the exact semidiscrete Cahn–Hilliard trajectory is the fixed-mean solution of $y^{'} = - M A_{h} (G_{c, h} (y) - G_{e, h} (y))$ . Assume the applicable exact trajectory is $C^{2}$ on $[0, T]$ and remains in a compact set. Let the numerical solution start from $u^{0} = y (0)$ and use the convex-splitting step. Then there are constants $C > 0$ and $τ_{0} > 0$ , depending on the fixed spatial realization, $ε, κ, M$ , the exact trajectory, and $T$ , such that, for $0 < τ \leq τ_{0}$ :

for Allen–Cahn, $\max_{n τ \leq T} ∥ u^{n} - y (t_{n}) ∥_{h} \leq C τ$ ;
for Cahn–Hilliard, with $y$ and $u^{n}$ having the same mean and $∥ z ∥_{- 1, h}^{2} = ⟨ A_{h}^{†} z, z ⟩_{h}$ on mean-zero vectors, $\max_{n τ \leq T} ∥ u^{n} - y (t_{n}) ∥_{- 1, h} \leq C τ$ .

This is a fixed-mesh time estimate; it is not a uniform spatial error bound.

Facts & Assumptions

Given: A fixed finite-dimensional realization, the convex energy split, the exact semidiscrete solution, its stated smoothness and compact range, the exact initial value, and a step size $0 < τ \leq τ_{0}$ .

[F1]

Backward-Euler convex splitting for Allen–Cahn and Cahn–Hilliard: the AC update is $δ u / τ = - M (G_{c, h} (u^{n + 1}) - G_{e, h} (u^{n}))$ , and the CH update is $δ u / τ = - M A_{h} (G_{c, h} (u^{n + 1}) - G_{e, h} (u^{n}))$ .

[F2]

Existence, uniqueness, mass conservation, and energy decay of a convex-splitting step: each step exists uniquely, the physical discrete energy is nonincreasing, and the convex implicit term has the monotonicity used in its proof.

[F3]

Kernel, range, and mean-zero inverse for the no-flux Laplacian: $A_{h}$ is self-adjoint, nonnegative, and invertible on mean-zero vectors, so $∥ \cdot ∥_{- 1, h}$ is a norm there and $A_{h}^{†}$ is available.

[F4]

Allen–Cahn and Cahn–Hilliard double-well gradient flows and No-flux finite-volume and conforming realizations for phase fields: the scalar split is $F_{c} (s) = s^{4} / (4 ε^{2}) + s^{2} / (2 ε^{2})$ , $F_{e} (s) = s^{2} / ε^{2} - 1 / (4 ε^{2})$ , so $\nabla_{h} P_{e, h} (u) = 2 u / ε^{2}$ is globally Lipschitz and $P_{c, h}$ is convex.

[A1]

The relevant exact semidiscrete trajectory is $C^{2}$ and its image lies in a compact set on which $G_{c, h}$ has bounded derivative.

Proof

1.1A1F1F3givenalgebra

Substitute the exact trajectory into the backward-Euler split. For Allen–Cahn define $R_{n}^{A C} : = y (t_{n + 1}) - y (t_{n}) + M τ (G_{c, h} (y (t_{n + 1})) - G_{e, h} (y (t_{n})))$ . For Cahn–Hilliard define $R_{n}^{C H} : = y (t_{n + 1}) - y (t_{n}) + M τ A_{h} (G_{c, h} (y (t_{n + 1})) - G_{e, h} (y (t_{n})))$ . The exact integral equations express these residuals as $M$ times the quadrature difference $τ G_{c, h} (y (t_{n + 1})) - \int_{t_{n}}^{t_{n + 1}} G_{c, h} (y (s)) d s + \int_{t_{n}}^{t_{n + 1}} G_{e, h} (y (s)) d s - τ G_{e, h} (y (t_{n}))$ , with an additional $A_{h}$ in the Cahn–Hilliard branch. The bounded derivatives on the compact exact trajectory and $∥ y (t) - y (s) ∥ \leq C ∣ t - s ∣$ imply $∥ R_{n}^{A C} ∥_{h} \leq C τ^{2}$ and $∥ R_{n}^{C H} ∥_{- 1, h} \leq C τ^{2}$ ; in the latter case $R_{n}^{C H}$ lies in the mean-zero range of $A_{h}$ by [F3].

2.1F2F4step 1.1algebra

Convexity of $P_{c, h}$ and nonnegativity of $A_{h}$ make $G_{c, h}$ monotone. By [F4], $G_{e, h}$ is globally Lipschitz with constant $L_{e} = 2 / ε^{2}$ . In the quartic realizations, the lower bound $F_{ε} (s) \geq s^{4} / (8 ε^{2}) - 1 / (4 ε^{2})$ and the energy inequality in [F2] also bound every numerical state on the fixed finite-dimensional space.

3.1F1F4step 1.1step 2.1algebra

In the Allen–Cahn branch put $e_{n} = u^{n} - y (t_{n})$ . Subtract the exact residual equation from the numerical recurrence and pair with $e_{n + 1}$ . The identity $2 ⟨ e_{n + 1} - e_{n}, e_{n + 1} ⟩_{h} = ∥ e_{n + 1} ∥_{h}^{2} - ∥ e_{n} ∥_{h}^{2} + ∥ e_{n + 1} - e_{n} ∥_{h}^{2}$ and monotonicity from step 2.1 leave only the explicit term and residual on the right. Cauchy–Schwarz and Young give $M τ L_{e} ∥ e_{n} ∥_{h} ∥ e_{n + 1} ∥_{h} \leq \frac{M τ L_{e}}{2} (∥ e_{n} ∥_{h}^{2} + ∥ e_{n + 1} ∥_{h}^{2})$ and $∥ R_{n}^{A C} ∥_{h} ∥ e_{n + 1} ∥_{h} \leq \frac{τ}{8} ∥ e_{n + 1} ∥_{h}^{2} + 2 τ^{- 1} ∥ R_{n}^{A C} ∥_{h}^{2}$ . For $τ$ small enough that $M τ L_{e} \leq 1 / 8$ and $τ \leq 1$ , step 1.1 then gives $∥ e_{n + 1} ∥_{h}^{2} \leq (1 + C τ) ∥ e_{n} ∥_{h}^{2} + C τ^{3}$ .

3.2F1F3F4step 1.1step 2.1algebra

In the Cahn–Hilliard branch both errors have mean zero. Pair the original difference equation with $A_{h}^{†} e_{n + 1}$ . Self-adjointness and $A_{h} A_{h}^{†} e_{n + 1} = e_{n + 1}$ give $2 ⟨ e_{n + 1} - e_{n}, A_{h}^{†} e_{n + 1} ⟩_{h} = ∥ e_{n + 1} ∥_{- 1, h}^{2} - ∥ e_{n} ∥_{- 1, h}^{2} + ∥ e_{n + 1} - e_{n} ∥_{- 1, h}^{2}$ . The implicit term becomes $M τ ⟨ G_{c, h} (u^{n + 1}) - G_{c, h} (y_{n + 1}), e_{n + 1} ⟩_{h} \geq M τ κ ∥ e_{n + 1} ∥_{1, h}^{2}$ , because $G_{c, h}$ is the sum of $κ A_{h}$ and the gradient of a convex functional. The explicit term obeys $∣ ⟨ G_{e, h} (u^{n}) - G_{e, h} (y_{n}), e_{n + 1} ⟩_{h} ∣ \leq L_{e} ∥ e_{n} ∥_{- 1, h} ∥ e_{n + 1} ∥_{1, h}$ , where $∥ v ∥_{1, h}^{2} = ⟨ A_{h} v, v ⟩_{h}$ . Indeed, on the mean-zero space $(x, y)_{A_{h}} : = ⟨ A_{h} x, y ⟩_{h}$ is an inner product and $⟨ e_{n}, e_{n + 1} ⟩_{h} = (A_{h}^{†} e_{n}, e_{n + 1})_{A_{h}}$ , with $∥ A_{h}^{†} e_{n} ∥_{A_{h}} = ∥ e_{n} ∥_{- 1, h}$ and $∥ e_{n + 1} ∥_{A_{h}} = ∥ e_{n + 1} ∥_{1, h}$ . Cauchy–Schwarz in this inner product gives the bound. Young's inequality absorbs half of the positive $M τ κ ∥ e_{n + 1} ∥_{1, h}^{2}$ term and leaves $C τ ∥ e_{n} ∥_{- 1, h}^{2}$ . The residual from step 1.1 satisfies $∣ ⟨ R_{n}^{C H}, A_{h}^{†} e_{n + 1} ⟩_{h} ∣ = ∣ ⟨ R_{n}^{C H}, e_{n + 1} ⟩_{- 1, h} ∣ \leq C τ^{2} ∥ e_{n + 1} ∥_{- 1, h} \leq \frac{τ}{8} ∥ e_{n + 1} ∥_{- 1, h}^{2} + C^{'} τ^{3}$ . Hence, for small $τ$ , $∥ e_{n + 1} ∥_{- 1, h}^{2} \leq (1 + C τ) ∥ e_{n} ∥_{- 1, h}^{2} + C τ^{3}$ .

4.1step 3.1step 3.2algebra∎

In either recurrence, $e_{0} = 0$ . Iterating $z_{n + 1} \leq (1 + C τ) z_{n} + C τ^{3}$ for $n τ \leq T$ gives $z_{n} \leq C τ^{3} \sum_{j = 0}^{n - 1} (1 + C τ)^{j} \leq C_{T} τ^{2}$ , since $(1 + C τ)^{n} \leq e^{C T}$ . Taking square roots gives the two asserted $O (τ)$ bounds. The constants include the fixed-mesh operator norms, the fixed parameters $M, κ, ε$ , and the trajectory bounds.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

13 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)
Jie Shen, Jie Xu, and Jiang Yang, The scalar auxiliary variable (SAV) approach for gradient flows, Journal of Computational Physics 353 (2018), 407–416 (standard reference, not scraped)