The Construction B lattice of the extended binary Golay code

Construction B applied to the extended binary Golay code is the lattice of integer vectors in ℚ^(Fin 24) reducing to a Golay codeword modulo two and having coordinate sum divisible by four, with the halved dot product. It is the kernel of half the coordinate sum modulo two on the unimodular Golay Construction A lattice, so it has index two there and discriminant four. It is positive definite, even, and of rank 24.

This is the half-lattice of the Construction B model of the Leech lattice: the Leech lattice is the union of it and one odd shifted coset. Every nonzero vector of the half-lattice has norm at least 4. Under the congruence conditions describing the Leech lattice in the coordinates x = a / 2, every nonzero admissible integer vector a has ∑ aᵢ² ≥ 32. Both bounds use the minimum distance 8 of the Golay code; the second also uses the divisibility of its weights by four.

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.

noncomputable def TauCeti.BinaryGolay.constructionBLattice : IntegralLattice (Fin 24 → ℚ)

The Construction B lattice of the extended binary Golay code: the integer vectors of ℚ^(Fin 24) reducing to a Golay codeword modulo two whose coordinate sum is divisible by four, with the dot product halved.

@[simp]

theorem TauCeti.BinaryGolay.constructionBLattice_carrier : constructionBLattice.carrier = ConstructionB.lattice code

The Golay Construction B carrier is the Construction B carrier of the Golay code.

@[simp]

theorem TauCeti.BinaryGolay.constructionBLattice_form : constructionBLattice.form = ConstructionA.form 2

The Golay Construction B form is the halved coordinate dot product.

theorem TauCeti.BinaryGolay.constructionBLattice_carrier_le : constructionBLattice.carrier ≤ constructionALattice.carrier

The Golay Construction B lattice is a sublattice of the Golay Construction A lattice.

theorem TauCeti.BinaryGolay.relIndex_constructionBLattice : constructionBLattice.carrier.toAddSubgroup.relIndex constructionALattice.carrier.toAddSubgroup = 2

The Golay Construction B lattice has index two in the Golay Construction A lattice.

instance TauCeti.BinaryGolay.instIsNondegenerateConstructionBLattice : constructionBLattice.IsNondegenerate

The Golay Construction B lattice is nondegenerate.

@[simp]

theorem TauCeti.BinaryGolay.finrank_constructionBLattice : Module.finrank ℤ ↥constructionBLattice.carrier = 24

The Golay Construction B lattice has rank 24.

theorem TauCeti.BinaryGolay.isPosDef_constructionBLattice : constructionBLattice.IsPosDef

The Golay Construction B lattice is positive definite.

theorem TauCeti.BinaryGolay.isEven_constructionBLattice : constructionBLattice.IsEven

The Golay Construction B lattice is even.

@[simp]

theorem TauCeti.BinaryGolay.discriminant_constructionBLattice : constructionBLattice.discriminant = 4

The Golay Construction B lattice has discriminant four, being of index two in the unimodular Golay Construction A lattice.

@[simp]

theorem TauCeti.BinaryGolay.natCard_discriminantGroup_constructionBLattice : Nat.card constructionBLattice.DiscriminantGroup = 4

The discriminant group of the Golay Construction B lattice has order four.

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

The Golay Construction B lattice has no nonzero vector of norm less than four, since the Golay code has minimum distance eight.

theorem TauCeti.BinaryGolay.thirtyTwo_le_sum_sq {m : ℤ} (hm : m = 0 ∨ m = 1) {b : Fin 24 → ℤ} (hb : (fun (i : Fin 24) => ↑(b i)) ∈ code) (hsum : ∑ i : Fin 24, (2 * b i + m) ≡ 4 * m [ZMOD 8]) (hne : (fun (i : Fin 24) => 2 * b i + m) ≠ 0) : 32 ≤ ∑ i : Fin 24, (2 * b i + m) ^ 2

The norm bound for the Leech lattice in congruence coordinates. Let m ∈ {0, 1} and let b be an integer vector reducing to a Golay codeword modulo two, and put a = 2b + m 𝟙. If ∑ aᵢ ≡ 4m (mod 8) and a ≠ 0, then ∑ aᵢ² ≥ 32. These are the congruence conditions that describe the Leech lattice in the coordinates x = a / 2, in which the halved dot product of x with itself is ∑ aᵢ² / 8; so the bound says that such an x has norm at least 4.