Triangular-lattice covering radius

This module converts the unit-square quadratic estimate into a covering-radius theorem for the triangular lattice and defines the chosen nearest lattice cell.

theorem HadwigerNelsonBounds.exists_lattice_point_within_circumradius (p : R2) : ∃ (q : ℤ × ℤ), dist p (isbellLatticePoint q.1 q.2) ≤ isbellLatticeStep / √3

Voronoi covering radius (the geometric heart of (G1)).

Constructive proof: given p ∈ R², compute lattice coordinates s := p₀/a − p₁/(a√3), t := 2·p₁/(a√3). Let i₀ := ⌊s⌋, j₀ := ⌊t⌋, α := s − i₀ ∈ [0, 1), β := t − j₀ ∈ [0, 1). The squared distance from p to lattice point (i₀ + Δi, j₀ + Δj) is a²·Q(α − Δi, β − Δj) where Q(u, v) = u² + uv + v².

The unit square [0, 1]² is covered by four Voronoi cells centered at (0,0), (1,0), (0,1), (1,1) in (α, β) space. In each cell, the corresponding Q value is ≤ 1/3. Case-split on the cell.

noncomputable def HadwigerNelsonBounds.nearestLatticeIdx (p : R2) : ℤ × ℤ

The lattice coordinates of a lattice point within the Voronoi circumradius of p. Built via classical choice on exists_lattice_point_within_circumradius.

Equations

• HadwigerNelsonBounds.nearestLatticeIdx p = ⋯.choose

theorem HadwigerNelsonBounds.nearestLatticeIdx_spec (p : R2) : dist p (isbellLatticePoint (nearestLatticeIdx p).1 (nearestLatticeIdx p).2) ≤ isbellLatticeStep / √3

The defining property of nearestLatticeIdx: it lies within the Voronoi circumradius.

noncomputable def HadwigerNelsonBounds.toFin7 (n : ℤ) : Fin 7

Cast an integer residue modulo seven to the corresponding finite color.

Equations

• HadwigerNelsonBounds.toFin7 n = (ZMod.finEquiv 7).symm ↑n

noncomputable def HadwigerNelsonBounds.isbellColor : R2 → Fin 7

The Isbell 7-coloring assigns to each point p ∈ R² the color (i + 3·j) mod 7, where (i, j) = nearestLatticeIdx p are the integer coordinates of a nearest lattice point.

Equations

• HadwigerNelsonBounds.isbellColor p = HadwigerNelsonBounds.toFin7 ((HadwigerNelsonBounds.nearestLatticeIdx p).1 + 3 * (HadwigerNelsonBounds.nearestLatticeIdx p).2)

The remaining geometric fact

theorem HadwigerNelsonBounds.dist_le_voronoi_circumradius (p : R2) : dist p (isbellLatticePoint (nearestLatticeIdx p).1 (nearestLatticeIdx p).2) ≤ isbellLatticeStep / √3

(G1) Voronoi covering radius. Every point of R² lies within distance a/√3 of its assigned lattice point.

Immediate corollary of exists_lattice_point_within_circumradius: by construction nearestLatticeIdx is chosen to satisfy this.