A sound checker for the second-stage Parts gadget

The finite constraint system has unit-edge inequalities and non-monochromatic sqrt-three triples. Unary stretches of its coloring trees are stored as forced stems, exactly as in the first-stage Parts certificate.

structure HadwigerNelsonBounds.PartsGadgetAssignment : Type

A vertex-color assignment in the 73-vertex second-stage gadget.

• vertex : Fin 73

  Assigned gadget vertex.

• color : Fin 4

  Assigned color.

@[implicit_reducible]

instance HadwigerNelsonBounds.instDecidableEqPartsGadgetAssignment : DecidableEq PartsGadgetAssignment

Equations

• HadwigerNelsonBounds.instDecidableEqPartsGadgetAssignment = HadwigerNelsonBounds.instDecidableEqPartsGadgetAssignment.decEq

def HadwigerNelsonBounds.instDecidableEqPartsGadgetAssignment.decEq (x✝ x✝¹ : PartsGadgetAssignment) : Decidable (x✝ = x✝¹)

Equations

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

structure HadwigerNelsonBounds.PartsGadgetTreeNode : Type

A compressed coloring-tree node.

• stem : List PartsGadgetAssignment

  Unary forced assignments preceding the branch.

• vertex : Fin 73

  Vertex branched on after the forced stem.

• children : Fin 4 → ℕ

  Encoded child index for each color, with zero meaning absent.

def HadwigerNelsonBounds.PartsGadgetTreeNode.child (node : PartsGadgetTreeNode) (color : Fin 4) : Option ℕ

Decode zero as no child and n + 1 as child index n.

Equations

• node.child color = match node.children color with | 0 => none | index.succ => some index

structure HadwigerNelsonBounds.PartsGadgetCertificate : Type

A normalized root coloring and its compressed contradiction tree.

• roots : List PartsGadgetAssignment

  Fixed root assignments.

• nodeCount : ℕ

  Number of nodes addressable in the chunked array.

• nodes : Array (Array PartsGadgetTreeNode)

  Coloring-tree nodes stored in 64-node chunks.

def HadwigerNelsonBounds.partsGadgetTreeNodeAt (nodes : Array (Array PartsGadgetTreeNode)) (index : ℕ) : Option PartsGadgetTreeNode

Constant-depth lookup in a tree stored as 64-node chunks.

Equations

• HadwigerNelsonBounds.partsGadgetTreeNodeAt nodes index = match nodes[index / 64]? with | none => none | some chunk => chunk[index % 64]?

def HadwigerNelsonBounds.PartsGadgetProper (coloring : Fin 73 → Fin 4) : Prop

Properness on every listed unit edge.

Equations

• HadwigerNelsonBounds.PartsGadgetProper coloring = ∀ (vertex neighbor : Fin 73), neighbor ∈ HadwigerNelsonBounds.partsGadgetNeighbors vertex → coloring vertex ≠ coloring neighbor

def HadwigerNelsonBounds.PartsGadgetNoMono (coloring : Fin 73 → Fin 4) : Prop

Every listed sqrt-three triangle is non-monochromatic.

Equations

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

def HadwigerNelsonBounds.PartsGadgetValid (coloring : Fin 73 → Fin 4) : Prop

The two constraints used by the second-stage checker.

Equations

• HadwigerNelsonBounds.PartsGadgetValid coloring = (HadwigerNelsonBounds.PartsGadgetProper coloring ∧ HadwigerNelsonBounds.PartsGadgetNoMono coloring)

def HadwigerNelsonBounds.PartsGadgetExtends (coloring : Fin 73 → Fin 4) (path : List PartsGadgetAssignment) : Prop

A coloring agrees with every assignment on a certificate path.

Equations

• HadwigerNelsonBounds.PartsGadgetExtends coloring path = ∀ assignment ∈ path, coloring assignment.vertex = assignment.color

def HadwigerNelsonBounds.PartsGadgetHasColor (path : List PartsGadgetAssignment) (vertex : Fin 73) (color : Fin 4) : Prop

The path already assigns a given color to a vertex.

Equations

• HadwigerNelsonBounds.PartsGadgetHasColor path vertex color = ∃ assignment ∈ path, assignment.vertex = vertex ∧ assignment.color = color

def HadwigerNelsonBounds.PartsGadgetBlocks (path : List PartsGadgetAssignment) (vertex : Fin 73) (color : Fin 4) : Prop

A path blocks a color through an edge or a monochromatic triple.

Equations

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

def HadwigerNelsonBounds.partsGadgetColors : List (Fin 4)

The four colors, as executable data.

Equations

• HadwigerNelsonBounds.partsGadgetColors = [0, 1, 2, 3]

theorem HadwigerNelsonBounds.mem_partsGadgetColors (color : Fin 4) : color ∈ partsGadgetColors

def HadwigerNelsonBounds.PartsGadgetHasColorB (path : List PartsGadgetAssignment) (vertex : Fin 73) (color : Fin 4) : Bool

Executable path-color lookup.

Equations

• HadwigerNelsonBounds.PartsGadgetHasColorB path vertex color = path.any fun (assignment : HadwigerNelsonBounds.PartsGadgetAssignment) => assignment.vertex == vertex && assignment.color == color

theorem HadwigerNelsonBounds.partsGadgetHasColorB_eq_true {path : List PartsGadgetAssignment} {vertex : Fin 73} {color : Fin 4} : PartsGadgetHasColorB path vertex color = true ↔ PartsGadgetHasColor path vertex color

def HadwigerNelsonBounds.PartsGadgetBlocksB (path : List PartsGadgetAssignment) (vertex : Fin 73) (color : Fin 4) : Bool

Executable counterpart of PartsGadgetBlocks.

Equations

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

theorem HadwigerNelsonBounds.partsGadgetBlocksB_eq_true {path : List PartsGadgetAssignment} {vertex : Fin 73} {color : Fin 4} : PartsGadgetBlocksB path vertex color = true ↔ PartsGadgetBlocks path vertex color

def HadwigerNelsonBounds.PartsGadgetForcedB (path : List PartsGadgetAssignment) (assignment : PartsGadgetAssignment) : Bool

A forced assignment is the only color not blocked by the path.

Equations

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

def HadwigerNelsonBounds.PartsGadgetRunStemB : List PartsGadgetAssignment → List PartsGadgetAssignment → Option (List PartsGadgetAssignment)

Execute a sequence of forced assignments.

Equations

• One or more equations did not get rendered due to their size.
• HadwigerNelsonBounds.PartsGadgetRunStemB [] x✝ = some x✝

def HadwigerNelsonBounds.PartsGadgetVerifiesNodeB (nodes : Array (Array PartsGadgetTreeNode)) : ℕ → List PartsGadgetAssignment → ℕ → Bool

Executable checker for a compressed contradiction tree.

Equations

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

def HadwigerNelsonBounds.PartsGadgetCertificate.Verifies (certificate : PartsGadgetCertificate) : Prop

Check a certificate from node zero with enough acyclic-tree fuel.

Equations

• certificate.Verifies = (HadwigerNelsonBounds.PartsGadgetVerifiesNodeB certificate.nodes (certificate.nodeCount + 1) certificate.roots 0 = true)

@[implicit_reducible]

instance HadwigerNelsonBounds.instDecidableVerifies_1 (certificate : PartsGadgetCertificate) : Decidable certificate.Verifies

Equations

• HadwigerNelsonBounds.instDecidableVerifies_1 certificate = id inferInstance

theorem HadwigerNelsonBounds.not_partsGadgetBlocks_of_valid {coloring : Fin 73 → Fin 4} (hvalid : PartsGadgetValid coloring) (path : List PartsGadgetAssignment) (hextends : PartsGadgetExtends coloring path) (vertex : Fin 73) : ¬PartsGadgetBlocks path vertex (coloring vertex)

theorem HadwigerNelsonBounds.partsGadgetForcedB_sound {coloring : Fin 73 → Fin 4} (hvalid : PartsGadgetValid coloring) {path : List PartsGadgetAssignment} (hextends : PartsGadgetExtends coloring path) {assignment : PartsGadgetAssignment} (hforced : PartsGadgetForcedB path assignment = true) : coloring assignment.vertex = assignment.color

theorem HadwigerNelsonBounds.partsGadgetRunStemB_sound {coloring : Fin 73 → Fin 4} (hvalid : PartsGadgetValid coloring) {stem path extended : List PartsGadgetAssignment} : PartsGadgetRunStemB stem path = some extended → PartsGadgetExtends coloring path → PartsGadgetExtends coloring extended

theorem HadwigerNelsonBounds.partsGadgetVerifiesNodeB_unsat {nodes : Array (Array PartsGadgetTreeNode)} {coloring : Fin 73 → Fin 4} (hvalid : PartsGadgetValid coloring) {fuel : ℕ} {path : List PartsGadgetAssignment} {index : ℕ} : PartsGadgetVerifiesNodeB nodes fuel path index = true → PartsGadgetExtends coloring path → False

theorem HadwigerNelsonBounds.PartsGadgetCertificate.not_colorable (certificate : PartsGadgetCertificate) (hverify : certificate.Verifies) {coloring : Fin 73 → Fin 4} (hvalid : PartsGadgetValid coloring) (hroots : PartsGadgetExtends coloring certificate.roots) : False

A verified coloring tree rules out every valid coloring extending its roots.