| _version_ | 1866902218217619456 |
|---|---|
| author | Sherrington, Ryan |
| author_facet | Sherrington, Ryan |
| contents | <div> <div>We formalize the convex cone of stress-energy tensors satisfying Averaged Quantum Energy Inequalities (AQEI) using Lean 4, with computational searches in Mathematica to identify extreme rays or boundary points. We prove that the admissible set defined by continuous affine inequalities is closed and convex, and that its homogenization yields a closed convex cone. In a finite-dimensional discretization using Gaussian wave-packets in 1+1D Minkowski space, we identify and formally verify a nontrivial vertex using exact rational arithmetic.</div> </div> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_18522457 |
| institution | Zenodo |
| language | eng |
| publishDate | 2026 |
| publisher | Zenodo |
| record_format | zenodo |
| spellingShingle | Convex Cone of Energy Tensors under AQEI: Formal Verification and Computational Exploration Sherrington, Ryan Averaged Quantum Energy Inequalities (AQEI) Lean 4 Formal Verification Convex Geometry Stress-Energy Tensor Extreme Rays Quantum field theory Geometry Minkowski Space Interactive Theorem Proving Exact Rational Arithmetic Polyhedral Geometry Mathematical physics Mathematical Computing Mathematics Mathematics Wolfram Mathematica <div> <div>We formalize the convex cone of stress-energy tensors satisfying Averaged Quantum Energy Inequalities (AQEI) using Lean 4, with computational searches in Mathematica to identify extreme rays or boundary points. We prove that the admissible set defined by continuous affine inequalities is closed and convex, and that its homogenization yields a closed convex cone. In a finite-dimensional discretization using Gaussian wave-packets in 1+1D Minkowski space, we identify and formally verify a nontrivial vertex using exact rational arithmetic.</div> </div> |
| title | Convex Cone of Energy Tensors under AQEI: Formal Verification and Computational Exploration |
| topic | Averaged Quantum Energy Inequalities (AQEI) Lean 4 Formal Verification Convex Geometry Stress-Energy Tensor Extreme Rays Quantum field theory Geometry Minkowski Space Interactive Theorem Proving Exact Rational Arithmetic Polyhedral Geometry Mathematical physics Mathematical Computing Mathematics Mathematics Wolfram Mathematica |
| url | https://doi.org/10.5281/zenodo.18522457 |