1 Sphere packings
The Sphere Packing problem is a classic optimisation problem with widespread applications that go well beyond mathematics. The task is to determine the “densest" possible arrangement of spheres in a given space. It remains unsolved in all but finitely many dimensions.
It was famously determined, in [ 12 ] , that the optimal arrangement in \(\mathbb {R}^8\) is given by the \(E_8\) lattice. The result is strongly dependent on the Cohn-Elkies linear programming bound (Theorem 3.1 in [ 3 ] ), which, if a \(\mathbb {R}^d \to \mathbb {R}\) function satisfying certain conditions exists, bounds the optimal density of sphere packings in \(\mathbb {R}^d\) in terms of it. The proof in [ 12 ] uses the theory of modular forms to construct a function that can be used to bound the density of all sphere packings in \(\mathbb {R}^8\) above by the density of the \(E_8\) lattice packing. This then allows us to conclude that no packing in \(\mathbb {R}^8\) can be denser than the \(E_8\) lattice packing.
1.1 The Setup
This subsection gives an overview for the setup of the problem, both informally and in Lean. Throughout this blueprint, \(\mathbb {R}^d\) will denote the Euclidean vector space equipped with distance \(\| \cdot \| \) and Lebesgue measure \(\mathrm{Vol}(\cdot )\). For any \(x\in \mathbb {R}^d\) and \(r\in \mathbb {R}_{{\gt}0}\), we denote by \(B_d(x,r)\) the open ball in \(\mathbb {R}^d\) with center \(x\) and radius \(r\). While we will give a more formal definition of a sphere packing below (and in Lean), the underlying idea is that it is a union of balls of equal radius centred at points that are far enough from each other that the balls do not overlap.
Arguably the most important definition in this subsection is that of packing density, which measures which portion of \(d\)-dimensional Euclidean space is covered by a given sphere packing. Taking the supremum over all packings gives what we refer to as the sphere packing constant, which is the quantity we are interested in optimising.
Given a set \(X \subset \mathbb {R}^d\) and a real number \(r {\gt} 0\) (known as the separation radius) such that \(\| x - y\| \geq r\) for all distinct \(x, y \in X\), we define the sphere packing \(\mathcal{P}(X)\) with centres at \(X\) to be the union of all open balls of radius \(r\) centred at points in \(X\):
Note that a sphere packing is uniquely defined from a given set of centres (which, in order to be a valid set of centres, must admit a corresponding separation radius). Therefore, as a conscious choice during the formalisation process, we will define everything that depends on sphere packings in terms of SpherePacking, a structure that bundles all the identifying information of a packing, but not the actual balls themselves. For the purposes of this blueprint, however, we will refrain from making this distinction.
We now define a notion of density for bounded regions of space by considering the density inside balls of finite radius.
The finite density of a packing \(\mathcal{P}\) is defined as
As intuitive as it seems to take the density of a packing to be the limit of the finite densities as the radius of the ball goes to infinity, it is not immediately clear that this limit exists. Therefore, we define the density of a sphere packing as a limit superior instead.
We define the density of a packing \(\mathcal{P}\) as the limit superior
We may now define the sphere packing constant, the quantity that the sphere packing problem requires us to compute.
The sphere packing constant is defined as supremum of packing densities over all possible packings:
1.2 Scaling Sphere Packings
Given that the problem involves the arrangement of balls in space, it is intuitive not to worry about the radius of the balls (so long as they are all equal to each other). However, Definition 1.1 involves a choice of separation radius. In principle, we would want two sphere packing configurations that differ only in separation radii to ‘encode the same information’. In this brief subsection, we will describe how to change the separation radius of a sphere packing by scaling the packing by a positive real number and prove that this does not affect its density. This will give us the freedom to choose any separation radius we like when attempting to define the optimal sphere packing in \(\mathbb {R}^d\).
Given a sphere packing \(\mathcal{P}(X)\) with separation radius \(r\), we defined the scaled packing with respect to a real number \(c {\gt} 0\) to be the packing \(\mathcal{P}(cX)\), where \(cX = \left\{ cx \in V \; \middle | \; x \in X \right\} \) has separation radius \(cr\).
Let \(\mathcal{P}(X)\) be a sphere packing and \(c\) a positive real number. Then, for all \(R {\gt} 0\),
The proof follows by direct computation:
where the second equality follows from applying the fact that scaling a (measurable) set by a factor of \(c\) scales its volume by a factor of \(c^d\) to the fact that \(\mathcal{P}(cX) \cap B_d(0, cR) = c \cdot (\mathcal{P}(X) \cap B_d(0, cR))\).
Let \(\mathcal{P}(X)\) be a sphere packing and \(c\) a positive real number. Then, the density of the scaled packing \(\mathcal{P}(cX)\) is equal to the density of the original packing \(\mathcal{P}(X)\).
One can show, using relatively unsophisticated real analysis, that
Lemma 1.7 tells us that \(\Delta _{\mathcal{P}(cX)}(cR) = \Delta _{\mathcal{P}(X)}(R)\) for every \(R {\gt} 0\). Therefore,
where the second equality is the result of a similar change of variables to the one done above.
Therefore, as expected, we do not need to worry about the separation radius when constructing sphere packings. This will be useful when we attempt to construct the optimal sphere packing in \(\mathbb {R}^8\)—and even more so when attempting to formalise this construction—because the underlying structure of the packing is given by a set known as the \(E_8\) lattice, which has separation radius \(\sqrt{2}\).
We can also use Lemma 1.8 to simplify the computation of the sphere packing constant by taking the supremum not over all sphere packings but only over those with density \(1\).
That the supremum over packings of unit density is at most the sphere packing constant is obvious. For the reverse inequality, let \(\mathcal{P}(X)\) be any sphere packing with separation radius \(r\). We know, from Lemma 1.8, that the density of \(\mathcal{P}(X)\) is equal to that of the scaled packing \(\mathcal{P}\! \left(\frac{X}{r}\right)\). Since the scaled packing has separation radius \(1\), its density is naturally at most the supremum over all packings of unit density, meaning that the same is true of \(\mathcal{P}(X)\).
1.3 Lattices and Periodic packings
We begin by defining what a lattice is in Euclidean space.
We say that an additive subgroup \(\Lambda \leq \mathbb {R}^d\) is a lattice if it is discrete and its \(\mathbb {R}\)-span contains all the elements of \(\mathbb {R}^d\).
There is also a corresponding dual notion, which will become relevant when we start doing Fourier analysis on functions over lattices.
The dual lattice of a lattice \(\Lambda \) is the set
As one might expect,
The dual of a lattice is also a lattice.
Let \(\Lambda \) be a lattice and \(\Lambda ^*\) its dual. We need to show three things: that \(\Lambda ^*\) is an additive subgroup of \(\mathbb {R}^d\); that \(\Lambda ^*\) is discrete; and that the \(\mathbb {R}\)-span of \(\Lambda ^*\) contains all of \(\mathbb {R}^d\).
It is easy enough to see that \(\Lambda ^*\) is an additive subgroup of \(\mathbb {R}^d\): it clearly contains the zero vector (whose inner-product with any vector is zero), and is closed under addition and negation because the inner-product is bilinear and \(\mathbb {Z}\) is closed under addition and negation.
We say that a sphere packing \(\mathcal{P}(X)\) is (\(\Lambda \)-)periodic if there exists a lattice \(\Lambda \subset \mathbb {R}^d\) such that for all \(x \in X\) and \(y \in \Lambda \), \(x + y \in X\) (ie, \(X\) is \(\Lambda \)-periodic).
There is a natural definition of density for periodic sphere packings, namely the “local” density of balls in a fundamental domain. However, a priori the density of sphere packing above need not to coincide with this alternative definition. In theorem 2.5, we will prove that this is the case.
Now that we have simplified the process of computing the packing densities of specific packings, we can simplify that of computing the sphere packing constant. It turns out that once again, periodicity is key.
The periodic sphere packing constant is defined to be
For all \(d\), the periodic sphere packing constant in \(\mathbb {R}^d\) is equal to the sphere packing constant in \(\mathbb {R}^d\).
redState this in Lean (ready). redFill in proof here (see [ 3 , Appendix A ] )
Thus, one can show a sphere packing to be optimal by showing its density to be equal to the periodic sphere packing constant instead of the regular sphere packing constant. The determination of the periodic constant is easier than that of the general constant, as we shall see when investigating the Linear Programming bounds derived by Cohn and Elkies in [ 3 ] .
1.4 Main Result
With the terminologies above, we can state the main theorem of this project.
All periodic packing \(\mathcal{P} \subseteq \mathbb {R}^8\) has density satisfying \(\Delta _{\mathcal{P}} \leq \Delta _{E_8} = \frac{\pi ^4}{384}\), the density of the \(E_8\) sphere packing (see definition 3.9).
Directly follows from Theorem 5.1 applied to the function \(f(x)=g(x/\sqrt{2})\) of Theorem 5.2.
All packing \(\mathcal{P} \subseteq \mathbb {R}^8\) has density satisfying \(\Delta _{\mathcal{P}} \leq \Delta _{E_8}\).
This is a direct consequence of Theorem theorem 1.15 and theorem 1.16.
\(\Delta _8 = \Delta _{E_8}\).
By definition, \(\Delta _{E_8} \leq \Delta _8\), while corollary 1.17 shows \(\Delta _8 = \sup _{\mathrm{packing} \, \mathcal{P}} \leq \Delta _{E_8}\), and the result follows.