Sphere Packing in R^8

4. The E8 Lattice🔗

Definition4.1
Group: Equivalent models of the <missing> lattice. (2)
Hover another entry in this group to preview it.
Preview
Definition 4.2
Blueprint label
  • «E8-Matrix»
Group
  • Equivalent models of the <missing> lattice.
AL∃∀Nused by 0

Define E_8 as vectors in \mathbb{R}^8 with even coordinate sum and either all integer or all half-integer coordinates.

Code for Definition4.1●1 definition, incomplete
  • axiom 
    Submodule.E8 : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    Submodule.E8 : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Direct algebraic definition.

Definition4.2
Group: Equivalent models of the <missing> lattice. (2)
Hover another entry in this group to preview it.
Preview
Definition 4.1
Blueprint label
  • «E8-Set»
Group
  • Equivalent models of the <missing> lattice.
AL∃∀Nused by 0

Define the explicit basis matrix whose \mathbb{Z}-span gives the same lattice.

Code for Definition4.2●1 definition, incomplete
  • axiom 
    E8Matrix : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    E8Matrix : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Direct matrix-level definition.

Theorem4.3
Group: Equivalent models of the <missing> lattice. (2)
Hover another entry in this group to preview it.
Preview
Definition 4.1
Blueprint label
  • «E8-Set»
Group
  • Equivalent models of the <missing> lattice.
AL∃∀Nused by 1

The two definitions coincide: set-based characterization equals \mathbb{Z}-span of the basis matrix.

Code for Theorem4.3●1 definition, incomplete
  • axiom 
    span_E8Matrix : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    span_E8Matrix : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Show each side contains the other by explicit coordinate arithmetic.

Lemma4.4
Group: Basic structural and arithmetic properties of <missing> . (4)
Hover another entry in this group to preview it.
Preview
Lemma 4.5
Blueprint label
  • «E8-Lattice»
Group
  • Basic structural and arithmetic properties of <missing> .
AL∃∀Nused by 0

The E_8 basis matrix spans all of \mathbb{R}^8 over \mathbb{R}.

Code for Lemma4.4●1 definition, incomplete
  • axiom 
    span_E8Matrix_eq_top : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    span_E8Matrix_eq_top : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Prove the matrix is invertible.

Lemma4.5
Group: Basic structural and arithmetic properties of <missing> . (4)
Hover another entry in this group to preview it.
Preview
Lemma 4.4
Blueprint label
  • «E8-is-basis»
Group
  • Basic structural and arithmetic properties of <missing> .
AL∃∀Nused by 0

E_8 is a lattice in \mathbb{R}^8.

Code for Lemma4.5●1 definition, incomplete
  • axiom 
    E8Lattice : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    E8Lattice : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Use Theorem 4.3 and subgroup closure.

Lemma4.6
Group: Basic structural and arithmetic properties of <missing> . (4)
Hover another entry in this group to preview it.
Preview
Lemma 4.4
Blueprint label
  • «E8-is-basis»
Group
  • Basic structural and arithmetic properties of <missing> .
AL∃∀Nused by 0

Every lattice vector has norm \sqrt{2n} for some nonnegative integer n.

Code for Lemma4.6●1 definition, incomplete
  • axiom 
    E8_norm_eq_sqrt_even : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    E8_norm_eq_sqrt_even : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Expand the norm-square as an even integral quadratic form.

Lemma4.7
Group: Basic structural and arithmetic properties of <missing> . (4)
Hover another entry in this group to preview it.
Preview
Lemma 4.4
Blueprint label
  • «E8-is-basis»
Group
  • Basic structural and arithmetic properties of <missing> .
AL∃∀Nused by 0

E_8 is discrete.

Code for Lemma4.7●1 definition, incomplete
  • axiom 
    instDiscreteE8Lattice : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    instDiscreteE8Lattice : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

The minimal nonzero norm gives an open neighborhood containing only zero.

Lemma4.8
Group: Basic structural and arithmetic properties of <missing> . (4)
Hover another entry in this group to preview it.
Preview
Lemma 4.4
Blueprint label
  • «E8-is-basis»
Group
  • Basic structural and arithmetic properties of <missing> .
AL∃∀Nused by 0

E_8 is a \mathbb{Z}-lattice.

Code for Lemma4.8●1 definition, incomplete
  • axiom 
    instIsZLatticeE8Lattice : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    instIsZLatticeE8Lattice : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Combine discreteness and spanning.

Definition4.9
Group: Definition and density computation of the <missing> sphere packing. (2)
Hover another entry in this group to preview it.
Preview
Lemma 4.10
Blueprint label
  • «E8Packing-covol»
Group
  • Definition and density computation of the <missing> sphere packing.
AL∃∀Nused by 0

Define the E_8 sphere packing with separation \sqrt{2} and centers E_8.

Code for Definition4.9●1 definition, incomplete
  • axiom 
    E8Packing : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    E8Packing : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Direct construction from the lattice.

Lemma4.10
Group: Definition and density computation of the <missing> sphere packing. (2)
Hover another entry in this group to preview it.
Preview
Definition 4.9
Blueprint label
  • E8Packing
Group
  • Definition and density computation of the <missing> sphere packing.
AL∃∀Nused by 1

The covolume of E_8 is 1.

Code for Lemma4.10●1 definition, incomplete
  • axiom 
    E8Basis_volume : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    E8Basis_volume : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Compute the determinant of the basis matrix.

Theorem4.11
Group: Definition and density computation of the <missing> sphere packing. (2)
Hover another entry in this group to preview it.
Preview
Definition 4.9
Blueprint label
  • E8Packing
Group
  • Definition and density computation of the <missing> sphere packing.
AL∃∀Nused by 0

\Delta_{\mathcal{P}(E_8)} = \pi^4 / 384.

Code for Theorem4.11●1 definition, incomplete
  • axiom 
    E8Packing_density : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    E8Packing_density : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Apply Theorem 3.5 together with Lemma 4.10.