Separation of equally colored lattice points

This module proves the modular quadratic-form estimate that separates distinct lattice points carrying the same residue color.

theorem HadwigerNelsonBounds.dist_between_same_color_lattice_points {i j i' j' : ℤ} (hne : (i, j) ≠ (i', j')) (hsame : ↑i + 3 * ↑j = ↑i' + 3 * ↑j') : dist (isbellLatticePoint i j) (isbellLatticePoint i' j') ≥ isbellLatticeStep * √7

(G2) Same-color lattice separation. Two distinct lattice points with the same (i + 3·j) mod 7 color are at Euclidean distance at least a·√7.

Proof: if (i, j) ≠ (i', j') and (i + 3·j) ≡ (i' + 3·j') (mod 7), then (Δi, Δj) := (i − i', j − j') is a nonzero integer vector with Δi + 3·Δj ≡ 0 (mod 7). The Euclidean length squared of Δi·v₁ + Δj·v₂ is a²·(Δi² + Δi·Δj + Δj²). By sublattice_quadratic_form_ge_seven, the integer quadratic form Δi² + Δi·Δj + Δj² ≥ 7, so squared distance ≥ 7·a², giving distance ≥ a·√7.