The Parts obstruction to a monochromatic sqrt-three triangle

This module expands the 36 normalized coloring trees through the six exact root symmetries and the remaining color swap. The resulting 432 certificates cover every proper normalized coloring of the 13-vertex 2-Golomb root.

def HadwigerNelsonBounds.partsSwapMiddleColor (color : Fin 4) : Fin 4

Swap the two colors not fixed by the normalized root.

Equations

• HadwigerNelsonBounds.partsSwapMiddleColor color = ![0, 2, 1, 3] color

def HadwigerNelsonBounds.partsTransformColor (swap : Bool) (color : Fin 4) : Fin 4

The color renaming used by a certificate variant.

Equations

• HadwigerNelsonBounds.partsTransformColor swap color = if swap = true then HadwigerNelsonBounds.partsSwapMiddleColor color else color

def HadwigerNelsonBounds.partsTransformAssignment (symmetry : Fin 6) (swap : Bool) (assignment : PartsAssignment) : PartsAssignment

Rename the vertices and optionally the two free colors of an assignment.

Equations

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

def HadwigerNelsonBounds.partsTransformPath (symmetry : Fin 6) (swap : Bool) : List PartsAssignment → List PartsAssignment

Transform a root path without materializing a second copy of its tree.

Equations

• One or more equations did not get rendered due to their size.
• HadwigerNelsonBounds.partsTransformPath symmetry swap [] = []

def HadwigerNelsonBounds.partsBaseCertificate (base : Fin 36) : PartsCertificate

Select one of the 36 normalized root-orbit certificates.

Equations

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

def HadwigerNelsonBounds.PartsVerifiesVariantNodeB (symmetry : Fin 6) (swap : Bool) (nodes : Array (Array PartsTreeNode)) : ℕ → List PartsAssignment → ℕ → Bool

Executable checker for a symmetry/color variant of a stored base tree.

Equations

• One or more equations did not get rendered due to their size.
• HadwigerNelsonBounds.PartsVerifiesVariantNodeB symmetry swap nodes 0 x✝¹ x✝ = false

def HadwigerNelsonBounds.PartsCertificateVariantVerifies (base : Fin 36) (symmetry : Fin 6) (swap : Bool) : Prop

One of the 432 symmetry-expanded certificates passes the checker.

Equations

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

theorem HadwigerNelsonBounds.partsBaseCertificate_verifies (base : Fin 36) : (partsBaseCertificate base).Verifies

Every stored base tree passes the checker before applying root symmetries.

@[instance_reducible]

instance HadwigerNelsonBounds.instDecidablePartsCertificateVariantVerifies (base : Fin 36) (symmetry : Fin 6) (swap : Bool) : Decidable (PartsCertificateVariantVerifies base symmetry swap)

Equations

• HadwigerNelsonBounds.instDecidablePartsCertificateVariantVerifies base symmetry swap = id inferInstance

theorem HadwigerNelsonBounds.partsVerifiesVariantNodeB_unsat {symmetry : Fin 6} {swap : Bool} {nodes : Array (Array PartsTreeNode)} {coloring : Fin 481 → Fin 4} (hproper : PartsProper coloring) {fuel : ℕ} {path : List PartsAssignment} {index : ℕ} : PartsVerifiesVariantNodeB symmetry swap nodes fuel path index = true → PartsExtends coloring path → False

theorem HadwigerNelsonBounds.partsCertificateVariant_not_colorable {base : Fin 36} {symmetry : Fin 6} {swap : Bool} (hverify : PartsCertificateVariantVerifies base symmetry swap) {coloring : Fin 481 → Fin 4} (hproper : PartsProper coloring) (hroots : PartsExtends coloring (partsTransformPath symmetry swap (partsBaseCertificate base).roots)) : False

Soundness of any checked symmetry-expanded Parts tree.

theorem HadwigerNelsonBounds.partsCertificateVariants0_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 0 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariant1_0_verify (swap : Bool) : PartsCertificateVariantVerifies 1 0 swap

theorem HadwigerNelsonBounds.partsCertificateVariant1_1_verify (swap : Bool) : PartsCertificateVariantVerifies 1 1 swap

theorem HadwigerNelsonBounds.partsCertificateVariant1_2_verify (swap : Bool) : PartsCertificateVariantVerifies 1 2 swap

theorem HadwigerNelsonBounds.partsCertificateVariant1_3_verify (swap : Bool) : PartsCertificateVariantVerifies 1 3 swap

theorem HadwigerNelsonBounds.partsCertificateVariant1_4_verify (swap : Bool) : PartsCertificateVariantVerifies 1 4 swap

theorem HadwigerNelsonBounds.partsCertificateVariant1_5_verify (swap : Bool) : PartsCertificateVariantVerifies 1 5 swap

theorem HadwigerNelsonBounds.partsCertificateVariants1_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 1 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants2_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 2 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants3_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 3 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants4_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 4 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants5_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 5 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants6_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 6 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants7_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 7 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariant8_0_verify (swap : Bool) : PartsCertificateVariantVerifies 8 0 swap

theorem HadwigerNelsonBounds.partsCertificateVariant8_1_verify (swap : Bool) : PartsCertificateVariantVerifies 8 1 swap

theorem HadwigerNelsonBounds.partsCertificateVariant8_2_verify (swap : Bool) : PartsCertificateVariantVerifies 8 2 swap

theorem HadwigerNelsonBounds.partsCertificateVariant8_3_verify (swap : Bool) : PartsCertificateVariantVerifies 8 3 swap

theorem HadwigerNelsonBounds.partsCertificateVariant8_4_verify (swap : Bool) : PartsCertificateVariantVerifies 8 4 swap

theorem HadwigerNelsonBounds.partsCertificateVariant8_5_verify (swap : Bool) : PartsCertificateVariantVerifies 8 5 swap

theorem HadwigerNelsonBounds.partsCertificateVariants8_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 8 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants9_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 9 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants10_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 10 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants11_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 11 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants12_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 12 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants13_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 13 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants14_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 14 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants15_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 15 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariant16_0_verify (swap : Bool) : PartsCertificateVariantVerifies 16 0 swap

theorem HadwigerNelsonBounds.partsCertificateVariant16_1_verify (swap : Bool) : PartsCertificateVariantVerifies 16 1 swap

theorem HadwigerNelsonBounds.partsCertificateVariant16_2_verify (swap : Bool) : PartsCertificateVariantVerifies 16 2 swap

theorem HadwigerNelsonBounds.partsCertificateVariant16_3_verify (swap : Bool) : PartsCertificateVariantVerifies 16 3 swap

theorem HadwigerNelsonBounds.partsCertificateVariant16_4_verify (swap : Bool) : PartsCertificateVariantVerifies 16 4 swap

theorem HadwigerNelsonBounds.partsCertificateVariant16_5_verify (swap : Bool) : PartsCertificateVariantVerifies 16 5 swap

theorem HadwigerNelsonBounds.partsCertificateVariants16_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 16 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariant17_0_verify (swap : Bool) : PartsCertificateVariantVerifies 17 0 swap

theorem HadwigerNelsonBounds.partsCertificateVariant17_1_verify (swap : Bool) : PartsCertificateVariantVerifies 17 1 swap

theorem HadwigerNelsonBounds.partsCertificateVariant17_2_verify (swap : Bool) : PartsCertificateVariantVerifies 17 2 swap

theorem HadwigerNelsonBounds.partsCertificateVariant17_3_verify (swap : Bool) : PartsCertificateVariantVerifies 17 3 swap

theorem HadwigerNelsonBounds.partsCertificateVariant17_4_verify (swap : Bool) : PartsCertificateVariantVerifies 17 4 swap

theorem HadwigerNelsonBounds.partsCertificateVariant17_5_verify (swap : Bool) : PartsCertificateVariantVerifies 17 5 swap

theorem HadwigerNelsonBounds.partsCertificateVariants17_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 17 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants18_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 18 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants19_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 19 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants20_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 20 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants21_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 21 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants22_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 22 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants23_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 23 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariant24_0_verify (swap : Bool) : PartsCertificateVariantVerifies 24 0 swap

theorem HadwigerNelsonBounds.partsCertificateVariant24_1_verify (swap : Bool) : PartsCertificateVariantVerifies 24 1 swap

theorem HadwigerNelsonBounds.partsCertificateVariant24_2_verify (swap : Bool) : PartsCertificateVariantVerifies 24 2 swap

theorem HadwigerNelsonBounds.partsCertificateVariant24_3_verify (swap : Bool) : PartsCertificateVariantVerifies 24 3 swap

theorem HadwigerNelsonBounds.partsCertificateVariant24_4_verify (swap : Bool) : PartsCertificateVariantVerifies 24 4 swap

theorem HadwigerNelsonBounds.partsCertificateVariant24_5_verify (swap : Bool) : PartsCertificateVariantVerifies 24 5 swap

theorem HadwigerNelsonBounds.partsCertificateVariants24_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 24 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariant25_0_verify (swap : Bool) : PartsCertificateVariantVerifies 25 0 swap

theorem HadwigerNelsonBounds.partsCertificateVariant25_1_verify (swap : Bool) : PartsCertificateVariantVerifies 25 1 swap

theorem HadwigerNelsonBounds.partsCertificateVariant25_2_verify (swap : Bool) : PartsCertificateVariantVerifies 25 2 swap

theorem HadwigerNelsonBounds.partsCertificateVariant25_3_verify (swap : Bool) : PartsCertificateVariantVerifies 25 3 swap

theorem HadwigerNelsonBounds.partsCertificateVariant25_4_verify (swap : Bool) : PartsCertificateVariantVerifies 25 4 swap

theorem HadwigerNelsonBounds.partsCertificateVariant25_5_verify (swap : Bool) : PartsCertificateVariantVerifies 25 5 swap

theorem HadwigerNelsonBounds.partsCertificateVariants25_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 25 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants26_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 26 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants27_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 27 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants28_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 28 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants29_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 29 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants30_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 30 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants31_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 31 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants32_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 32 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants33_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 33 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariant34_0_verify (swap : Bool) : PartsCertificateVariantVerifies 34 0 swap

theorem HadwigerNelsonBounds.partsCertificateVariant34_1_verify (swap : Bool) : PartsCertificateVariantVerifies 34 1 swap

theorem HadwigerNelsonBounds.partsCertificateVariant34_2_verify (swap : Bool) : PartsCertificateVariantVerifies 34 2 swap

theorem HadwigerNelsonBounds.partsCertificateVariant34_3_verify (swap : Bool) : PartsCertificateVariantVerifies 34 3 swap

theorem HadwigerNelsonBounds.partsCertificateVariant34_4_verify (swap : Bool) : PartsCertificateVariantVerifies 34 4 swap

theorem HadwigerNelsonBounds.partsCertificateVariant34_5_verify (swap : Bool) : PartsCertificateVariantVerifies 34 5 swap

theorem HadwigerNelsonBounds.partsCertificateVariants34_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 34 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariants35_verify (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies 35 symmetry swap

theorem HadwigerNelsonBounds.partsCertificateVariant_verifies (base : Fin 36) (symmetry : Fin 6) (swap : Bool) : PartsCertificateVariantVerifies base symmetry swap