Plane unit-distance graph and triangular lattice

This module defines the Euclidean plane graph and the lattice geometry used by the seven-color construction.

@[reducible, inline]

abbrev HadwigerNelsonBounds.R2 : Type

The plane R² as a 2-dimensional Euclidean space.

Equations

• HadwigerNelsonBounds.R2 = EuclideanSpace ℝ (Fin 2)

def HadwigerNelsonBounds.unitDistanceGraph : SimpleGraph R2

The unit-distance graph on R²: vertices are points of the plane, with an edge between p and q iff dist p q = 1. Built via SimpleGraph.fromRel, which automatically symmetrizes the relation and removes self-loops (dist p p = 0 ≠ 1, so this is harmless).

Equations

• HadwigerNelsonBounds.unitDistanceGraph = SimpleGraph.fromRel fun (p q : HadwigerNelsonBounds.R2) => dist p q = 1

@[simp]

theorem HadwigerNelsonBounds.unitDistanceGraph_adj (p q : R2) : unitDistanceGraph.Adj p q ↔ p ≠ q ∧ (dist p q = 1 ∨ dist q p = 1)

Adjacency unfolds to: distinct points at distance exactly 1.

Isbell hexagonal-tiling 7-coloring

noncomputable def HadwigerNelsonBounds.isbellLatticeStep : ℝ

Lattice basis spacing. Any value in the interval (1/(√7 − 2/√3), √3/2) ≈ (0.671, 0.866) is geometrically valid; we pick the clean rational 3/4.

Equations

• HadwigerNelsonBounds.isbellLatticeStep = 3 / 4

noncomputable def HadwigerNelsonBounds.isbellLatticePoint (i j : ℤ) : R2

The triangular-lattice point at integer coords (i, j): i · (a, 0) + j · (a/2, a·√3/2).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HadwigerNelsonBounds.isbellLatticePoint_zero (i j : ℤ) : (isbellLatticePoint i j).ofLp 0 = ↑i * isbellLatticeStep + ↑j * (isbellLatticeStep / 2)

@[simp]

theorem HadwigerNelsonBounds.isbellLatticePoint_one (i j : ℤ) : (isbellLatticePoint i j).ofLp 1 = ↑j * (isbellLatticeStep * √3 / 2)

theorem HadwigerNelsonBounds.sqrt_three_mul_self : √3 * √3 = 3

√3 * √3 = 3, hoisted to file scope for use in the squared-distance computation.

theorem HadwigerNelsonBounds.isbellLatticePoint_dist_sq (i j i' j' : ℤ) : dist (isbellLatticePoint i j) (isbellLatticePoint i' j') ^ 2 = isbellLatticeStep ^ 2 * ((↑i - ↑i') ^ 2 + (↑i - ↑i') * (↑j - ↑j') + (↑j - ↑j') ^ 2)

Squared Euclidean distance between two lattice points.

theorem HadwigerNelsonBounds.dist_point_lattice_sq_cart (p : R2) (i j : ℤ) : dist p (isbellLatticePoint i j) ^ 2 = (p.ofLp 0 - (↑i * isbellLatticeStep + ↑j * (isbellLatticeStep / 2))) ^ 2 + (p.ofLp 1 - ↑j * (isbellLatticeStep * √3 / 2)) ^ 2

Squared Euclidean distance from a point p : R² to a lattice point. Helper formula expressed directly in terms of p 0, p 1, i, j.

theorem HadwigerNelsonBounds.Q_le_third_origin {α β : ℝ} (hα : 0 ≤ α) (hβ : 0 ≤ β) (h1 : 2 * α + β ≤ 1) (h2 : α + 2 * β ≤ 1) : α ^ 2 + α * β + β ^ 2 ≤ 1 / 3

The Voronoi covering bound Q(u, v) ≤ 1/3 holds in the centroid region of the triangle with vertices (0,0), (1,0), (0,1).