3 The \(E_8\) lattice
3.1 Definitions of \(E_8\) lattice
There are several equivalent definitions of the \(E_8\) lattice. Below, we formalise two of them, and prove they are equivalent.
(\(E_8\)-lattice, Definition 1)We define the \(E_8\)-lattice (as a subset of \(\mathbb {R}^8\)) to be
(\(E_8\)-lattice, Definition 2)We define the \(E_8\) basis vectors to be the set of vectors
The two definitions above coincide, i.e. \(\Lambda _8 = \mathrm{span}_{\mathbb {Z}}(\mathcal{B}_8)\).
We prove each side contains the other side.
For a vector \(\vec{v} \in \Lambda _8 \subseteq \mathbb {R}^8\), we have \(\sum _i \vec{v}_i \equiv 0 \pmod{2}\) and \(\vec{v}_i\) being either all integers or all half-integers. After some modulo arithmetic, it can be seen that \(\mathcal{B}_8^{-1}\vec{v}\) as integer coordinates (i.e. it is congruent to \(0\) modulo \(1\)). Hence, \(\vec{v} \in \mathrm{span}_{\mathbb {Z}}(\mathcal{B}_8)\).
For the opposite direction, we write the vector as \(\vec{v} = \sum _i c_i\mathcal{B}_8^i \in \mathrm{span}_{\mathbb {Z}}(\mathcal{B}_8)\) with \(c_i\) being integers and \(\mathcal{B}_8^i\) being the \(i\)-th basis vector. Expanding the definition then gives \(\vec{v} = \left(c_1 - \frac{1}{2}c_7, -c_1 + c_2 - \frac{1}{2}c_7, \cdots , -\frac{1}{2}c_7\right)\). Again, after some modulo arithmetic, it can be seen that \(\sum _i \vec{v}_i\) is indeed \(0\) modulo \(2\) and are all either integers and half-integers, concluding the proof.
(Note: this proof doesn’t depend on that \(\mathcal{B}_8\) is linearly independent.)
3.2 Basic Properties of \(E_8\) lattice
In this section, we establish basic properties of the \(E_8\) lattice and the \(\mathcal{B}_8\) vectors.
\(B_8\) is a \(\mathbb {R}\)-basis of \(\mathbb {R}^8\).
It suffices to prove that \(\mathcal{B}_8 \in \mathrm{GL}_8(\mathbb {R})\). We prove this by explicitly defining the inverse matrix \(\mathcal{B}_8^{-1}\) and proving \(\mathcal{B}_8 \mathcal{B}_8^{-1} = I_8\), which implies that \(\det (\mathcal{B}_8)\) is nonzero. See the Lean code for more details.,
\(\Lambda _8\) is an additive subgroup of \(\mathbb {R}^8\).
Trivially follows from that \(\Lambda _8 \subseteq \mathbb {R}^8\) is the \(\mathbb {Z}\)-span of \(\mathcal{B}_8\) and hence an additive group.
All vectors in \(\Lambda _8\) have norm of the form \(\sqrt{2n}\), where \(n\) is a nonnegative inteeger.
Writing \(\vec{v} = \sum _i c_i\mathcal{B}_8^i\), we have \(\| v\| ^2 = \sum _i \sum _j c_ic_j (\mathcal{B}_8^i \cdot \mathcal{B}_8^j)\). Computing all \(64\) pairs of dot products and simplifying, we get a massive term that is a quadratic form in \(c_i\) with even integer coefficients, concluding the proof.
\(c\Lambda _8\) is discrete, i.e. that the subspace topology induced by its inclusion into \(\mathbb {R}^8\) is the discrete topology.
Since \(\Lambda _8\) is a topological group and \(+\) is continuous, it suffices to prove that \(\{ 0\} \) is open in \(\Lambda _8\). This follows from the fact that there is an open ball \(\mathcal{B}(\sqrt{2}) \subseteq \mathbb {R}^8\) around it containing no other lattice points, since the shortest nonzero vector has norm \(\sqrt{2}\).
\(c\Lambda _8\) is a \(\mathbb {Z}\)-lattice, i.e. it is discrete and spans \(\mathbb {R}^8\) over \(\mathbb {R}\).
redProve \(E_8\) is unimodular. redProve \(E_8\) is positive-definite.
3.3 The \(E_8\) sphere packing
The \(E_8\) sphere packing is the (periodic) sphere packing with separation \(\sqrt{2}\), whose set of centres is \(\Lambda _8\).
\(\operatorname {Vol}\! \left(\Lambda _8\right) = \mathrm{Covol}(\mathbb {R}^8 / \Lambda _8) = 1\).
redIn theory this should follow directly from \(\det (\Lambda _8) = 1\), but Lean hates me and EuclideanSpace is being annoying.
We have \(\Delta _{\mathcal{P}(E_8)} = \frac{\pi ^4}{384}\).
By theorem 2.5, we have \(\Delta _{\mathcal{P}(E_8)} = |E_8 / E_8| \cdot \frac{\operatorname {Vol}\! \left(\mathcal{B}_8(\sqrt{2} / 2)\right)}{\mathrm{Covol}(E_8)} = \frac{\pi ^4}{384}\), where the last equality follows from lemma 3.10 and the formula for volume of a ball: \(\operatorname {Vol}\! \left(\mathcal{B}_d(R)\right) = R^d \pi ^{d / 2} / \Gamma \left(\frac{d}{2} + 1\right)\).