Euclidean realization of the finite Parts gadget

The 73 descriptors encode two radius-three triangular-lattice patches with a common center. The second patch is rotated through cosine 7/8.

def HadwigerNelsonBounds.partsAxialNormSq (q r : ℤ) : ℤ

The integral quadratic norm of an axial lattice vector.

Equations

• HadwigerNelsonBounds.partsAxialNormSq q r = q ^ 2 + q * r + r ^ 2

def HadwigerNelsonBounds.PartsGadgetVertex.IsCenter (vertex : PartsGadgetVertex) : Prop

Whether a descriptor is the common center of both patches.

Equations

• vertex.IsCenter = (vertex.q = 0 ∧ vertex.r = 0)

@[implicit_reducible]

instance HadwigerNelsonBounds.instDecidableIsCenter (vertex : PartsGadgetVertex) : Decidable vertex.IsCenter

Equations

• HadwigerNelsonBounds.instDecidableIsCenter vertex = id inferInstance

def HadwigerNelsonBounds.PartsGadgetEdgeCase (left right : Fin 73) : Prop

Arithmetic classification of every unit edge in the gadget.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance HadwigerNelsonBounds.instDecidablePartsGadgetEdgeCase (left right : Fin 73) : Decidable (PartsGadgetEdgeCase left right)

Equations

• HadwigerNelsonBounds.instDecidablePartsGadgetEdgeCase left right = id inferInstance

noncomputable def HadwigerNelsonBounds.partsGadgetPoint (vertex : Fin 73) : R2

Explicit point of the doubled triangular-lattice patch.

Equations

• One or more equations did not get rendered due to their size.

theorem HadwigerNelsonBounds.partsGadgetPoint_eq_of_axialAt {rotated : Bool} {q r : ℤ} {vertex : Fin 73} (hposition : partsGadgetAxialAt rotated q r vertex) : partsGadgetPoint vertex = partsApplyPatch rotated (partsAxialPoint q r)

theorem HadwigerNelsonBounds.partsGadgetPoint_dist_eq_one_of_edgeCase {left right : Fin 73} (hedge : PartsGadgetEdgeCase left right) : dist (partsGadgetPoint left) (partsGadgetPoint right) = 1

Every arithmetically classified gadget edge has Euclidean length one.

theorem HadwigerNelsonBounds.PartsGadgetTriangleWitnessData.point_a_eq {witness : PartsGadgetTriangleWitnessData} {root : Fin 73} (hvalid : witness.Valid root) : partsGadgetPoint witness.a = partsTriangleMotion witness.rotated witness.centerQ witness.centerR witness.negated partsTriangleA

theorem HadwigerNelsonBounds.PartsGadgetTriangleWitnessData.point_b_eq {witness : PartsGadgetTriangleWitnessData} {root : Fin 73} (hvalid : witness.Valid root) : partsGadgetPoint witness.b = partsTriangleMotion witness.rotated witness.centerQ witness.centerR witness.negated partsTriangleB

theorem HadwigerNelsonBounds.PartsGadgetTriangleWitnessData.point_c_eq {witness : PartsGadgetTriangleWitnessData} {root : Fin 73} (hvalid : witness.Valid root) : partsGadgetPoint witness.c = partsTriangleMotion witness.rotated witness.centerQ witness.centerR witness.negated partsTriangleC

theorem HadwigerNelsonBounds.partsGadgetWitness_roles_not_monochromatic (planeColoring : unitDistanceGraph.Coloring (Fin 4)) {witness : PartsGadgetTriangleWitnessData} {root : Fin 73} (hvalid : witness.Valid root) : ¬(planeColoring (partsGadgetPoint witness.a) = planeColoring (partsGadgetPoint witness.b) ∧ planeColoring (partsGadgetPoint witness.b) = planeColoring (partsGadgetPoint witness.c))

theorem HadwigerNelsonBounds.partsGadget_monochromatic_of_sameTriple (coloring : Fin 73 → Fin 4) {a b c x y z : Fin 73} (hsame : partsGadgetSameTriple a b c x y z) (hmono : coloring x = coloring y ∧ coloring y = coloring z) : coloring a = coloring b ∧ coloring b = coloring c