Complete normalized root dispatch

The 1,023-node trie has 432 leaves, one for each proper normalized coloring of the 13-vertex 2-Golomb root. Every leaf names a separately checked Parts tree.

def HadwigerNelsonBounds.partsRootDecisionNodes : Array (Array PartsRootNode)

All chunks of the complete normalized root-decision trie.

Equations

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

theorem HadwigerNelsonBounds.partsRootDecision_verifies : PartsRootVerifiesNodeB partsRootDecisionNodes 1024 partsNormalizedRootPath 0 = true

theorem HadwigerNelsonBounds.no_parts_coloring_of_normalized_root {coloring : Fin 481 → Fin 4} (hproper : PartsProper coloring) (hroots : PartsExtends coloring partsNormalizedRootPath) : False

No proper coloring of the Parts graph extends the normalized fixed root.