Voronoi quadratic-form bounds

This module proves that one of the four corners of a lattice-coordinate unit square lies within the required quadratic-form radius.

theorem HadwigerNelsonBounds.unitSquare_has_near_lattice_corner {α β : ℝ} (hαLower : 0 ≤ α) (hαUpper : α < 1) (hβLower : 0 ≤ β) (hβUpper : β < 1) : ∃ (Δi : ℤ) (Δj : ℤ), (α - ↑Δi) ^ 2 + (α - ↑Δi) * (β - ↑Δj) + (β - ↑Δj) ^ 2 ≤ 1 / 3

Every point of the half-open lattice-coordinate unit square lies within quadratic-form radius 1 / 3 of one of its four corners.