Sphere Packing in R^8

2. Sphere Packings🔗

The high-level plan follows Viazovska (2017) and Cohn and Elkies (2003).

Definition2.1
Group: Definitions of sphere packings, density, and the optimization target. (3)
Hover another entry in this group to preview it.
Preview
Definition 2.2
Blueprint label
  • «SpherePacking.finiteDensity»
Group
  • Definitions of sphere packings, density, and the optimization target.
AL∃∀Nused by 0

Given centers X \subseteq \mathbb{R}^d and separation radius r > 0, define the packing \mathcal{P}(X) as the union of open radius-r balls at points of X.

Code for Definition2.1●1 definition, incomplete
  • axiom 
    SpherePacking.balls : PropThe universe of propositions. `Prop ≡ Sort 0`.

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

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

This is the foundational geometric object used throughout the blueprint.

Definition2.2
Group: Definitions of sphere packings, density, and the optimization target. (3)
Hover another entry in this group to preview it.
Preview
Definition 2.1
Blueprint label
  • «SpherePacking.balls»
Group
  • Definitions of sphere packings, density, and the optimization target.
AL∃∀Nused by 0

For R > 0, the finite density is \Delta_{\mathcal{P}}(R) = \mathrm{Vol}(\mathcal{P} \cap B_d(0,R)) / \mathrm{Vol}(B_d(0,R)).

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

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

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

Direct definition.

Definition2.3
Group: Definitions of sphere packings, density, and the optimization target. (3)
Hover another entry in this group to preview it.
Preview
Definition 2.1
Blueprint label
  • «SpherePacking.balls»
Group
  • Definitions of sphere packings, density, and the optimization target.
AL∃∀Nused by 0

The packing density is the limit superior \Delta_{\mathcal{P}} := \limsup_{R \to \infty} \Delta_{\mathcal{P}}(R).

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

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

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

Direct definition.

Definition2.4
Group: Definitions of sphere packings, density, and the optimization target. (3)
Hover another entry in this group to preview it.
Preview
Definition 2.1
Blueprint label
  • «SpherePacking.balls»
Group
  • Definitions of sphere packings, density, and the optimization target.
AL∃∀Nused by 0

Define the sphere packing constant \Delta_d as the supremum of densities over all sphere packings in \mathbb{R}^d.

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

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

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

Direct definition.

Definition2.5
Group: Scaling invariance of finite density and asymptotic density. (3)
Hover another entry in this group to preview it.
Preview
Lemma 2.6
Blueprint label
  • «SpherePacking.scale_finiteDensity»
Group
  • Scaling invariance of finite density and asymptotic density.
AL∃∀Nused by 0

For c > 0, scaling a packing \mathcal{P}(X) gives \mathcal{P}(cX).

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

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

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

Direct definition.

Lemma2.6
Group: Scaling invariance of finite density and asymptotic density. (3)
Hover another entry in this group to preview it.
Preview
Definition 2.5
Blueprint label
  • «SpherePacking.scale»
Group
  • Scaling invariance of finite density and asymptotic density.
AL∃∀Nused by 1

Finite density is scale-covariant: \Delta_{\mathcal{P}(cX)}(cR) = \Delta_{\mathcal{P}(X)}(R).

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

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

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

By scaling Lebesgue measure in dimension d.

Lemma2.7
Group: Scaling invariance of finite density and asymptotic density. (3)
Hover another entry in this group to preview it.
Preview
Definition 2.5
Blueprint label
  • «SpherePacking.scale»
Group
  • Scaling invariance of finite density and asymptotic density.
AL∃∀Nused by 1

Asymptotic density is scale-invariant.

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

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

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

Apply Lemma 2.6 and pass to limit superior.

Lemma2.8
Group: Scaling invariance of finite density and asymptotic density. (3)
Hover another entry in this group to preview it.
Preview
Definition 2.5
Blueprint label
  • «SpherePacking.scale»
Group
  • Scaling invariance of finite density and asymptotic density.
AL∃∀Nused by 0

The same supremum can be computed over unit-separation packings.

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

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

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

Use Lemma 2.7 to normalize every packing.

Definition2.9
Group: Periodic and lattice packings as a reduced optimization class. (4)
Hover another entry in this group to preview it.
Preview
Definition 2.10
Blueprint label
  • «def:dual-lattice»
Group
  • Periodic and lattice packings as a reduced optimization class.
AL∃∀Nused by 0

A \mathbb{Z}-lattice in \mathbb{R}^d is a discrete additive subgroup spanning the ambient space.

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

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

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

Standard lattice definition.

Definition2.10
Group: Periodic and lattice packings as a reduced optimization class. (4)
Hover another entry in this group to preview it.
Preview
Definition 2.9
Blueprint label
  • IsZLattice
Group
  • Periodic and lattice packings as a reduced optimization class.
AL∃∀Nused by 0

Define the dual lattice with respect to the Euclidean bilinear pairing.

Code for Definition2.10●1 definition, incomplete
  • axiom 
    LinearMap.BilinForm.dualSubmodule : PropThe universe of propositions. `Prop ≡ Sort 0`.

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

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

Direct linear-algebraic definition.

Definition2.11
Group: Periodic and lattice packings as a reduced optimization class. (4)
Hover another entry in this group to preview it.
Preview
Definition 2.9
Blueprint label
  • IsZLattice
Group
  • Periodic and lattice packings as a reduced optimization class.
AL∃∀Nused by 0

A periodic packing is a sphere packing with centers invariant under translation by a lattice.

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

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

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

Direct structure-level definition.

Definition2.12
Group: Periodic and lattice packings as a reduced optimization class. (4)
Hover another entry in this group to preview it.
Preview
Definition 2.9
Blueprint label
  • IsZLattice
Group
  • Periodic and lattice packings as a reduced optimization class.
AL∃∀Nused by 0

Define the periodic sphere packing constant as the supremum over periodic packings.

Code for Definition2.12●1 definition, incomplete
  • axiom 
    PeriodicSpherePackingConstant : PropThe universe of propositions. `Prop ≡ Sort 0`.

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

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

Direct definition.

Theorem2.13
Group: Periodic and lattice packings as a reduced optimization class. (4)
Hover another entry in this group to preview it.
Preview
Definition 2.9
Blueprint label
  • IsZLattice
Group
  • Periodic and lattice packings as a reduced optimization class.
AL∃∀N
Used by 2
Hover a use site to preview it.
Preview
Corollary 2.15
Blueprint label
  • «corollary:upper-bound-E8»
Uses target in
  • proof

The periodic sphere packing constant equals the unrestricted sphere packing constant.

Code for Theorem2.13●1 definition, incomplete
  • axiom 
    periodic_constant_eq_constant : PropThe universe of propositions. `Prop ≡ Sort 0`.

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

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

Reduction by approximation of arbitrary packings with periodic ones.

Theorem2.14
Group: Reduction from Cohn-Elkies bounds to the final dimension-8 theorem. (2)
Hover another entry in this group to preview it.
Preview
Corollary 2.15
Blueprint label
  • «corollary:upper-bound-E8»
Group
  • Reduction from Cohn-Elkies bounds to the final dimension-8 theorem.
XL∃∀Nused by 1

Assuming the Cohn-Elkies optimal auxiliary function and the computed density of the E_8 packing, we obtain the upper bound \Delta_8 \leq \Delta_{\mathcal{P}(E_8)}.

Proof

Apply the global Cohn-Elkies inequality to the normalized optimal function.

Corollary2.15
Group: Reduction from Cohn-Elkies bounds to the final dimension-8 theorem. (2)
Hover another entry in this group to preview it.
Preview
Theorem 2.14
Blueprint label
  • «theorem:CE_Main»
Group
  • Reduction from Cohn-Elkies bounds to the final dimension-8 theorem.
XL∃∀Nused by 1

The sphere packing constant in dimension 8 is bounded above by the E_8 lattice packing density.

Proof

Combine Theorem 2.14 with Theorem 2.13.

Corollary2.16
Group: Reduction from Cohn-Elkies bounds to the final dimension-8 theorem. (2)
Hover another entry in this group to preview it.
Preview
Theorem 2.14
Blueprint label
  • «theorem:CE_Main»
Group
  • Reduction from Cohn-Elkies bounds to the final dimension-8 theorem.
AL∃∀Nused by 0

\Delta_8 = \Delta_{\mathcal{P}(E_8)}.

Code for Corollary2.16●1 definition, incomplete
  • axiom 
    SpherePacking.MainTheorem : PropThe universe of propositions. `Prop ≡ Sort 0`.

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

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

Use Corollary 2.15 and the matching lower bound from the explicit E_8 packing construction.