Shortest vectors in the discriminant cosets of Dₙ

The discriminant group of the checkerboard lattice Dₙ consists of the classes of 0, of the vector representative v = eₙ, of the spinor representative s = (1/2, …, 1/2) and of the cospinor representative c = s - eₙ. This file computes the minimum norm of each nonzero coset, together with the vectors attaining it:

• the vector coset v + Dₙ consists of the integer vectors with odd coordinate sum; its minimum norm is 1, attained exactly by the 2n vectors ±eᵢ;
• the spinor and cospinor cosets consist of the vectors with all coordinates in ℤ + 1/2, split by the parity of the coordinate sum of x - s; their minimum norm is n / 4, attained exactly by the vectors with all coordinates ±1/2 whose number of negative coordinates is even (for s) or odd (for c).

These are the shortest-norm values attached to the Conway–Sloane glue labels [2] = v, [1] = s and [3] = c of a Dₙ component, the input for bounding the norm of a glue vector in an orthogonal sum of root lattices. The minima are stated as IsLeast over the norms of the actual dual-lattice vectors in each discriminant class, so they record attainment as well as the lower bound.

Main results

• TauCeti.IntegralLattice.div_four_le_checkerboardLattice_form_self: vectors with all coordinates in ℤ + 1/2 have norm at least n / 4.
• TauCeti.IntegralLattice.isLeast_form_self_checkerboardVectorClass, isLeast_form_self_checkerboardSpinorClass, isLeast_form_self_checkerboardCospinorClass: the minimum norms 1, n / 4 and n / 4 of the three nonzero cosets.
• TauCeti.IntegralLattice.isLeast_form_self_zmodTwoProdAddEquivCheckerboardDiscriminantGroup, isLeast_form_self_zmodFourAddEquivCheckerboardDiscriminantGroup: the same minima, indexed by the label of the class in ℤ/2 × ℤ/2 (even n) or ℤ/4 (odd n).
• TauCeti.IntegralLattice.sub_checkerboardVector_mem_and_form_self_eq_one_iff, sub_checkerboardSpinor_mem_and_form_self_eq_iff, sub_checkerboardCospinor_mem_and_form_self_eq_iff: the minimal vectors of each coset.

References

• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, §4.7.1 and Chapter 16, §1.

The vector coset

theorem TauCeti.IntegralLattice.sub_checkerboardVector_mem_and_form_self_eq_one_iff {n : ℕ} [NeZero n] (x : Fin n → ℚ) : x - checkerboardVector n ∈ checkerboardCarrier n ∧ ((checkerboardLattice n).form x) x = 1 ↔ ∃ (i : Fin n), x = Pi.single i 1 ∨ x = -Pi.single i 1

The minimal vectors of the vector coset. A vector x with x - v ∈ Dₙ has norm one exactly when it is one of the 2n vectors ±eᵢ.

theorem TauCeti.IntegralLattice.isLeast_form_self_checkerboardVectorClass {n : ℕ} [NeZero n] : IsLeast {q : ℚ | ∃ (x : ↥(checkerboardLattice n).dualCarrier), Submodule.Quotient.mk x = checkerboardVectorClass n ∧ ((checkerboardLattice n).form ↑x) ↑x = q} 1

The minimum norm of the vector coset of Dₙ is 1: it is attained by v = eₙ and bounds the norm of every dual vector in the vector class.

The spinor and cospinor cosets

theorem TauCeti.IntegralLattice.div_four_le_checkerboardLattice_form_self {n : ℕ} {x : Fin n → ℚ} (hx : ∀ (i : Fin n), ∃ (z : ℤ), x i = ↑z + 1 / 2) : ↑n / 4 ≤ ((checkerboardLattice n).form x) x

Vectors with all coordinates in ℤ + 1/2 have norm at least n / 4, since each coordinate has square at least 1 / 4.

theorem TauCeti.IntegralLattice.div_four_le_checkerboardLattice_form_self_of_sub_checkerboardSpinor_mem {n : ℕ} {x : Fin n → ℚ} (hx : x - checkerboardSpinor n ∈ checkerboardCarrier n) : ↑n / 4 ≤ ((checkerboardLattice n).form x) x

Vectors of the spinor coset have norm at least n / 4.

theorem TauCeti.IntegralLattice.div_four_le_checkerboardLattice_form_self_of_sub_checkerboardCospinor_mem {n : ℕ} [NeZero n] {x : Fin n → ℚ} (hx : x - checkerboardCospinor n ∈ checkerboardCarrier n) : ↑n / 4 ≤ ((checkerboardLattice n).form x) x

Vectors of the cospinor coset have norm at least n / 4.

theorem TauCeti.IntegralLattice.sub_checkerboardSpinor_mem_and_form_self_eq_iff {n : ℕ} (x : Fin n → ℚ) : x - checkerboardSpinor n ∈ checkerboardCarrier n ∧ ((checkerboardLattice n).form x) x = ↑n / 4 ↔ (∀ (i : Fin n), x i = 1 / 2 ∨ x i = -(1 / 2)) ∧ Even {i : Fin n | x i = -(1 / 2)}.card

The minimal vectors of the spinor coset. A vector x with x - s ∈ Dₙ has norm n / 4 exactly when all of its coordinates are ±1/2 and an even number of them are negative.

theorem TauCeti.IntegralLattice.sub_checkerboardCospinor_mem_and_form_self_eq_iff {n : ℕ} [NeZero n] (x : Fin n → ℚ) : x - checkerboardCospinor n ∈ checkerboardCarrier n ∧ ((checkerboardLattice n).form x) x = ↑n / 4 ↔ (∀ (i : Fin n), x i = 1 / 2 ∨ x i = -(1 / 2)) ∧ Odd {i : Fin n | x i = -(1 / 2)}.card

The minimal vectors of the cospinor coset. A vector x with x - c ∈ Dₙ has norm n / 4 exactly when all of its coordinates are ±1/2 and an odd number of them are negative.

theorem TauCeti.IntegralLattice.isLeast_form_self_checkerboardSpinorClass {n : ℕ} : IsLeast {q : ℚ | ∃ (x : ↥(checkerboardLattice n).dualCarrier), Submodule.Quotient.mk x = checkerboardSpinorClass n ∧ ((checkerboardLattice n).form ↑x) ↑x = q} (↑n / 4)

The minimum norm of the spinor coset of Dₙ is n / 4: it is attained by s = (1/2, …, 1/2) and bounds the norm of every dual vector in the spinor class.

theorem TauCeti.IntegralLattice.isLeast_form_self_checkerboardCospinorClass {n : ℕ} [NeZero n] : IsLeast {q : ℚ | ∃ (x : ↥(checkerboardLattice n).dualCarrier), Submodule.Quotient.mk x = checkerboardCospinorClass n ∧ ((checkerboardLattice n).form ↑x) ↑x = q} (↑n / 4)

The minimum norm of the cospinor coset of Dₙ is n / 4: it is attained by c = (1/2, …, 1/2, -1/2) and bounds the norm of every dual vector in the cospinor class.

Minima indexed by labels

theorem TauCeti.IntegralLattice.isLeast_form_self_zmodTwoProdAddEquivCheckerboardDiscriminantGroup {n : ℕ} [NeZero n] (hn : Even n) (b : ZMod 2 × ZMod 2) : IsLeast {q : ℚ | ∃ (x : ↥(checkerboardLattice n).dualCarrier), Submodule.Quotient.mk x = (zmodTwoProdAddEquivCheckerboardDiscriminantGroup n hn) b ∧ ((checkerboardLattice n).form ↑x) ↑x = q} (if b = 0 then 0 else if b = (1, 0) then 1 else ↑n / 4)

The minimum norm of each discriminant class of Dₙ, n even. The class labelled b : ZMod 2 × ZMod 2 by zmodTwoProdAddEquivCheckerboardDiscriminantGroup has minimum norm 0 for b = 0, 1 for the vector label (1, 0), and n / 4 for the spinor and cospinor labels (0, 1) and (1, 1).

theorem TauCeti.IntegralLattice.isLeast_form_self_zmodFourAddEquivCheckerboardDiscriminantGroup {n : ℕ} (hn : Odd n) (b : ZMod 4) : IsLeast {q : ℚ | ∃ (x : ↥(checkerboardLattice n).dualCarrier), Submodule.Quotient.mk x = (zmodFourAddEquivCheckerboardDiscriminantGroup n hn) b ∧ ((checkerboardLattice n).form ↑x) ↑x = q} (if b = 0 then 0 else if b = 2 then 1 else ↑n / 4)

The minimum norm of each discriminant class of Dₙ, n odd. The class labelled b : ZMod 4 by zmodFourAddEquivCheckerboardDiscriminantGroup has minimum norm 0 for b = 0, 1 for the vector label 2, and n / 4 for the spinor and cospinor labels 1 and 3.