Levels of the checkerboard lattices

For positive n, the checkerboard lattice Dₙ has level 8 / gcd(n, 4). Thus its level is 8 in odd rank, 4 in rank congruent to 2 modulo 4, and 2 in rank divisible by 4. For n ≥ 4 this is the type D root lattice, whose simple-root Gram matrix is identified in TypeD.SimpleRoots.

The four discriminant classes computed in TypeD.Basic have quadratic values 0, 1/2, n/8, and n/8. The level must annihilate all four values, not merely the discriminant group. This gives the least common multiple of their reduced denominators using IntegralLattice.IsEven.level_dvd_iff.

References

• W. Ebeling, Lattices and Codes, Chapters 1 and 3.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, §4.7.1.

@[simp]

theorem TauCeti.IntegralLattice.level_checkerboardLattice (n : ℕ) [NeZero n] : (checkerboardLattice n).level = 8 / n.gcd 4

The level of a positive-rank checkerboard lattice is 8 / gcd(n, 4).

theorem TauCeti.IntegralLattice.level_checkerboardLattice_of_odd {n : ℕ} (hn : Odd n) : (checkerboardLattice n).level = 8

An odd-rank checkerboard lattice has level 8.

theorem TauCeti.IntegralLattice.level_checkerboardLattice_of_mod_four_eq_two {n : ℕ} (hn : n % 4 = 2) : (checkerboardLattice n).level = 4

A checkerboard lattice of rank congruent to 2 modulo 4 has level 4.

theorem TauCeti.IntegralLattice.level_checkerboardLattice_of_four_dvd {n : ℕ} [NeZero n] (hn : 4 ∣ n) : (checkerboardLattice n).level = 2

A positive-rank checkerboard lattice with rank divisible by 4 has level 2.