The finite Parts gadget inside the unit-distance plane

Every combinatorial edge is a unit segment and every hyperedge is a rigid copy of the canonical triangle ruled out by the checked 481-vertex certificate.

noncomputable def HadwigerNelsonBounds.partsGadgetColoring (planeColoring : unitDistanceGraph.Coloring (Fin 4)) : Fin 73 → Fin 4

Restrict a plane coloring to the 73 explicit gadget points.

Equations

• HadwigerNelsonBounds.partsGadgetColoring planeColoring vertex = planeColoring (HadwigerNelsonBounds.partsGadgetPoint vertex)

theorem HadwigerNelsonBounds.partsGadgetColoring_valid (planeColoring : unitDistanceGraph.Coloring (Fin 4)) : PartsGadgetValid (partsGadgetColoring planeColoring)

theorem HadwigerNelsonBounds.parts_doubled_patch_forces_monochromatic_pair (planeColoring : unitDistanceGraph.Coloring (Fin 4)) : planeColoring (partsGadgetPoint 5) = planeColoring (partsGadgetPoint 31)

The explicitly embedded doubled patch forces its opposite endpoints to have equal colors in every proper four-coloring of the plane.

theorem HadwigerNelsonBounds.partsGadgetPoint_five : partsGadgetPoint 5 = partsAxialPoint (-2) 0

theorem HadwigerNelsonBounds.partsGadgetPoint_thirtyOne : partsGadgetPoint 31 = partsAxialPoint 2 0

theorem HadwigerNelsonBounds.parts_axial_pair_forces_monochromatic (planeColoring : unitDistanceGraph.Coloring (Fin 4)) : planeColoring (partsAxialPoint (-2) 0) = planeColoring (partsAxialPoint 2 0)

The forced pair in axial coordinates; its Euclidean distance is four.

theorem HadwigerNelsonBounds.parts_axial_pair_forces_under_motion (planeColoring : unitDistanceGraph.Coloring (Fin 4)) (motion : R2 → R2) (hdist : ∀ (p q : R2), dist (motion p) (motion q) = dist p q) : planeColoring (motion (partsAxialPoint (-2) 0)) = planeColoring (motion (partsAxialPoint 2 0))

Every distance-preserving image of the doubled patch forces the corresponding distance-four pair to be monochromatic.