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

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).