← All papers
First page of Arranging convex bodies for maximum intersection volume: the sharp efficiency of centroid alignment

Arranging convex bodies for maximum intersection volume: the sharp efficiency of centroid alignment

David Victor Feldman

math.MG Aug 5, 2026 · v1 math.OC
All results, including sharp intersection-volume bounds for centroid-aligned convex bodies, verified in Lean 4 against Mathlib v4.28.0.
Given finitely many compact convex bodies in $\R^n$, 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 $\left(\tfrac{2}{n+1}\right)^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 $\tfrac{1}{n+1}(K-K)$. We close with a promise-problem variant in which the lazy strategy captures at least $\left(\tfrac{n}{n+1}\right)^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\ge2$.

Given finitely many compact convex bodies in R^n, one seeks translates maximizing the volume of their common intersection. The question is how efficient the lazy strategy of aligning centroids at the origin is relative to the optimum.

The authors prove that centroid alignment always captures strictly more than (2/(n+1))^n of the optimal volume and that this constant is sharp. The proof rests on an identity: for a convex body K centered at the origin, the intersection of all centroid-recentered compact convex supersets equals (1/(n+1))(K-K). A promise-problem variant is also analyzed. The full formal development was carried out in Lean 4 using the Aristotle system and builds against mathlib4.

The sharp constant (2/(n+1))^n is established, closing a gap open since 1996 where the planar two-body constant is 4/9. Under an offcenter promise, the lazy strategy captures at least (n/(n+1))^n > 1/e uniformly in dimension. Formalization revealed that an appeal to the Brunn–Minkowski equality case was unnecessary for the extremal identification.