Convex Cone of Energy Tensors under AQEI: Formal Verification and Computational Exploration

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.