Documentation

LeanPool.HadwigerNelsonBounds.PartsGadgetForcedPair

The forced pair in the second-stage Parts gadget #

The checked finite constraints force the opposite radius-two vertices 5 and 31 to have the same color. Color renamings and central inversion reduce every case to the independently checked normalized trees.

source
theorem HadwigerNelsonBounds.PartsGadgetValid.rename {coloring : Fin 73 → Fin 4} (hvalid : PartsGadgetValid coloring) (rename : Fin 4 ≃ Fin 4) :
PartsGadgetValid fun (vertex : Fin 73) => rename (coloring vertex)

Renaming colors preserves both gadget constraints.

source
theorem HadwigerNelsonBounds.PartsGadgetValid.negation {coloring : Fin 73 → Fin 4} (hvalid : PartsGadgetValid coloring) :
PartsGadgetValid fun (vertex : Fin 73) => coloring (partsGadgetNegation vertex)

Pulling a coloring back through central inversion preserves validity.

source
def HadwigerNelsonBounds.partsGadgetSwapOneTwo :
Fin 4 ≃ Fin 4

Swap the two residual colors while fixing zero and three.

Equations
Instances For
    source
    def HadwigerNelsonBounds.partsGadgetSwapZeroThree :
    Fin 4 ≃ Fin 4

    Swap the endpoint colors zero and three.

    Equations
    Instances For
      source
      @[simp]
      theorem HadwigerNelsonBounds.partsGadgetSwapOneTwo_zero :
      partsGadgetSwapOneTwo 0 = 0
      source
      @[simp]
      theorem HadwigerNelsonBounds.partsGadgetSwapOneTwo_one :
      partsGadgetSwapOneTwo 1 = 2
      source
      @[simp]
      theorem HadwigerNelsonBounds.partsGadgetSwapOneTwo_two :
      partsGadgetSwapOneTwo 2 = 1
      source
      @[simp]
      theorem HadwigerNelsonBounds.partsGadgetSwapOneTwo_three :
      partsGadgetSwapOneTwo 3 = 3
      source
      @[simp]
      theorem HadwigerNelsonBounds.partsGadgetSwapZeroThree_zero :
      partsGadgetSwapZeroThree 0 = 3
      source
      @[simp]
      theorem HadwigerNelsonBounds.partsGadgetSwapZeroThree_one :
      partsGadgetSwapZeroThree 1 = 1
      source
      @[simp]
      theorem HadwigerNelsonBounds.partsGadgetSwapZeroThree_two :
      partsGadgetSwapZeroThree 2 = 2
      source
      @[simp]
      theorem HadwigerNelsonBounds.partsGadgetSwapZeroThree_three :
      partsGadgetSwapZeroThree 3 = 0
      source
      theorem HadwigerNelsonBounds.partsGadgetHardRoots {coloring : Fin 73 → Fin 4} (ha : coloring 5 = 0) (hb : coloring 31 = 3) (hcenter : coloring 18 = 0) (hanchor : coloring 25 = 1) :
      PartsGadgetExtends coloring partsGadgetHardCaseTree.roots
      source
      theorem HadwigerNelsonBounds.partsGadgetMiddleRoots {coloring : Fin 73 → Fin 4} (ha : coloring 5 = 0) (hb : coloring 31 = 3) (hcenter : coloring 18 = 1) :
      PartsGadgetExtends coloring partsGadgetMiddleCertificate.roots
      source
      theorem HadwigerNelsonBounds.no_partsGadget_coloring_of_hard_roots {coloring : Fin 73 → Fin 4} (hvalid : PartsGadgetValid coloring) (ha : coloring 5 = 0) (hb : coloring 31 = 3) (hcenter : coloring 18 = 0) :
      False
      source
      theorem HadwigerNelsonBounds.no_partsGadget_coloring_of_middle_roots {coloring : Fin 73 → Fin 4} (hvalid : PartsGadgetValid coloring) (ha : coloring 5 = 0) (hb : coloring 31 = 3) (hcenter : coloring 18 = 1) :
      False
      source
      theorem HadwigerNelsonBounds.no_partsGadget_coloring_of_normalized_endpoints {coloring : Fin 73 → Fin 4} (hvalid : PartsGadgetValid coloring) (ha : coloring 5 = 0) (hb : coloring 31 = 3) :
      False
      source
      theorem HadwigerNelsonBounds.parts_gadget_forces_monochromatic_pair {coloring : Fin 73 → Fin 4} (hvalid : PartsGadgetValid coloring) :
      coloring 5 = coloring 31

      The finite Parts gadget forces its opposite distance-four pair to be monochromatic under the unit-edge and non-mono-triple constraints.