Short vectors of Construction B and of its odd shifted coset

Let C be a binary linear code with coordinates ι. This file proves the two elementary norm bounds behind the absence of roots in the Construction B model of the Leech lattice. They are stated for integer vectors, in the coordinates in which the congruence conditions are read off.

• The Construction B vectors. If every nonzero codeword of C has weight at least eight, then every nonzero integer vector z reducing into C modulo two, with 4 ∣ ∑ zᵢ, satisfies ∑ zᵢ² ≥ 8. If z reduces to a nonzero codeword, at least eight coordinates are odd. If it reduces to zero, then z = 2w with ∑ wᵢ even. Since wᵢ² ≡ wᵢ (mod 2), the positive integer ∑ wᵢ² is even, so it is at least two.
• The odd shifted coset. If C is doubly even and 8 ∣ #ι, then every vector a = 2z + 𝟙 with z reducing into C modulo two and ∑ aᵢ ≡ 4 (mod 8) satisfies ∑ aᵢ² ≥ #ι + 8. Each aᵢ² - 1 = 4 zᵢ (zᵢ + 1) is a nonnegative multiple of eight. If all of them vanish, then every aᵢ is ±1, and the coordinates equal to -1 are the support of the reduction c of z. Then ∑ aᵢ = #ι - 2 wt(c) ≡ 0 (mod 8), since 4 ∣ wt(c). This contradicts the sum congruence.

In the Construction A form, the dot product halved, the first bound says that a nonzero vector of the Construction B carrier has norm at least 4 (four_le_form_self).

Main declarations

• TauCeti.ConstructionB.eight_le_sum_sq: the bound for Construction B vectors.
• TauCeti.ConstructionB.four_le_form_self: the same bound for the halved dot product.
• TauCeti.ConstructionB.card_add_eight_le_sum_sq: the bound for the odd shifted coset.

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.ConstructionB.eight_le_sum_sq {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} (hC : ∀ c ∈ C, c ≠ 0 → 8 ≤ hammingNorm c) {z : ι → ℤ} (hz : (fun (i : ι) => ↑(z i)) ∈ C) (hsum : 4 ∣ ∑ i : ι, z i) (hne : z ≠ 0) : 8 ≤ ∑ i : ι, z i ^ 2

Construction B vectors are not short. If every nonzero codeword of C has weight at least eight, a nonzero integer vector reducing into C modulo two whose coordinate sum is divisible by four has squared length at least eight.

theorem TauCeti.ConstructionB.four_le_form_self {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} (hC : ∀ c ∈ C, c ≠ 0 → 8 ≤ hammingNorm c) {x : ι → ℚ} (hx : x ∈ lattice C) (hne : x ≠ 0) : 4 ≤ ((ConstructionA.form 2) x) x

Construction B vectors have norm at least four. If every nonzero codeword of C has weight at least eight, every nonzero vector of the Construction B carrier has Construction A norm, the dot product halved, at least 4.

theorem TauCeti.ConstructionB.card_add_eight_le_sum_sq {ι : Type u_1} [Fintype ι] {C : LinearCode (ZMod 2) ι} (hC : BinaryCode.IsDoublyEven C) (hι : 8 ∣ Fintype.card ι) {z : ι → ℤ} (hz : (fun (i : ι) => ↑(z i)) ∈ C) (hsum : ∑ i : ι, (2 * z i + 1) ≡ 4 [ZMOD 8]) : ↑(Fintype.card ι) + 8 ≤ ∑ i : ι, (2 * z i + 1) ^ 2

The odd shifted coset of Construction B is not short. If C is doubly even and the length is divisible by eight, every odd vector a = 2z + 𝟙 with z reducing into C modulo two and ∑ aᵢ ≡ 4 (mod 8) has squared length at least the length plus eight.