# Sharp projection-body inequalities and a counterexample to simplex maximization

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

- [Petty’s projection-volume conjecture in dimensions at least four](../../preprints/Pettys-projection-volume-conjecture-in-dimensions-at-least-four-September-24-2026/paper.pdf)
- [A product counterexample to the simplex maximum for projection-body volume](../../preprints/A-product-counterexample-to-the-simplex-maximum-for-projection-body-volume-September-24-2026/paper.pdf)

## Scope

Petty's projection-volume conjecture predicts

$\displaystyle \frac{|\Pi K|}{|K|^{n-1}}\ge \kappa_{n-1}^{n}\kappa_n^{2-n},$

with equality exactly for ellipsoids; here $\kappa_j$ is the volume of the Euclidean unit ball in dimension $j$. The formalization establishes this for every convex body $K\subset\mathbb R^n$ and every $n\ge4$.

Other inequalities in the projection-body family are not included.

Brannen's simplex-maximization conjecture predicts that a simplex maximizes normalized projection-body volume $|\Pi K|/|K|^{n-1}$ in dimension $n$. The formalized counterexample is the product of two ten-dimensional simplices. Its normalized projection volume, divided by that of a twenty-dimensional simplex, is

$\displaystyle \frac{22{,}355{,}476}{22{,}020{,}096}>1.$

Thus the proposed maximum fails in dimension $20$. The paper's exponential-factor result for every sufficiently large dimension is not included.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Petty's projection-volume inequality | [PettyProjectionVolume.lean](../ComparatorChallenges/PettyProjectionVolume.lean) |
| Failure of the simplex upper bound in dimension 20 | [ProjectionCounterexample.lean](../ComparatorChallenges/ProjectionCounterexample.lean) |
| Explicit product-of-simplices counterexample | [ProjectionVolume.lean](../ComparatorChallenges/ProjectionVolume.lean) |