A sharp minimum for cube-apex bodies in every dimension
Hanyue Shen, Pavel B. Dubovski
math.MG
Oct 7, 2026 · v1
TL;DR
Lean 4 formalizes the actual-volume minimum (as an IsLeast statement), its attainment, the equality structure, and both extension bounds.
Abstract
We determine the minimum volume product of centrally symmetric polytopes obtained by adding facet apices to a cube while fixing their total outward height. Heights and tangential coordinates vary subject to a product condition on the polar-cap denominators. In every dimension at least two, the minimum has an explicit formula, attained by concentrating the height at one opposite pair of corner apices. For positive height in dimensions at least three, every minimizing array has this structure. The product condition strictly extends coordinatewise quadratic constraints. We also obtain two bounds without that condition: a four-dimensional Mahler bound for a specified height range, and a correction measuring volume generated jointly by two apices. The latter certifies a continuous family outside the preceding sufficient conditions. The proof combines known cap volumes with a sharp aggregate height estimate and a double-pyramid construction. Lean 4 verifies the actual-volume minimum, the necessary equality structure and both extensions.
Problem
The work determines the minimum volume product |P||P°| for centrally symmetric polytopes formed by adding facet apices to the cube [-1,1]^n, with the total outward height fixed and a product condition imposed on the polar-cap denominators. This setting is connected to the symmetric Mahler conjecture.
Approach
Lower bounds on the primal volume come from disjoint facet pyramids. Lower bounds on the polar volume come from a cap union bound built on known one-vertex cap volumes, combined with a sharp aggregate height estimate. A double-pyramid cell construction captures the extra volume generated jointly by two apices. The main results are verified in Lean 4 with pinned dependencies, using only the standard axioms.
Results
An explicit minimum c_n F_n(A) holds in every dimension n≥2. It is attained by concentrating all the height at one opposite pair of corner apices, and this minimizer is unique up to symmetry for n≥3 and A>0. The paper also proves a four-dimensional Mahler bound for A≤11/4, plus a two-apex correction that certifies a continuous family of examples lying outside the earlier sufficient conditions.
