The congruence model of the Leech lattice and its minimum

The Leech lattice Λ ⊆ ℚ^(Fin 24), glued from the Golay Construction B lattice K along the odd shift s = (-3/2, 1/2, …, 1/2), has the following integral description. A vector x lies in Λ exactly when x = a / 2 for an integer vector a = 2b + m 𝟙 with m ∈ {0, 1}, the reduction of b modulo two a Golay codeword, and ∑ aᵢ ≡ 4m (mod 8). The case m = 0 is the half-lattice K itself; the case m = 1 is the coset s + K, since a / 2 - s is the integer vector b + 2 e₀.

In these coordinates the norm, the dot product halved, is B(x, x) = ∑ aᵢ² / 8. The four-case bound ∑ aᵢ² ≥ 32 for nonzero admissible a, which uses only the minimum distance 8 and the divisibility by four of the Golay weights, then shows that every nonzero vector of Λ has norm at least 4. The shift s has norm exactly 4, so the minimum of the Leech lattice is 4. In particular the Leech lattice has no roots: it has no vector of norm 2, and its root sublattice is zero. No theta series, sphere-packing bound, or uniqueness theorem is used.

Main declarations

• TauCeti.mem_leechLattice_carrier_iff_exists: the congruence model of the Leech lattice.
• TauCeti.leechLattice_norm_intCast_div_two: the norm ∑ aᵢ² / 8 in congruence coordinates.
• TauCeti.four_le_norm_leechLattice: every nonzero vector of the Leech lattice has norm ≥ 4.
• TauCeti.minimum_leechLattice: the minimum of the Leech lattice is 4.
• TauCeti.vectorsOfNorm_two_leechLattice and TauCeti.span_vectorsOfNorm_two_leechLattice: the Leech lattice has no roots, and its root sublattice is zero.

References

• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 4, §11, and Chapter 10, §1.
• R. A. Wilson, The Finite Simple Groups, §5.4.

theorem TauCeti.mem_leechLattice_carrier_iff_exists (x : Fin 24 → ℚ) : x ∈ leechLattice.carrier ↔ ∃ (m : ℤ), (m = 0 ∨ m = 1) ∧ ∃ (b : Fin 24 → ℤ), (fun (i : Fin 24) => ↑(b i)) ∈ BinaryGolay.code ∧ ∑ i : Fin 24, (2 * b i + m) ≡ 4 * m [ZMOD 8] ∧ x = fun (i : Fin 24) => ↑(2 * b i + m) / 2

The congruence model of the Leech lattice. A vector x lies in the Leech lattice exactly when x = a / 2 for an integer vector a = 2b + m 𝟙 with m ∈ {0, 1}, b reducing to a Golay codeword modulo two, and ∑ aᵢ ≡ 4m (mod 8).

theorem TauCeti.leechLattice_norm_intCast_div_two (a : Fin 24 → ℤ) : (leechLattice.norm fun (i : Fin 24) => ↑(a i) / 2) = ↑(∑ i : Fin 24, a i ^ 2) / 8

The norm in congruence coordinates: the Leech lattice norm of a / 2 is ∑ aᵢ² / 8.

theorem TauCeti.four_le_norm_leechLattice {x : Fin 24 → ℚ} (hx : x ∈ leechLattice.carrier) (hne : x ≠ 0) : 4 ≤ leechLattice.norm x

Every nonzero vector of the Leech lattice has norm at least four. In congruence coordinates x = a / 2 this is the four-case bound ∑ aᵢ² ≥ 32.

instance TauCeti.instNontrivialLeechLattice : Nontrivial ↥leechLattice.carrier

The Leech lattice is nontrivial: it contains the nonzero odd shift.

@[simp]

theorem TauCeti.minimum_leechLattice : leechLattice.minimum = 4

The minimum of the Leech lattice is four: every nonzero vector has norm at least 4, and the odd shift has norm exactly 4.

@[simp]

theorem TauCeti.vectorsOfNorm_two_leechLattice : leechLattice.vectorsOfNorm 2 = ∅

The Leech lattice has no roots: it has no vector of norm 2.

theorem TauCeti.span_vectorsOfNorm_two_leechLattice : Submodule.span ℤ ((fun (x : ↥leechLattice.carrier) => ↑x) '' leechLattice.vectorsOfNorm 2) = ⊥

The root sublattice of the Leech lattice is zero: the span of its norm-2 vectors in the ambient space is trivial.