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.
Phase-field and dissipative gradient-flow computation — Examples
1 · Prerequisites
- Absolute and Conditional Convergence; Rearrangement; Products
- Absolute Continuity and the Sharp Fundamental Theorem of Calculus
- Areas of Elementary Plane Figures
- Banach Valued Integration and the Radon Nikodym Property
- Binary Operations, Monoids, Groups and Subgroups
- Bounded Variation and the Riemann–Stieltjes Integral
- Compactness
- Compactness in Metric Spaces
- Completeness, Completion, and Uniform Continuity
- Complex Lp Spaces and Test-Function Conventions
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Continuity, IVT, EVT, and Uniform Continuity
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Countability Axioms and Cardinal Functions
- Density Separability and Convolution in Lᵖ
- Determinants of Matrices over a Commutative Ring
- Differentiation of Monotone Functions and the Vitali Covering Theorem
- Distributions Test Functions and Differentiation
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Dual Spaces, Bilinear and Quadratic Forms, and Sylvester's Law of Inertia
- Euclidean Surface Measure, Divergence, and Green Identities
- Filters and Ultrafilters
- Finite Counting, Factorials and Binomial Coefficients
- Finite-volume diffusion on admissible meshes
- Foundations of the Real Numbers for Analysis
- Fubini and Change of Variables
- Gaussian Elimination, Elementary Matrices and Reduced Row Echelon Form
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Inner Product Spaces, Gram-Schmidt, Projections and Adjoints
- Lebesgue Measure on Euclidean Space
- Limits of Real Functions
- limsup, liminf, and Subsequential Limits
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- Matrices, the Matrix of a Linear Map, and Change of Basis
- Measurable Functions and Simple Approximation
- Measures and Their Basic Properties
- Metric Spaces
- Mixed Partials, Taylor Formulae, and Extrema
- Modes of Convergence Egorov and Lusin
- Monotone Functions, Discontinuities, and Continuity Sets
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Normal Subgroups and Quotient Groups
- Order, Zorn's Lemma, and the Axiom of Choice
- Outer Measure and the Caratheodory Extension Theorem
- Phase-field and dissipative gradient-flow computation
- Pointwise Extended-Real Function Products
- Polynomial Rings, the Division Algorithm and Roots
- Power Series and Real-Analytic Functions
- Product Measures and the Fubini Tonelli Theorems
- Properties of the Integral and the Working FTC
- Relations, Functions, and Quotients
- Rings, Subrings, Integral Domains and Fields
- Rⁿ as a Normed Space; Vector-Valued Functions
- Roots, Rational Powers, and Classical Inequalities
- Schwartz Space and the Plancherel Theorem
- Separation Axioms: the Hierarchy
- Sequences and Limits
- Sequences and Series of Functions; Uniform Convergence
- Series: Convergence and the Nonnegative Tests
- Sigma Algebras and Borel Sets
- Signed and Complex Measures Hahn and Jordan
- Simple Field Extensions and the Construction of the Complex Numbers
- Smooth Approximation and Sobolev Extension
- Smooth Partitions of Unity and Exhaustions
- Sobolev Poincare and Morrey Inequalities
- Subspaces, Products, and Quotients
- Suprema and Infima
- Symmetric Groups, Cycle Decomposition and the Sign Homomorphism
- The Cantor Set, Baire Category, and Measure Zero in ℝ
- The Complex Exponential and Euler's Formula
- The Derivative and the Mean Value Theorems
- The Exponential Function
- The Inverse and Implicit Function Theorems
- The Lebesgue Integral and the Convergence Theorems
- The Logarithm and General Powers
- The Lᵖ Spaces Holder Minkowski and Riesz Fischer
- The Maximal Function and Lebesgue Differentiation
- The Radon Nikodym Theorem and Lebesgue Decomposition
- The Riemann Integral in Rᵐ and Jordan Content
- The Riemann Integral: Definition and Integrability
- The Topology of Euclidean Space
- The Total Derivative in ℝᵐ → ℝⁿ
- The ZFC Axioms and the Basic Set Constructions
- Topological Spaces and Continuity
- Topology of ℝ
- Triangularisation, Generalised Eigenspaces and Jordan Canonical Form
- Vector Spaces, Linear Subspaces, Span and Direct Sums
- Weak Derivatives and Sobolev Spaces
2 · Summary
These four worked examples keep exact calculations separate from general stability claims. The one-dimensional Allen–Cahn front The one-dimensional Allen–Cahn double-well front verifies the stationary ODE and finite energy on ; it is not a bounded-interval no-flux solution. Its profile has a transition width . The companion grid calculation Interface width and a grid that misses the transition places a uniform grid of spacing halfway between samples and shows that when exceeds this width, no sample lies inside the transition. This is a missed-interface example, not a sufficient resolution criterion.
Modified-energy decay alone does not imply physical-energy decay gives scalar pairs on a one-cell no-flux mesh of unit cell volume with . The auxiliary values move from to : decreases from to , while the physical double-well energy rises from to . These pairs refute the implication from a modified-energy inequality alone; they are explicitly not claimed to be a trajectory of the SAV update.
The two-cell ledger A two-cell Cahn–Hilliard mass and energy ledger takes unit cells, one interior transmissibility , zero boundary flux, unit parameters, and initial data . It reduces the convex-splitting CH step to the unique root of and returns . The mean remains zero, and the exact physical energies are and . Each calculation is proved in its item carrier.
Companion A page: phase-field-and-energy-dissipative-discretization.
3 · Logical flowchart
4 · Definitions, theorems and proofs
None yet.
5 · Examples, counterexamples and false statements
The one-dimensional Allen–Cahn double-well front
Example
For , on the real line set This is a stationary finite-energy heteroclinic profile for the one-dimensional Allen–Cahn Euler–Lagrange equation . It is a profile example on , 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 .
Allen–Cahn and Cahn–Hilliard double-well gradient flows: and the stationary Allen–Cahn equation is .
Verification
Put . Differentiation gives and . Since , by [F1].
The limits of at are . Also , so the energy density is , which is integrable because it decays exponentially at both ends. Hence the profile has finite energy and joins the two wells.
Interface width and a grid that misses the transition
Example
For the front in The one-dimensional Allen–Cahn double-well front, the interval where has width If a uniform sample grid has spacing and the front is centered halfway between two sample points, no grid point lies in that transition interval. This gives a precise unresolved-interface configuration; it is not a sufficient resolution criterion.
Facts & Assumptions
Given: The exact front profile and positive parameters .
The one-dimensional Allen–Cahn double-well front: and its transition is centered at .
Verification
Since is strictly increasing and , the endpoints of are . Subtracting them gives as stated.
Place sample points at for . Their distance from the front center is at least , so every sample point lies outside the transition interval from step 1.1. The grid therefore records no sample with .
Modified-energy decay alone does not imply physical-energy decay
Statement refuted
The scalar inequality , by itself, implies .
Construction
Take a one-cell no-flux mesh with cell volume , so the gradient term is zero and the cell-volume mass is one, and set . Let , , , and . Then the modified scalar energy decreases from to , while the original double-well energy increases from to . These scalar pairs are a counterexample to the stated implication from an energy inequality alone; they are not asserted to be a trajectory of the SAV update equations.
Facts & Assumptions
Given: The physical double-well energy and the SAV modified energy definition.
Allen–Cahn and Cahn–Hilliard double-well gradient flows: is the original potential energy density.
No-flux finite-volume and conforming realizations for phase fields: ; on a one-cell no-flux mesh and the potential term is .
The SAV step is uniquely solvable and dissipates a modified energy: the SAV theorem dissipates .
Refutation
On one cell, [F2] gives and . Direct substitution using [F1] gives and .
The modified energies of the displayed pairs are and by [F3], so the modified energy strictly decreases while the physical energy strictly increases by step 1.1. Hence the proposed implication is false. The pairs are not claimed to satisfy the SAV update, so this refutes only the logical implication from modified-energy decay alone.
A two-cell Cahn–Hilliard mass and energy ledger
Example
Take two unit cells on , one interior face with transmissibility , no-flux boundary faces, , and . The discrete mean is zero, and the one-step convex-splitting state is where is the unique root in of . The initial energy is and the new energy is .
Facts & Assumptions
Given: The two-cell finite-volume realization and the convex-splitting Cahn–Hilliard step.
No-flux finite-volume and conforming realizations for phase fields: for this two-cell mesh, , , and .
Existence, uniqueness, mass conservation, and energy decay of a convex-splitting step: the Cahn–Hilliard step is unique, preserves the discrete mean, and does not increase .
Verification
The initial mean is zero, so mass conservation [F2] forces . Since and , , the first chemical-potential component is . The first state equation gives , hence . The polynomial is strictly increasing because its derivative is , and its values at and are and ; therefore it has exactly one root .
The initial gradient energy is and both potential terms vanish, so . For the gradient energy is and the potential energy is . Since , , hence . This is the exact finite ledger for the step.
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
- Jie Shen, Jie Xu, and Jiang Yang, The scalar auxiliary variable (SAV) approach for gradient flows, Journal of Computational Physics 353 (2018), 407–416
- R. Eymard, T. Gallouët, and R. Herbin, Finite Volume Methods, Handbook of Numerical Analysis, Vol. VII, 2000; complete updated author text
- Jing Guo, Cheng Wang, Steven M. Wise, and Xingye Yue, An H2 convergence of a second-order convex-splitting finite difference scheme for the three-dimensional Cahn–Hilliard equation, Communications in Mathematical Sciences 14 (2016), 489–515