A sound checker for Parts coloring trees

Unary stretches of a coloring tree are stored as forced-color stems. A tree node therefore ends at either a genuine branch or an uncolorable leaf. This is the same certificate as the source coloring diagram, but avoids artificial recursion depth from long chains of forced assignments.

structure HadwigerNelsonBounds.PartsAssignment : Type

A vertex-color assignment on the finite Parts graph.

• vertex : Fin 481

  Assigned graph vertex.

• color : Fin 4

  Assigned color.

def HadwigerNelsonBounds.instDecidableEqPartsAssignment.decEq (x✝ x✝¹ : PartsAssignment) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance HadwigerNelsonBounds.instDecidableEqPartsAssignment : DecidableEq PartsAssignment

Equations

• HadwigerNelsonBounds.instDecidableEqPartsAssignment = HadwigerNelsonBounds.instDecidableEqPartsAssignment.decEq

structure HadwigerNelsonBounds.PartsTreeNode : Type

A compressed coloring-tree node: a forced stem followed by a branch/leaf.

• stem : List PartsAssignment

  Unary forced assignments preceding the branch.

• vertex : Fin 481

  Vertex branched on after the forced stem.

• children : Fin 4 → ℕ

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

def HadwigerNelsonBounds.PartsTreeNode.child (node : PartsTreeNode) (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 | n.succ => some n

structure HadwigerNelsonBounds.PartsCertificate : Type

A root coloring together with its compressed contradiction tree.

• roots : List PartsAssignment

  Fixed root assignments.

• nodeCount : ℕ

  Number of nodes addressable in the chunked array.

• nodes : Array (Array PartsTreeNode)

  Coloring-tree nodes stored in 64-node chunks.

def HadwigerNelsonBounds.partsTreeNodeAt (nodes : Array (Array PartsTreeNode)) (index : ℕ) : Option PartsTreeNode

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

Equations

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

def HadwigerNelsonBounds.PartsBlocks (path : List PartsAssignment) (vertex : Fin 481) (color : Fin 4) : Prop

A path assignment blocks color at vertex through a unit edge.

Equations

• HadwigerNelsonBounds.PartsBlocks path vertex color = ∃ assignment ∈ path, assignment.color = color ∧ HadwigerNelsonBounds.partsAdjacent vertex assignment.vertex = true

def HadwigerNelsonBounds.PartsExtends (coloring : Fin 481 → Fin 4) (path : List PartsAssignment) : Prop

A coloring agrees with every assignment on a certificate path.

Equations

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

def HadwigerNelsonBounds.PartsProper (coloring : Fin 481 → Fin 4) : Prop

Properness for the exact unit edges recognized by the certificate.

Equations

• HadwigerNelsonBounds.PartsProper coloring = ∀ ⦃v w : Fin 481⦄, HadwigerNelsonBounds.partsAdjacent v w = true → coloring v ≠ coloring w

def HadwigerNelsonBounds.partsColors : List (Fin 4)

The four colors, as data for the executable checker.

Equations

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

theorem HadwigerNelsonBounds.mem_partsColors (color : Fin 4) : color ∈ partsColors

def HadwigerNelsonBounds.PartsBlocksB (path : List PartsAssignment) (vertex : Fin 481) (color : Fin 4) : Bool

Executable counterpart of PartsBlocks.

Equations

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

theorem HadwigerNelsonBounds.partsBlocksB_eq_true {path : List PartsAssignment} {vertex : Fin 481} {color : Fin 4} : PartsBlocksB path vertex color = true ↔ PartsBlocks path vertex color

def HadwigerNelsonBounds.PartsForcedB (path : List PartsAssignment) (assignment : PartsAssignment) : Bool

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

Equations

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

def HadwigerNelsonBounds.PartsRunStemB : List PartsAssignment → List PartsAssignment → Option (List PartsAssignment)

Execute a sequence of forced assignments, returning the extended path.

Equations

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

def HadwigerNelsonBounds.PartsVerifiesNodeB (nodes : Array (Array PartsTreeNode)) : ℕ → List PartsAssignment → ℕ → Bool

Executable checker for a compressed coloring tree.

Equations

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

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

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

Equations

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

@[implicit_reducible]

instance HadwigerNelsonBounds.instDecidableVerifies (certificate : PartsCertificate) : Decidable certificate.Verifies

Equations

• HadwigerNelsonBounds.instDecidableVerifies certificate = id inferInstance

theorem HadwigerNelsonBounds.not_partsBlocks_of_proper {coloring : Fin 481 → Fin 4} (hproper : PartsProper coloring) (path : List PartsAssignment) (hextends : PartsExtends coloring path) (vertex : Fin 481) : ¬PartsBlocks path vertex (coloring vertex)

theorem HadwigerNelsonBounds.partsForcedB_sound {coloring : Fin 481 → Fin 4} (hproper : PartsProper coloring) {path : List PartsAssignment} (hextends : PartsExtends coloring path) {assignment : PartsAssignment} (hforced : PartsForcedB path assignment = true) : coloring assignment.vertex = assignment.color

theorem HadwigerNelsonBounds.partsRunStemB_sound {coloring : Fin 481 → Fin 4} (hproper : PartsProper coloring) {stem path extended : List PartsAssignment} : PartsRunStemB stem path = some extended → PartsExtends coloring path → PartsExtends coloring extended

theorem HadwigerNelsonBounds.partsVerifiesNodeB_unsat {nodes : Array (Array PartsTreeNode)} {coloring : Fin 481 → Fin 4} (hproper : PartsProper coloring) {fuel : ℕ} {path : List PartsAssignment} {index : ℕ} : PartsVerifiesNodeB nodes fuel path index = true → PartsExtends coloring path → False

theorem HadwigerNelsonBounds.PartsCertificate.not_colorable (certificate : PartsCertificate) (hverify : certificate.Verifies) {coloring : Fin 481 → Fin 4} (hproper : PartsProper coloring) (hroots : PartsExtends coloring certificate.roots) : False

Soundness of a checked Parts coloring tree.