Exact geometry for the Parts lower-bound certificate

The 481-vertex base graph in Parts' certificate uses points

(a + b * sqrt 33, c * sqrt 3 + d * sqrt 11) / 12.

The equivalent coordinates below use only sqrt 33 and sqrt 3; this makes the unit-distance check an integer calculation.

structure HadwigerNelsonBounds.PartsPoint : Type

Integer coordinates for the quadratic field used by the Parts graph.

• a : ℤ

  Rational coefficient in the first Cartesian coordinate.

• b : ℤ

  sqrt 33 coefficient in the first Cartesian coordinate.

• c : ℤ

  Rational coefficient in the second Cartesian coordinate.

• d : ℤ

  sqrt 33 coefficient in the second Cartesian coordinate.

@[implicit_reducible]

instance HadwigerNelsonBounds.instDecidableEqPartsPoint : DecidableEq PartsPoint

Equations

• HadwigerNelsonBounds.instDecidableEqPartsPoint = HadwigerNelsonBounds.instDecidableEqPartsPoint.decEq

def HadwigerNelsonBounds.instDecidableEqPartsPoint.decEq (x✝ x✝¹ : PartsPoint) : Decidable (x✝ = x✝¹)

Equations

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

def HadwigerNelsonBounds.PartsPoint.sub (p q : PartsPoint) : PartsPoint

Difference of two exact Parts coordinates.

Equations

• p.sub q = { a := p.a - q.a, b := p.b - q.b, c := p.c - q.c, d := p.d - q.d }

def HadwigerNelsonBounds.PartsPoint.normNumerator (p : PartsPoint) : ℤ

Rational coefficient of 144 times the squared norm.

Equations

• p.normNumerator = p.a ^ 2 + 33 * p.b ^ 2 + 3 * p.c ^ 2 + 11 * p.d ^ 2

def HadwigerNelsonBounds.PartsPoint.radicalCoefficient (p : PartsPoint) : ℤ

Coefficient of 2 * sqrt 33 in 144 times the squared norm.

Equations

• p.radicalCoefficient = p.a * p.b + p.c * p.d

def HadwigerNelsonBounds.PartsPoint.IsUnit (p : PartsPoint) : Bool

Exact decidable test that an integer coordinate vector has length one.

Equations

• p.IsUnit = decide (p.normNumerator = 144 ∧ p.radicalCoefficient = 0)

theorem HadwigerNelsonBounds.PartsPoint.isUnit_iff (p : PartsPoint) : p.IsUnit = true ↔ p.normNumerator = 144 ∧ p.radicalCoefficient = 0

noncomputable def HadwigerNelsonBounds.PartsPoint.toR2 (p : PartsPoint) : R2

Embed exact certificate coordinates in the Euclidean plane.

Equations

• p.toR2 = !₂[(↑p.a + ↑p.b * √33) / 12, (3 * ↑p.c + ↑p.d * √33) / (12 * √3)]

@[simp]

theorem HadwigerNelsonBounds.PartsPoint.toR2_zero (p : PartsPoint) : p.toR2.ofLp 0 = (↑p.a + ↑p.b * √33) / 12

@[simp]

theorem HadwigerNelsonBounds.PartsPoint.toR2_one (p : PartsPoint) : p.toR2.ofLp 1 = (3 * ↑p.c + ↑p.d * √33) / (12 * √3)

theorem HadwigerNelsonBounds.PartsPoint.dist_sq (p q : PartsPoint) : dist p.toR2 q.toR2 ^ 2 = ↑(p.sub q).normNumerator / 144 + 2 * ↑(p.sub q).radicalCoefficient * √33 / 144

theorem HadwigerNelsonBounds.PartsPoint.dist_eq_one_of_isUnit {p q : PartsPoint} (h : (p.sub q).IsUnit = true) : dist p.toR2 q.toR2 = 1

Every positive exact unit vector embeds as a Euclidean unit segment.