Sign changes preserve the checkerboard lattice

Changing the signs of some coordinates of ℚⁿ maps the checkerboard carrier Dₙ onto itself: it keeps a vector integral, and changes its coordinate sum by twice the sum of the negated coordinates. Together with TauCeti.dotProduct_signedEquiv, this makes every such sign change a symmetry of the checkerboard lattice.

Main results

• TauCeti.IntegralLattice.signedEquiv_mem_checkerboardCarrier_iff: a sign change of coordinates preserves membership in Dₙ.

References

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

theorem TauCeti.IntegralLattice.signedEquiv_mem_checkerboardCarrier {n : ℕ} (u : Fin n → ℤˣ) {x : Fin n → ℚ} (hx : x ∈ checkerboardCarrier n) : (signedEquiv u (Equiv.refl (Fin n))) x ∈ checkerboardCarrier n

A sign change of coordinates maps Dₙ into itself: it changes the coordinate sum by an even integer.

theorem TauCeti.IntegralLattice.signedEquiv_mem_checkerboardCarrier_iff {n : ℕ} (u : Fin n → ℤˣ) (x : Fin n → ℚ) : (signedEquiv u (Equiv.refl (Fin n))) x ∈ checkerboardCarrier n ↔ x ∈ checkerboardCarrier n

A sign change of coordinates preserves membership in Dₙ.