Isbell's seven-coloring

This module proves the numerical gap estimates, constructs the plane coloring, and establishes the seven-color upper bound.

Numerical inequalities

theorem HadwigerNelsonBounds.isbell_voronoi_diameter_lt_one : 2 * (isbellLatticeStep / √3) < 1

The within-tile diameter 2·(a/√3) = √3/2 is < 1.

theorem HadwigerNelsonBounds.isbell_same_color_min_gt_one : isbellLatticeStep * (√7 - 2 / √3) > 1

The same-color spacing a·(√7 − 2/√3) > 1 for a = 3/4.

The proper-coloring theorem

theorem HadwigerNelsonBounds.isbell_isProperColoring {p q : R2} : unitDistanceGraph.Adj p q → isbellColor p ≠ isbellColor q

The Isbell coloring is proper. Two points at unit distance receive different colors.

noncomputable def HadwigerNelsonBounds.isbellColoring : unitDistanceGraph.Coloring (Fin 7)

Bundle the Isbell witness into a SimpleGraph.Coloring.

Equations

• HadwigerNelsonBounds.isbellColoring = SimpleGraph.Coloring.mk HadwigerNelsonBounds.isbellColor ⋯

theorem HadwigerNelsonBounds.chromaticNumber_le_seven : unitDistanceGraph.Colorable 7

Upper bound — χ(R²) ≤ 7. The unit-distance graph on R² is 7-colorable.