Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Computer-Assisted Proofs for Geometric Optimization: From Crystallization to Carbon Nanotubes

Miguel Ayala, Rustum Choksi, Benedikt Wirth

TL;DR

The paper develops a rigorous computer-assisted proof (CAP) framework to certify the existence and stability of critical points for atomistic energy functions $E:\mathbb{R}^{3n}\to\mathbb{R}$ that are invariant under translations and rotations. It uses a Newton-Kantorovich–type fixed-point argument with an extended system $F_{\bar p}$ that enforces six invariances, together with interval arithmetic to obtain computable bounds $Y$ and $Z(r^*)$ and certify a unique zero in a certified ball, as well as local minimality via Hessian positivity checks. The framework is demonstrated on two applications: (i) capped carbon nanotubes under harmonic, Tersoff, and Huber-type potentials, yielding proven local minimizers and cap-induced diameter oscillations; (ii) a finite Lennard–Jones crystal in an fcc lattice with a perfect crystal, a vacancy, and a connecting saddle, all validated, with NEB providing the approximate saddle. This work provides a general, rigorous workflow for geometry optimization in molecular systems, with potential to handle modern, possibly machine-learned potentials through interval arithmetic and validated derivatives.$

Abstract

We present a framework based on computer-assisted proofs that turns standard geometry optimization simulations for atomistic structures into mathematical proofs. Starting from a numerically computed approximation of a local minimizer or saddle point, we use validated numerical computations to prove the existence of a critical point of the potential energy close to this approximation. We demonstrate this framework in two settings. In the first, we study capped carbon nanotubes modeled as minimizers of carbon interatomic potentials (harmonic, Tersoff, and a Huber potential) and obtain proven bounds on tube diameter, bond lengths, and bond angles. In particular, we show that caps induce diameter oscillations along the tube. As a second application, we consider a finite Lennard-Jones crystal in a face-centered cubic (fcc) lattice and provide computer-proofs of a local minimizer representing the perfect crystal, a local minimizer with a single vacancy defect, and a saddle point that connects two single-vacancy configurations on the energy landscape.

Computer-Assisted Proofs for Geometric Optimization: From Crystallization to Carbon Nanotubes

TL;DR

The paper develops a rigorous computer-assisted proof (CAP) framework to certify the existence and stability of critical points for atomistic energy functions that are invariant under translations and rotations. It uses a Newton-Kantorovich–type fixed-point argument with an extended system that enforces six invariances, together with interval arithmetic to obtain computable bounds and and certify a unique zero in a certified ball, as well as local minimality via Hessian positivity checks. The framework is demonstrated on two applications: (i) capped carbon nanotubes under harmonic, Tersoff, and Huber-type potentials, yielding proven local minimizers and cap-induced diameter oscillations; (ii) a finite Lennard–Jones crystal in an fcc lattice with a perfect crystal, a vacancy, and a connecting saddle, all validated, with NEB providing the approximate saddle. This work provides a general, rigorous workflow for geometry optimization in molecular systems, with potential to handle modern, possibly machine-learned potentials through interval arithmetic and validated derivatives.$

Abstract

We present a framework based on computer-assisted proofs that turns standard geometry optimization simulations for atomistic structures into mathematical proofs. Starting from a numerically computed approximation of a local minimizer or saddle point, we use validated numerical computations to prove the existence of a critical point of the potential energy close to this approximation. We demonstrate this framework in two settings. In the first, we study capped carbon nanotubes modeled as minimizers of carbon interatomic potentials (harmonic, Tersoff, and a Huber potential) and obtain proven bounds on tube diameter, bond lengths, and bond angles. In particular, we show that caps induce diameter oscillations along the tube. As a second application, we consider a finite Lennard-Jones crystal in a face-centered cubic (fcc) lattice and provide computer-proofs of a local minimizer representing the perfect crystal, a local minimizer with a single vacancy defect, and a saddle point that connects two single-vacancy configurations on the energy landscape.

Paper Structure

This paper contains 4 sections, 10 theorems, 39 equations, 17 figures, 2 tables.

Table of Contents

  1. Introduction
  2. Computer-assisted Proofs for Geometry Optimization
  3. Carbon Nanotubes Geometries
  4. FCC Lattice

Key Result

Theorem 2.1

Let $f:\mathbb{R}^{m} \to \mathbb{R}^{m}$ be differentiable and $\bar{x} \in \mathbb{R}^{m}$, $A\in\mathbb{R}^{m\times m}$. Suppose that for some $r^{*}>0$ and $Y,Z(r^*)>0$ we have Then for any $r$ in the interval $[r_{\min}, r^{*}]$ there exists a unique zero of $f$ in $\overline {B}_r(\bar{x})$.

Figures (17)

  • Figure 1: Top: Initialization of the BFGS gradient descent to find a local minimizer for a $(5,5)$-armchair nanotube using the harmonic potential $E_{\mathrm{h}}$. Bottom and right: Validated numerical approximation of the local minimizer (side and top view).
  • Figure 1: Left: A portion of a graphene sheet with the chiral vector $\mathbf{C} = n {a}_1 + m {a}_2$ indicated. Rolling the sheet along $\mathbf{C}$ forms a carbon nanotube with chirality $(n, m)$. Right: Structure of a $\mathrm{C}_{60}$ fullerene.
  • Figure 1: Left: approximate local minimizer of the Lennard--Jones energy $E_{\mathrm{LJ}}$ from \ref{['eq:LJ-potential']}, corresponding to an fcc lattice block of $864$ atoms. Right: face-centered cubic (fcc) reference cell, with line segments drawn between atoms to make the three-dimensional structure easier to see.
  • Figure 2: Dependence of $Z(r^*)$ and $r_{\min}$ on $r^*$ for the example of \ref{['theorem:existence_armchair_harmonic']}.
  • Figure 2: Slice of the fcc lattice around a reference atom and neighborhood-distance diagram. Left: slice of the lattice block in the local minimizer from Theorem \ref{['theorem:lattice_minimizer']}, with the reference atom indicated by a red rectangle. Right: neighborhood-distance diagram for the reference atom. Each point represents a neighboring atom. The vertical axis shows its distance from the reference atom, and the horizontal axis orders atoms in the vicinity by their distance from this reference atom. The diagram shows the fcc shell structure in the first three shells, with 12 neighbors in the first shell, 6 in the second, and 24 in the third.
  • ...and 12 more figures

Theorems & Definitions (18)

  • Theorem 2.1: Validated zero
  • Proof 1
  • Theorem 2.2: Removal of invariances
  • Proof 2
  • Corollary 2.3: Validated local minimizers of $E$
  • Proof 3
  • Theorem 3.1: Capped armchair nanotube
  • Proof 4
  • Remark 3.2: The radius of the nanotube
  • Theorem 3.3: Capped zigzag nanotube
  • ...and 8 more