Root-case dispatcher for the Parts certificate

The dispatcher colors the nine unfixed vertices of the 13-vertex 2-Golomb root. Its leaves point to the appropriate one of the 432 checked symmetry and color variants from PartsFirstStage.

inductive HadwigerNelsonBounds.PartsRootNode : Type

A branch in the root trie, or a leaf selecting a checked Parts tree.

• branch (vertex : Fin 481) (children : Fin 4 → ℕ) : PartsRootNode
• leaf (base : Fin 36) (symmetry : Fin 6) (swap : Bool) : PartsRootNode

def HadwigerNelsonBounds.partsRootChild (children : Fin 4 → ℕ) (color : Fin 4) : Option ℕ

Decode a branch's zero-sentinel child table.

Equations

• HadwigerNelsonBounds.partsRootChild children color = match children color with | 0 => none | n.succ => some n

def HadwigerNelsonBounds.partsRootNodeAt (nodes : Array (Array PartsRootNode)) (index : ℕ) : Option PartsRootNode

Constant-depth lookup in 64-node root-trie chunks.

Equations

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

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

Executable membership of an exact assignment in a current path.

Equations

• HadwigerNelsonBounds.PartsAssignmentInPathB path assignment = path.any fun (current : HadwigerNelsonBounds.PartsAssignment) => current == assignment

def HadwigerNelsonBounds.PartsRootsInPathB (path roots : List PartsAssignment) : Bool

Every selected certificate root already occurs in the root-trie path.

Equations

• HadwigerNelsonBounds.PartsRootsInPathB path roots = roots.all (HadwigerNelsonBounds.PartsAssignmentInPathB path)

theorem HadwigerNelsonBounds.partsRootsInPathB_sound {coloring : Fin 481 → Fin 4} {path roots : List PartsAssignment} (hcheck : PartsRootsInPathB path roots = true) (hextends : PartsExtends coloring path) : PartsExtends coloring roots

def HadwigerNelsonBounds.PartsRootVerifiesNodeB (nodes : Array (Array PartsRootNode)) : ℕ → List PartsAssignment → ℕ → Bool

Executable checker for the finite root-case trie.

Equations

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

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

def HadwigerNelsonBounds.partsNormalizedRootPath : List PartsAssignment

The four fixed assignments after color normalization.

Equations

• HadwigerNelsonBounds.partsNormalizedRootPath = [{ vertex := 0, color := 3 }, { vertex := 195, color := 0 }, { vertex := 205, color := 0 }, { vertex := 215, color := 0 }]

theorem HadwigerNelsonBounds.partsRootDecision_not_colorable (nodes : Array (Array PartsRootNode)) (nodeCount : ℕ) (hverify : PartsRootVerifiesNodeB nodes (nodeCount + 1) partsNormalizedRootPath 0 = true) {coloring : Fin 481 → Fin 4} (hproper : PartsProper coloring) (hroots : PartsExtends coloring partsNormalizedRootPath) : False

A checked root trie eliminates every proper coloring extending the fixed root.