AI 中文总结
研究n维空间中有限紧凸体平移最大化公共相交体积问题，证明质心对齐的简易策略能获得严格多于(2/(n+1))ⁿ的最优体积且常数精确，填补平面两凸体4/9常数的长期空白，结果经Lean 4验证。
AI 中文摘要
给定$\reals^n$中有限个紧凸体，人们寻求使它们的公共相交体积最大的平移方式。一种简易求解器仅将每个凸体平移，使其质心置于原点。我们证明，这种简易策略总能获得严格多于$\bigl(\frac{2}{n+1}\bigr)^n$的最优体积，且该常数是精确的：由球面上有限网格索引的、切圆盘上的锥族可逼近该常数。此下确界无法取到。对于平面中的两个凸体，得到的精确常数$4/9$填补了自1996年以来的空白，当时de Berg、Cheong、Devillers、van Kreveld和Teillaud证明，两个凸多边形的质心对齐至少能获得$9/25$的最大重叠，并给出了仅获得$4/9$的例子。证明基于以下恒等式：对于质心在原点的凸体$K$，所有以质心为中心的$K$的紧凸超集的交集等于$\frac{1}{n+1}(K-K)$。最后我们提出一个允诺问题变体，其中简易策略至少能获得$\bigl(\frac{n}{n+1}\bigr)^n > \frac{1}{e}$的最优值，且与维度无关。以下所有结果均已在Lean 4中验证；唯一被引用而非证明的经典结论是Brunn–Minkowski不等式的等号情形，该情形仅在$n\neq2$时用到。
英文摘要
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$.
Comments13 pages, LEAN 4 verified (modulo one classical result)
