Plane geometry for the Parts spindle #

This module gives an explicit triangular-lattice realization and elementary distance-preserving rotations. The two exact cosines are the angles used in Parts' doubled wheel and spindle.

source

noncomputable def HadwigerNelsonBounds.pointR2 (x y : ℝ) :

A point in R² from its two Cartesian coordinates.

Equations

HadwigerNelsonBounds.pointR2 x y = !₂[x, y]

Instances For

source

@[simp]

theorem HadwigerNelsonBounds.pointR2_zero (x y : ℝ) :

(pointR2 x y).ofLp 0 = x

source

@[simp]

theorem HadwigerNelsonBounds.pointR2_one (x y : ℝ) :

(pointR2 x y).ofLp 1 = y

source

noncomputable def HadwigerNelsonBounds.partsAxialPoint (q r : ℤ) :

The triangular-lattice point with axial coordinates (q,r).

Equations

HadwigerNelsonBounds.partsAxialPoint q r = HadwigerNelsonBounds.pointR2 ((↑q - ↑r) / 2) ((↑q + ↑r) * √3 / 2)

Instances For

source

@[simp]

theorem HadwigerNelsonBounds.partsAxialPoint_zero :

partsAxialPoint 0 0 = 0

source

theorem HadwigerNelsonBounds.partsAxialPoint_add (q r q' r' : ℤ) :

partsAxialPoint (q + q') (r + r') = partsAxialPoint q r + partsAxialPoint q' r'

source

theorem HadwigerNelsonBounds.partsAxialPoint_neg (q r : ℤ) :

partsAxialPoint (-q) (-r) = -partsAxialPoint q r

source

theorem HadwigerNelsonBounds.partsAxialPoint_sub (q r q' r' : ℤ) :

partsAxialPoint (q - q') (r - r') = partsAxialPoint q r - partsAxialPoint q' r'

source

theorem HadwigerNelsonBounds.partsTriangleA_eq_axial :

partsTriangleA = partsAxialPoint 1 0

source

theorem HadwigerNelsonBounds.partsTriangleB_eq_axial :

partsTriangleB = partsAxialPoint 0 (-1)

source

theorem HadwigerNelsonBounds.partsTriangleC_eq_axial :

partsTriangleC = partsAxialPoint (-1) 1

source

theorem HadwigerNelsonBounds.partsAxialPoint_dist_sq (q r q' r' : ℤ) :

dist (partsAxialPoint q r) (partsAxialPoint q' r') ^ 2 = ↑(q - q') ^ 2 + ↑(q - q') * ↑(r - r') + ↑(r - r') ^ 2

Squared distance on the axial triangular lattice.

source

theorem HadwigerNelsonBounds.partsAxialPoint_dist_eq_one {q r q' r' : ℤ} (hnorm : (q - q') ^ 2 + (q - q') * (r - r') + (r - r') ^ 2 = 1) :

dist (partsAxialPoint q r) (partsAxialPoint q' r') = 1

source

noncomputable def HadwigerNelsonBounds.planeRotation (cosine sine : ℝ) (p : R2) :

Rotation through an angle represented by its cosine and sine.

Equations

HadwigerNelsonBounds.planeRotation cosine sine p = HadwigerNelsonBounds.pointR2 (cosine * p.ofLp 0 - sine * p.ofLp 1) (sine * p.ofLp 0 + cosine * p.ofLp 1)

Instances For

source

@[simp]

theorem HadwigerNelsonBounds.planeRotation_zero (cosine sine : ℝ) :

planeRotation cosine sine 0 = 0

source

theorem HadwigerNelsonBounds.planeRotation_dist_eq {cosine sine : ℝ} (htrig : cosine ^ 2 + sine ^ 2 = 1) (p q : R2) :

dist (planeRotation cosine sine p) (planeRotation cosine sine q) = dist p q

source

theorem HadwigerNelsonBounds.planeRotation_displacement_sq {cosine sine : ℝ} (htrig : cosine ^ 2 + sine ^ 2 = 1) (p : R2) :

dist p (planeRotation cosine sine p) ^ 2 = 2 * (1 - cosine) * dist p 0 ^ 2

source

noncomputable def HadwigerNelsonBounds.partsPatchCosine :

ℝ

The doubled-wheel angle has cosine 7/8.

Equations

HadwigerNelsonBounds.partsPatchCosine = 7 / 8

Instances For

source

noncomputable def HadwigerNelsonBounds.partsPatchSine :

ℝ

Positive sine of the doubled-wheel angle.

Equations

HadwigerNelsonBounds.partsPatchSine = √15 / 8

Instances For

source

theorem HadwigerNelsonBounds.partsPatch_trig :

partsPatchCosine ^ 2 + partsPatchSine ^ 2 = 1

source

noncomputable def HadwigerNelsonBounds.partsPatchRotation :

R2 → R2

Rotation used to superimpose the second triangular-lattice patch.

Equations

HadwigerNelsonBounds.partsPatchRotation = HadwigerNelsonBounds.planeRotation HadwigerNelsonBounds.partsPatchCosine HadwigerNelsonBounds.partsPatchSine

Instances For

source

theorem HadwigerNelsonBounds.partsPatchRotation_dist_eq (p q : R2) :

dist (partsPatchRotation p) (partsPatchRotation q) = dist p q

source

theorem HadwigerNelsonBounds.partsPatchRotation_displacement_sq (p : R2) :

dist p (partsPatchRotation p) ^ 2 = dist p 0 ^ 2 / 4

source

@[simp]

theorem HadwigerNelsonBounds.partsPatchRotation_zero :

partsPatchRotation 0 = 0

source

noncomputable def HadwigerNelsonBounds.partsApplyPatch (rotated : Bool) (p : R2) :

Apply the doubled-wheel rotation exactly when selecting its second patch.

Equations

HadwigerNelsonBounds.partsApplyPatch rotated p = if rotated = true then HadwigerNelsonBounds.partsPatchRotation p else p

Instances For

source

theorem HadwigerNelsonBounds.partsApplyPatch_dist_eq (rotated : Bool) (p q : R2) :

dist (partsApplyPatch rotated p) (partsApplyPatch rotated q) = dist p q

source

@[simp]

theorem HadwigerNelsonBounds.partsApplyPatch_zero (rotated : Bool) :

partsApplyPatch rotated 0 = 0

source

def HadwigerNelsonBounds.partsApplyNegation (negated : Bool) (p : R2) :

Optionally apply the central inversion used by a triangle witness.

Equations

HadwigerNelsonBounds.partsApplyNegation negated p = if negated = true then -p else p

Instances For

source

theorem HadwigerNelsonBounds.partsApplyNegation_dist_eq (negated : Bool) (p q : R2) :

dist (partsApplyNegation negated p) (partsApplyNegation negated q) = dist p q

source

noncomputable def HadwigerNelsonBounds.partsTriangleMotion (rotated : Bool) (centerQ centerR : ℤ) (negated : Bool) (p : R2) :

Translate, optionally invert, and optionally rotate a canonical triangle.

Equations

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

Instances For

source

theorem HadwigerNelsonBounds.partsTriangleMotion_dist_eq (rotated : Bool) (centerQ centerR : ℤ) (negated : Bool) (p q : R2) :

dist (partsTriangleMotion rotated centerQ centerR negated p) (partsTriangleMotion rotated centerQ centerR negated q) = dist p q

source

theorem HadwigerNelsonBounds.partsTriangleMotion_A (rotated : Bool) (centerQ centerR : ℤ) (negated : Bool) :

partsTriangleMotion rotated centerQ centerR negated partsTriangleA = partsApplyPatch rotated (partsAxialPoint (centerQ + if negated = true then -1 else 1) centerR)

source

theorem HadwigerNelsonBounds.partsTriangleMotion_B (rotated : Bool) (centerQ centerR : ℤ) (negated : Bool) :

partsTriangleMotion rotated centerQ centerR negated partsTriangleB = partsApplyPatch rotated (partsAxialPoint centerQ (centerR + if negated = true then 1 else -1))

source

theorem HadwigerNelsonBounds.partsTriangleMotion_C (rotated : Bool) (centerQ centerR : ℤ) (negated : Bool) :

partsTriangleMotion rotated centerQ centerR negated partsTriangleC = partsApplyPatch rotated (partsAxialPoint (centerQ + if negated = true then 1 else -1) (centerR + if negated = true then -1 else 1))

source

noncomputable def HadwigerNelsonBounds.pullbackUnitDistanceColoring {color : Type u_1} (planeColoring : unitDistanceGraph.Coloring color) (motion : R2 → R2) (hdist : ∀ (p q : R2), dist (motion p) (motion q) = dist p q) :

unitDistanceGraph.Coloring color

Pull a proper plane coloring back along any distance-preserving map.

Equations

HadwigerNelsonBounds.pullbackUnitDistanceColoring planeColoring motion hdist = SimpleGraph.Coloring.mk (fun (p : HadwigerNelsonBounds.R2) => planeColoring (motion p)) ⋯

Instances For

source

@[simp]

theorem HadwigerNelsonBounds.pullbackUnitDistanceColoring_apply {color : Type u_1} (planeColoring : unitDistanceGraph.Coloring color) (motion : R2 → R2) (hdist : ∀ (p q : R2), dist (motion p) (motion q) = dist p q) (p : R2) :

(pullbackUnitDistanceColoring planeColoring motion hdist) p = planeColoring (motion p)

source

theorem HadwigerNelsonBounds.parts_triangle_motion_not_monochromatic (planeColoring : unitDistanceGraph.Coloring (Fin 4)) (rotated : Bool) (centerQ centerR : ℤ) (negated : Bool) :

¬(planeColoring (partsTriangleMotion rotated centerQ centerR negated partsTriangleA) = planeColoring (partsTriangleMotion rotated centerQ centerR negated partsTriangleB) ∧ planeColoring (partsTriangleMotion rotated centerQ centerR negated partsTriangleB) = planeColoring (partsTriangleMotion rotated centerQ centerR negated partsTriangleC))

Every rigid image of the checked canonical triangle is non-monochromatic.

source

noncomputable def HadwigerNelsonBounds.partsSpindleCosine :

ℝ

The final spindle angle has cosine 31/32.

Equations