4. The E8 Lattice
There are several equivalent definitions of the E_8 lattice. Below, we
formalise two of them and prove that they are equivalent.
-
Submodule.E8[complete]
We define the E_8 lattice as a subset of \R^8 by
\Lambda_8=\{(x_i)\in\Z^8\cup(\Z+\textstyle\frac12\displaystyle )^8|\;\sum_{i=1}^8x_i\equiv 0\;(\mathrm{mod\;2})\}.
Lean code for Definition4.1●1 definition
Associated Lean declarations
-
Submodule.E8[complete]
-
Submodule.E8[complete]
-
defdefined in SpherePacking/Basic/E8.leancomplete
def Submodule.E8.{u_2} (R : Type u_2) [Field R] [NeZero 2] : Submodule ℤ (Fin 8 → R)
def Submodule.E8.{u_2} (R : Type u_2) [Field R] [NeZero 2] : Submodule ℤ (Fin 8 → R)
-
E8Matrix[complete]
We define the E_8 basis vectors to be the set of vectors
\B_8 =
\left\{
\begin{bmatrix}
1 \\ -1 \\ 0 \\ 0 \\ 0 \\ 0 \\ 0 \\ 0
\end{bmatrix},
\begin{bmatrix}
0 \\ 1 \\ -1 \\ 0 \\ 0 \\ 0 \\ 0 \\ 0
\end{bmatrix},
\begin{bmatrix}
0 \\ 0 \\ 1 \\ -1 \\ 0 \\ 0 \\ 0 \\ 0
\end{bmatrix},
\begin{bmatrix}
0 \\ 0 \\ 0 \\ 1 \\ -1 \\ 0 \\ 0 \\ 0
\end{bmatrix},
\begin{bmatrix}
0 \\ 0 \\ 0 \\ 0 \\ 1 \\ -1 \\ 0 \\ 0
\end{bmatrix},
\begin{bmatrix}
0 \\ 0 \\ 0 \\ 0 \\ 0 \\ 1 \\ 1 \\ 0
\end{bmatrix},
\begin{bmatrix}
-1/2 \\ -1/2 \\ -1/2 \\ -1/2 \\ -1/2 \\ -1/2 \\ -1/2 \\ -1/2
\end{bmatrix},
\begin{bmatrix}
0 \\ 0 \\ 0 \\ 0 \\ 0 \\ 1 \\ -1 \\ 0
\end{bmatrix}
\right\}.
Lean code for Definition4.2●1 definition
Associated Lean declarations
-
E8Matrix[complete]
-
E8Matrix[complete]
-
defdefined in SpherePacking/Basic/E8.leancomplete
def E8Matrix.{u_2} (R : Type u_2) [Field R] : Matrix (Fin 8) (Fin 8) R
def E8Matrix.{u_2} (R : Type u_2) [Field R] : Matrix (Fin 8) (Fin 8) R
-
span_E8Matrix[complete]
The two definitions above coincide, i.e. \Lambda_8 = \mathrm{span}_{\Z}(\B_8).
Lean code for Theorem4.3●1 theorem
Associated Lean declarations
-
span_E8Matrix[complete]
-
span_E8Matrix[complete]
-
theoremdefined in SpherePacking/Basic/E8.leancomplete
theorem span_E8Matrix.{u_2} (R : Type u_2) [Field R] [CharZero R] : Submodule.span ℤ (Set.range (E8Matrix R).row) = Submodule.E8 R
theorem span_E8Matrix.{u_2} (R : Type u_2) [Field R] [CharZero R] : Submodule.span ℤ (Set.range (E8Matrix R).row) = Submodule.E8 R
We prove that each side contains the other.
/- source paragraph break -/
For a vector \vec{v} \in \Lambda_8 \subseteq \R^8, we have
\sum_i \vec{v}_i \equiv 0 \pmod{2} and all coordinates are either integers
or half-integers. After some modulo arithmetic, it can be seen that
\B_8^{-1}\vec{v} has integer coordinates, so
\vec{v} \in \mathrm{span}_{\Z}(\B_8).
/- source paragraph break -/
For the opposite direction, write
\vec{v} = \sum_i c_i\B_8^i \in \mathrm{span}_{\Z}(\B_8) with the
c_i integers and \B_8^i the i-th basis vector. Expanding the
definition 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 0 modulo 2 and that the coordinates are all
either integers or all half-integers.
/- source paragraph break -/
This proof does not depend on \B_8 being linearly independent.
In this section, we establish basic properties of the E_8 lattice and the
\B_8 vectors.
\B_8 is an \R-basis of \R^8. This uses Definition 4.2.
Lean code for Lemma4.4●1 theorem
Associated Lean declarations
-
span_E8Matrix_eq_top[complete]
-
span_E8Matrix_eq_top[complete]
-
theoremdefined in SpherePacking/Basic/E8.leancomplete
theorem span_E8Matrix_eq_top.{u_2} (R : Type u_2) [Field R] [NeZero 2] : Submodule.span R (Set.range (E8Matrix R).row) = ⊤
theorem span_E8Matrix_eq_top.{u_2} (R : Type u_2) [Field R] [NeZero 2] : Submodule.span R (Set.range (E8Matrix R).row) = ⊤
It suffices to prove that \B_8 \in \mathrm{GL}_8(\R).
We do this by explicitly defining the inverse matrix \B_8^{-1} and
proving \B_8 \B_8^{-1} = I_8, which implies that \det(\B_8) is
nonzero. See the Lean code for more details.
\Lambda_8 is an additive subgroup of \R^8.
Lean code for Lemma4.5●1 definition
Associated Lean declarations
-
E8Lattice[complete]
-
E8Lattice[complete]
-
abbrevdefined in SpherePacking/Basic/E8.leancomplete
abbrev E8Lattice : Submodule ℤ (EuclideanSpace ℝ (Fin 8))
abbrev E8Lattice : Submodule ℤ (EuclideanSpace ℝ (Fin 8))
This follows trivially from the fact that
\Lambda_8 \subseteq \R^8 is the \Z-span of \B_8 and hence an
additive group.
All vectors in \Lambda_8 have norm of the form \sqrt{2n}, where
n is a nonnegative integer. This uses Theorem 4.3.
Lean code for Lemma4.6●1 theorem
Associated Lean declarations
-
E8_norm_eq_sqrt_even[complete]
-
E8_norm_eq_sqrt_even[complete]
-
theoremdefined in SpherePacking/Basic/E8.leancomplete
theorem E8_norm_eq_sqrt_even (v : Fin 8 → ℝ) (hv : v ∈ Submodule.E8 ℝ) : ∃ n, Even n ∧ ↑n = ‖WithLp.toLp 2 v‖ ^ 2
theorem E8_norm_eq_sqrt_even (v : Fin 8 → ℝ) (hv : v ∈ Submodule.E8 ℝ) : ∃ n, Even n ∧ ↑n = ‖WithLp.toLp 2 v‖ ^ 2
Writing \vec{v} = \sum_i c_i\B_8^i, we have
\|v\|^2 = \sum_i \sum_j c_ic_j (\B_8^i \cdot \B_8^j).
Computing all 64 pairs of dot products and simplifying gives a large
quadratic form in the c_i with even integer coefficients, concluding the
proof.
c\Lambda_8 is discrete, that is, the subspace topology induced by its
inclusion into \R^8 is the discrete topology.
Lean code for Lemma4.7●1 theorem
Associated Lean declarations
-
instDiscreteE8Lattice[complete]
-
instDiscreteE8Lattice[complete]
-
theoremdefined in SpherePacking/Basic/E8.leancomplete
theorem instDiscreteE8Lattice : DiscreteTopology ↥E8Lattice
theorem instDiscreteE8Lattice : DiscreteTopology ↥E8Lattice
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 existence of an open ball \B(\sqrt{2}) \subseteq \R^8 around zero
containing no other lattice points, since the shortest nonzero vector has norm
\sqrt{2}.
c\Lambda_8 is a \Z-lattice, that is, it is discrete and spans
\R^8 over \R.
Lean code for Lemma4.8●1 theorem
Associated Lean declarations
-
instIsZLatticeE8Lattice[complete]
-
instIsZLatticeE8Lattice[complete]
-
theoremdefined in SpherePacking/Basic/E8.leancomplete
theorem instIsZLatticeE8Lattice : IsZLattice ℝ E8Lattice
theorem instIsZLatticeE8Lattice : IsZLattice ℝ E8Lattice
Prove E_8 is unimodular.
Prove E_8 is positive-definite.
The E_8 sphere packing is the (periodic) sphere packing with separation
\sqrt{2}, whose set of centres is \Lambda_8.
Lean code for Definition4.9●1 definition
Associated Lean declarations
-
E8Packing[complete]
-
E8Packing[complete]
-
defdefined in SpherePacking/Basic/E8.leancomplete
def E8Packing : PeriodicSpherePacking 8
def E8Packing : PeriodicSpherePacking 8
-
E8Basis_volume[complete]
\Vol{\Lambda_8} = \mathrm{Covol}(\R^8 / \Lambda_8) = 1.
Lean code for Lemma4.10●1 theorem
Associated Lean declarations
-
E8Basis_volume[complete]
-
E8Basis_volume[complete]
-
theoremdefined in SpherePacking/Basic/E8.leancomplete
theorem E8Basis_volume : MeasureTheory.volume (ZSpan.fundamentalDomain (E8Basis ℝ)) = 1
theorem E8Basis_volume : MeasureTheory.volume (ZSpan.fundamentalDomain (E8Basis ℝ)) = 1
TODO: In theory this should follow directly from \det(\Lambda_8) = 1, but
Lean hates me and EuclideanSpace is being annoying.
-
E8Packing_density[complete]
We have \Delta_{\mathcal{P}(E_8)} = \frac{\pi^4}{384}.
Lean code for Theorem4.11●1 theorem
Associated Lean declarations
-
E8Packing_density[complete]
-
E8Packing_density[complete]
-
theoremdefined in SpherePacking/Basic/E8.leancomplete
theorem E8Packing_density : E8Packing.density = ENNReal.ofReal Real.pi ^ 4 / 384
theorem E8Packing_density : E8Packing.density = ENNReal.ofReal Real.pi ^ 4 / 384
By Theorem 3.5, we have
\Delta_{\mathcal{P}(E_8)} = |E_8 / E_8| \cdot \frac{\Vol{\mathcal{B}_8(\sqrt{2} / 2)}}{\mathrm{Covol}(E_8)} = \frac{\pi^4}{384},
where the last equality follows from Lemma 4.10 and the
formula for volume of a ball:
\Vol{\mathcal{B}_d(R)} = R^d \pi^{d / 2} / \Gamma\left(\frac{d}{2} + 1\right).