| _version_ | 1866902216459157504 |
|---|---|
| author | Sherrington, Ryan |
| author_facet | Sherrington, Ryan |
| contents | <div> <div>We formally verify convexity of the AQEI-admissible cone in Lean 4, and perform computational near-miss searches in a Gaussian basis to approximate an infinite family of worldline constraints. 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, and benchmark our proxy bound model against representative analytic QEI formulations (e.g., Fewster's general worldline framework).</div> </div> |
| format | Recurso digital |
| id | zenodo_https___doi_org_10_5281_zenodo_18728106 |
| 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 formally verify convexity of the AQEI-admissible cone in Lean 4, and perform computational near-miss searches in a Gaussian basis to approximate an infinite family of worldline constraints. 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, and benchmark our proxy bound model against representative analytic QEI formulations (e.g., Fewster's general worldline framework).</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.18728106 |