The canonical non-monochromatic sqrt-three triangle

The checked Parts certificate rules out a monochromatic copy of its canonical equilateral triangle in every proper four-coloring of the plane.

def HadwigerNelsonBounds.partsColorEquiv (triple center : Fin 4) : Fin 4 ≃ Fin 4

Rename a distinguished color to zero and a different color to three.

Equations

• HadwigerNelsonBounds.partsColorEquiv triple center = Equiv.trans (Equiv.swap triple 0) (Equiv.swap ((Equiv.swap triple 0) center) 3)

theorem HadwigerNelsonBounds.partsColorEquiv_spec {triple center : Fin 4} (hne : triple ≠ center) : (partsColorEquiv triple center) triple = 0 ∧ (partsColorEquiv triple center) center = 3

noncomputable def HadwigerNelsonBounds.partsTriangleA : R2

First vertex of the canonical equilateral triangle in the Parts graph.

Equations

• HadwigerNelsonBounds.partsTriangleA = (HadwigerNelsonBounds.partsPoint 195).toR2

noncomputable def HadwigerNelsonBounds.partsTriangleB : R2

Second vertex of the canonical equilateral triangle in the Parts graph.

Equations

• HadwigerNelsonBounds.partsTriangleB = (HadwigerNelsonBounds.partsPoint 205).toR2

noncomputable def HadwigerNelsonBounds.partsTriangleC : R2

Third vertex of the canonical equilateral triangle in the Parts graph.

Equations

• HadwigerNelsonBounds.partsTriangleC = (HadwigerNelsonBounds.partsPoint 215).toR2

noncomputable def HadwigerNelsonBounds.partsTriangleCenter : R2

The origin, adjacent to all three canonical triangle vertices.

Equations

• HadwigerNelsonBounds.partsTriangleCenter = (HadwigerNelsonBounds.partsPoint 0).toR2

theorem HadwigerNelsonBounds.parts_canonical_triangle_not_monochromatic (planeColoring : unitDistanceGraph.Coloring (Fin 4)) : ¬(planeColoring partsTriangleA = planeColoring partsTriangleB ∧ planeColoring partsTriangleB = planeColoring partsTriangleC)

The full Parts certificate: its canonical sqrt-three triangle is never monochromatic in a proper four-coloring of the unit-distance graph.