# Symplectic ball packing in higher dimensions

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

- [Symplectic Ball Packings in Higher Dimensions](../../preprints/Symplectic-Ball-Packings-in-Higher-Dimensions-September-23-2026/paper.pdf)

## Scope

The formalization proves Siegel and Yao's ball-packing criterion in every symplectic dimension $2n$ with $n\ge3$. For $k\ge1$ closed standard balls of positive capacities $R_1,\ldots,R_k$, disjoint symplectic embeddings into the interior of a ball of capacity $R$ exist exactly when
$\sum_i R_i^n<R^n$ and $R_i+R_j<R$ for all $i\ne j$.
Capacity is $\pi$ times squared Euclidean radius, and each embedding is defined on a neighborhood of its closed source ball. The linked statements include both the full equivalence and the necessity direction.

## Comparator links

| Result | Comparator statement |
| --- | --- |
| Exact criterion for higher-dimensional symplectic ball packings | [BallPacking.lean](../ComparatorChallenges/BallPacking.lean) |
| Necessity of the volume and pairwise capacity inequalities | [BallPackingNecessity.lean](../ComparatorChallenges/BallPackingNecessity.lean) |