Generated exact combinatorics for the finite second-stage Parts gadget.

structure HadwigerNelsonBounds.PartsGadgetVertex : Type

Axial coordinates in one of the two triangular-lattice patches.

• rotated : Bool

  Whether the point lies in the rotated patch.

• q : ℤ

  First axial coordinate.

• r : ℤ

  Second axial coordinate.

def HadwigerNelsonBounds.instDecidableEqPartsGadgetVertex.decEq (x✝ x✝¹ : PartsGadgetVertex) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance HadwigerNelsonBounds.instDecidableEqPartsGadgetVertex : DecidableEq PartsGadgetVertex

Equations

• HadwigerNelsonBounds.instDecidableEqPartsGadgetVertex = HadwigerNelsonBounds.instDecidableEqPartsGadgetVertex.decEq

def HadwigerNelsonBounds.partsGadgetVertex (vertex : Fin 73) : PartsGadgetVertex

Exact descriptor of one of the 73 gadget vertices.

Equations

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

structure HadwigerNelsonBounds.PartsGadgetTriangleWitnessData : Type

Raw geometric witness for one listed sqrt-three triple.

• left : Fin 73

  First partner of the rooted triple.

• right : Fin 73

  Second partner of the rooted triple.

• a : Fin 73

  Vertex in the canonical A role.

• b : Fin 73

  Vertex in the canonical B role.

• c : Fin 73

  Vertex in the canonical C role.

• rotated : Bool

  Patch containing the triple.

• centerQ : ℤ

  First axial coordinate of its center.

• centerR : ℤ

  Second axial coordinate of its center.

• negated : Bool

  Whether the canonical triangle is inverted.

def HadwigerNelsonBounds.instDecidableEqPartsGadgetTriangleWitnessData.decEq (x✝ x✝¹ : PartsGadgetTriangleWitnessData) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance HadwigerNelsonBounds.instDecidableEqPartsGadgetTriangleWitnessData : DecidableEq PartsGadgetTriangleWitnessData

Equations

• HadwigerNelsonBounds.instDecidableEqPartsGadgetTriangleWitnessData = HadwigerNelsonBounds.instDecidableEqPartsGadgetTriangleWitnessData.decEq

def HadwigerNelsonBounds.partsGadgetAxialAt (rotated : Bool) (q r : ℤ) (vertex : Fin 73) : Prop

A vertex has the requested axial coordinates in the requested patch. The common origin belongs to both patches.

Equations

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

@[implicit_reducible]

instance HadwigerNelsonBounds.instDecidablePartsGadgetAxialAt (rotated : Bool) (q r : ℤ) (vertex : Fin 73) : Decidable (partsGadgetAxialAt rotated q r vertex)

Equations

• HadwigerNelsonBounds.instDecidablePartsGadgetAxialAt rotated q r vertex = id inferInstance

def HadwigerNelsonBounds.partsGadgetSameTriple (a b c x y z : Fin 73) : Prop

Decidable equality-up-to-permutation for three named vertices.

Equations

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

@[implicit_reducible]

instance HadwigerNelsonBounds.instDecidablePartsGadgetSameTriple (a b c x y z : Fin 73) : Decidable (partsGadgetSameTriple a b c x y z)

Equations

• HadwigerNelsonBounds.instDecidablePartsGadgetSameTriple a b c x y z = id inferInstance

def HadwigerNelsonBounds.PartsGadgetTriangleWitnessData.Valid (witness : PartsGadgetTriangleWitnessData) (root : Fin 73) : Prop

Exact validity conditions for a triangle witness.

Equations

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

@[implicit_reducible]

instance HadwigerNelsonBounds.instDecidableValid (witness : PartsGadgetTriangleWitnessData) (root : Fin 73) : Decidable (witness.Valid root)

Equations

• HadwigerNelsonBounds.instDecidableValid witness root = id inferInstance

def HadwigerNelsonBounds.partsGadgetTriangleWitnesses (vertex : Fin 73) : List PartsGadgetTriangleWitnessData

Geometric witnesses for every listed sqrt-three triple.

Equations

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

def HadwigerNelsonBounds.partsGadgetNeighbors (vertex : Fin 73) : List (Fin 73)

Unit-edge neighbors used by the executable certificate checker.

Equations

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

def HadwigerNelsonBounds.partsGadgetTriplePairs (vertex : Fin 73) : List (Fin 73 × Fin 73)

Opposite pairs completing sqrt-three triples at a vertex.

Equations

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

def HadwigerNelsonBounds.partsGadgetNegation (vertex : Fin 73) : Fin 73

Central inversion of both lattice patches.

Equations

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