Two-neighbors

For a lattice vector v of norm divisible by four, the two-neighbor of L along v is the general neighbor TauCeti.IntegralLattice.neighbor at p = 2. It is obtained by keeping the vectors pairing evenly with v (the neighbor kernel TauCeti.IntegralLattice.neighborKernel at p = 2) and adjoining v / 2. This file shows that its carrier is the union of the even-pairing kernel and the translate of that kernel by v / 2.

The general results specialise as follows. When L is even and the norm of v is divisible by eight, the two-neighbor is even (TauCeti.IntegralLattice.isEven_neighbor). When some lattice vector pairs oddly with v (Int.isCoprime_two_right), the two-neighbor is a Kneser two-neighbor (TauCeti.IntegralLattice.isNeighbor_neighbor). Then it is unimodular when L is (TauCeti.IntegralLattice.IsNeighbor.isUnimodular).

Main results

• TauCeti.IntegralLattice.mem_neighbor_two_carrier_iff_mem_or_sub_mem: the two-neighbor is the union of the even-pairing kernel and its translate by v / 2.

References

• G. Nebe, Extremal lattices, slide 11, for the two-neighbor construction of the Leech lattice.
• R. E. Borcherds, The Leech lattice and other lattices, §0.2, for the even-pairing kernel.

@[simp]

theorem TauCeti.IntegralLattice.mem_neighbor_two_carrier_iff_mem_or_sub_mem {V : Type u_1} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) {v : ↥L.carrier} (hv : 2 ^ 2 ∣ L.integralNorm v) (x : V) : x ∈ (neighbor 2 v hv).carrier ↔ x ∈ L.neighborKernel 2 v ∨ x - 2⁻¹ • ↑v ∈ L.neighborKernel 2 v

The two-neighbor is the union of the even-pairing kernel and the translate of that kernel by v / 2.