2026/08/05 by David Victor Feldman
Mathematics · #math.MG #math.OC #msc:52A40 #msc:52A20 #msc:52A38 #msc:68U05 #msc:68V20
13 pages, LEAN 4 verified (modulo one classical result)
arxiv created 2026/08/05 · arxiv updated 2026/08/06
Given finitely many compact convex bodies in \Rn, one seeks translates maximizing the volume of their common intersection. A lazy solver merely translates each body so as to place its centroid at the origin. We prove that the lazy strategy always captures strictly more than (\tfrac2n+1)n of the optimal volume, and that this constant is sharp: families of cones over tangent disks, indexed by finite nets on the sphere, approach it. The infimum is not attained. For two convex bodies in the plane the resulting sharp constant 4/9 closes a gap open since 1996, when de Berg, Cheong, Devillers, van Kreveld and Teillaud proved that centroid alignment of two convex polygons captures at least 9/25 of the maximum overlap and exhibited examples capturing only 4/9. The proof rests on the following identity: for a convex body K with centroid at the origin, the intersection of all centroid-recentered compact convex supersets of K equals \tfrac1n+1(K-K). We close with a promise-problem variant in which the lazy strategy captures at least (\tfracnn+1)n > \tfrac1e of the optimum, uniformly in the dimension. All results below have been checked in Lean~4; the one classical input quoted rather than proved is the equality case of the Brunn--Minkowski inequality, which enters only for n≥2.