Roots of the Golay Construction A lattice

The norm-two vectors of TauCeti.BinaryGolay.constructionALattice are precisely the forty-eight vectors ±2 eᵢ. Its twenty-four positive coordinate roots have Gram matrix 2 I, so these roots form twenty-four mutually orthogonal copies of A₁. In particular its minimum is two and its kissing number is forty-eight.

References

• G. Nebe, Extremal lattices, slides 10–11, for the Golay code lattice and its minimal vectors.

def TauCeti.BinaryGolay.coordinateRoot (i : Fin 24) : ↥constructionALattice.carrier

The positive coordinate root 2 eᵢ of the Golay Construction A lattice.

@[simp]

theorem TauCeti.BinaryGolay.coe_coordinateRoot (i : Fin 24) : ↑(coordinateRoot i) = Pi.single i 2

The coordinates of a positive Golay lattice root.

@[simp]

theorem TauCeti.BinaryGolay.form_coordinateRoot_coordinateRoot (i j : Fin 24) : (constructionALattice.form ↑(coordinateRoot i)) ↑(coordinateRoot j) = if i = j then 2 else 0

The positive coordinate roots have Gram matrix 2 I: different coordinates give orthogonal copies of the root system A₁.

@[simp]

theorem TauCeti.BinaryGolay.norm_coordinateRoot (i : Fin 24) : constructionALattice.norm ↑(coordinateRoot i) = 2

Every positive coordinate root has norm two.

@[simp]

theorem TauCeti.BinaryGolay.integralNorm_coordinateRoot (i : Fin 24) : constructionALattice.integralNorm (coordinateRoot i) = 2

Every positive coordinate root has integral norm two.

theorem TauCeti.BinaryGolay.norm_eq_two_iff {x : Fin 24 → ℚ} (hx : x ∈ constructionALattice.carrier) : constructionALattice.norm x = 2 ↔ ∃ (i : Fin 24), x = Pi.single i 2 ∨ x = -Pi.single i 2

Classification of the Golay lattice roots. With the halved dot product, an ambient vector in the Golay lattice has norm two exactly when it is 2 eᵢ or -2 eᵢ.

theorem TauCeti.BinaryGolay.mem_vectorsOfNorm_two_iff (x : ↥constructionALattice.carrier) : x ∈ constructionALattice.vectorsOfNorm 2 ↔ ∃ (i : Fin 24), x = coordinateRoot i ∨ x = -coordinateRoot i

The norm-two shell consists of the positive coordinate roots and their negatives.

theorem TauCeti.BinaryGolay.span_vectorsOfNorm_two : Submodule.span ℤ ((fun (x : ↥constructionALattice.carrier) => ↑x) '' constructionALattice.vectorsOfNorm 2) = (ConstructionA.zeroLattice 2 (Fin 24)).carrier

The roots generate exactly the zero-code sublattice 2 ℤ²⁴. Thus the root lattice has no additional glue coming from nonzero Golay codewords.

noncomputable def TauCeti.BinaryGolay.rootLatticeIsometry : (IntegralLattice.a1.coordinatePower (Fin 24)).Isometry (ConstructionA.zeroLattice 2 (Fin 24))

The Golay root lattice is A₁²⁴. The zero-code lattice generated by all Golay roots is isometric to the orthogonal sum of twenty-four copies of the existing A₁ lattice. The ambient isometry doubles every coordinate.

@[simp]

theorem TauCeti.BinaryGolay.rootLatticeIsometry_apply (x : Fin 24 → ℚ) : rootLatticeIsometry x = 2 • x

The A₁²⁴ root-lattice identification doubles the standard coordinates.

noncomputable def TauCeti.BinaryGolay.rootsEquiv : Fin 24 × Bool ≃ ↑(constructionALattice.vectorsOfNorm 2)

The forty-eight roots, indexed by a coordinate and a sign. The Boolean value false selects 2 eᵢ, and true selects -2 eᵢ.

@[simp]

theorem TauCeti.BinaryGolay.rootsEquiv_apply (i : Fin 24) (b : Bool) : ↑(rootsEquiv (i, b)) = if b = true then -coordinateRoot i else coordinateRoot i

The explicit root indexing recovers the chosen signed coordinate root.

theorem TauCeti.BinaryGolay.representationNumber_constructionALattice_two : constructionALattice.representationNumber 2 = 48

The Golay lattice has forty-eight norm-two vectors.

theorem TauCeti.BinaryGolay.minimum_constructionALattice : constructionALattice.minimum = 2

The Golay lattice has minimum two.

theorem TauCeti.BinaryGolay.kissingNumber_constructionALattice : constructionALattice.kissingNumber = 48

The forty-eight coordinate roots are precisely the shortest nonzero Golay lattice vectors, so its kissing number is forty-eight.