Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2506.22614 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866917191124779008 |
|---|---|
| author | Ayala, Miguel Choksi, Rustum Wirth, Benedikt |
| author_facet | Ayala, Miguel Choksi, Rustum Wirth, Benedikt |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_22614 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Computer-Assisted Proofs for Geometric Optimization: From Crystallization to Carbon Nanotubes Ayala, Miguel Choksi, Rustum Wirth, Benedikt Computational Physics Mathematical Physics 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. |
| title | Computer-Assisted Proofs for Geometric Optimization: From Crystallization to Carbon Nanotubes |
| topic | Computational Physics Mathematical Physics |
| url | https://arxiv.org/abs/2506.22614 |