Documentation

LeanPool.HadwigerNelsonBounds.PartsSpindle

The Parts spindle and the known bounds #

Two copies of the forced distance-four pair share one endpoint. Rotating the second copy through cosine 31/32 makes the remaining endpoints unit-adjacent, contradicting a proper four-coloring.

source
noncomputable def HadwigerNelsonBounds.partsSpindleVector :
R2

The distance-four vector between the translated gadget endpoints.

Equations
Instances For
    source
    noncomputable def HadwigerNelsonBounds.partsFirstSpindleMotion (p : R2) :
    R2

    Translate the first doubled patch so its left endpoint is the origin.

    Equations
    Instances For
      source
      noncomputable def HadwigerNelsonBounds.partsSecondSpindleMotion (p : R2) :
      R2

      Translate the second doubled patch and rotate it around the shared origin.

      Equations
      Instances For
        source
        theorem HadwigerNelsonBounds.partsFirstSpindleMotion_dist_eq (p q : R2) :
        dist (partsFirstSpindleMotion p) (partsFirstSpindleMotion q) = dist p q
        source
        theorem HadwigerNelsonBounds.partsSecondSpindleMotion_dist_eq (p q : R2) :
        dist (partsSecondSpindleMotion p) (partsSecondSpindleMotion q) = dist p q
        source
        @[simp]
        theorem HadwigerNelsonBounds.partsFirstSpindleMotion_left :
        partsFirstSpindleMotion (partsAxialPoint (-2) 0) = 0
        source
        @[simp]
        theorem HadwigerNelsonBounds.partsFirstSpindleMotion_right :
        partsFirstSpindleMotion (partsAxialPoint 2 0) = partsSpindleVector
        source
        @[simp]
        theorem HadwigerNelsonBounds.partsSecondSpindleMotion_left :
        partsSecondSpindleMotion (partsAxialPoint (-2) 0) = 0
        source
        @[simp]
        theorem HadwigerNelsonBounds.partsSecondSpindleMotion_right :
        partsSecondSpindleMotion (partsAxialPoint 2 0) = partsSpindleRotation partsSpindleVector
        source
        theorem HadwigerNelsonBounds.partsSpindleVector_norm_sq :
        dist partsSpindleVector 0 ^ 2 = 16
        source
        theorem HadwigerNelsonBounds.partsSpindleVector_rotated_dist :
        dist partsSpindleVector (partsSpindleRotation partsSpindleVector) = 1

        The two free spindle endpoints are exactly one unit apart.

        source
        theorem HadwigerNelsonBounds.unitDistanceGraph_not_colorable_four :
        ¬unitDistanceGraph.Colorable 4

        Parts lower bound. The unit-distance graph of the Euclidean plane has no proper coloring with four colors.

        source
        theorem HadwigerNelsonBounds.five_le_chromaticNumber :
        5 ≤ unitDistanceGraph.chromaticNumber

        Lower bound — 5 ≤ χ(ℝ²).

        source
        theorem HadwigerNelsonBounds.hadwiger_nelson_known_bounds :
        5 ≤ unitDistanceGraph.chromaticNumber ∧ unitDistanceGraph.chromaticNumber ≤ 7

        Known bounds for the Hadwiger--Nelson problem: 5 ≤ χ(ℝ²) ≤ 7.