Routing between independently checked gadget certificates

Large coloring trees are split into small, default-heartbeat certificates. This checker verifies that the roots of those certificates cover every unblocked color branch. Certificate soundness remains a theorem of Lean, while each small tree is independently reduced by the kernel.

inductive HadwigerNelsonBounds.PartsGadgetCaseNode (certificateCount : ℕ) : Type

A routing node either selects a checked certificate or branches on a color.

• leaf {certificateCount : ℕ} (certificate : Fin certificateCount) : PartsGadgetCaseNode certificateCount
• branch {certificateCount : ℕ} (vertex : Fin 73) (children : Fin 4 → ℕ) : PartsGadgetCaseNode certificateCount

def HadwigerNelsonBounds.PartsGadgetCaseNode.child {certificateCount : ℕ} (node : PartsGadgetCaseNode certificateCount) (color : Fin 4) : Option ℕ

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

Equations

• (HadwigerNelsonBounds.PartsGadgetCaseNode.leaf certificate).child color = none
• (HadwigerNelsonBounds.PartsGadgetCaseNode.branch vertex children).child color = match children color with | 0 => none | index.succ => some index

structure HadwigerNelsonBounds.PartsGadgetCaseTree (certificateCount : ℕ) : Type

A finite router covering a normalized root path by small certificates.

• roots : List PartsGadgetAssignment

  Fixed normalized assignments shared by every routed case.

• nodeCount : ℕ

  Number of routing nodes.

• nodes : Array (PartsGadgetCaseNode certificateCount)

  Branch and certificate-leaf nodes.

def HadwigerNelsonBounds.PartsGadgetCaseVerifiesNodeB {certificateCount : ℕ} (certificates : Fin certificateCount → PartsGadgetCertificate) (nodes : Array (PartsGadgetCaseNode certificateCount)) : ℕ → List PartsGadgetAssignment → ℕ → Bool

Check routing, but leave each selected certificate proof as a separate fact.

Equations

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

def HadwigerNelsonBounds.PartsGadgetCaseTree.VerifiesRouting {certificateCount : ℕ} (tree : PartsGadgetCaseTree certificateCount) (certificates : Fin certificateCount → PartsGadgetCertificate) : Prop

The root-routing check for a case tree.

Equations

• tree.VerifiesRouting certificates = (HadwigerNelsonBounds.PartsGadgetCaseVerifiesNodeB certificates tree.nodes (tree.nodeCount + 1) tree.roots 0 = true)

@[implicit_reducible]

instance HadwigerNelsonBounds.instDecidableVerifiesRouting {certificateCount : ℕ} (tree : PartsGadgetCaseTree certificateCount) (certificates : Fin certificateCount → PartsGadgetCertificate) : Decidable (tree.VerifiesRouting certificates)

Equations

• HadwigerNelsonBounds.instDecidableVerifiesRouting tree certificates = id inferInstance

theorem HadwigerNelsonBounds.partsGadgetCaseVerifiesNodeB_unsat {certificateCount : ℕ} {certificates : Fin certificateCount → PartsGadgetCertificate} (hcertificates : ∀ (index : Fin certificateCount), (certificates index).Verifies) {coloring : Fin 73 → Fin 4} (hvalid : PartsGadgetValid coloring) {fuel : ℕ} {nodes : Array (PartsGadgetCaseNode certificateCount)} {path : List PartsGadgetAssignment} {index : ℕ} : PartsGadgetCaseVerifiesNodeB certificates nodes fuel path index = true → PartsGadgetExtends coloring path → False

theorem HadwigerNelsonBounds.PartsGadgetCaseTree.not_colorable {certificateCount : ℕ} (tree : PartsGadgetCaseTree certificateCount) (certificates : Fin certificateCount → PartsGadgetCertificate) (hrouting : tree.VerifiesRouting certificates) (hcertificates : ∀ (index : Fin certificateCount), (certificates index).Verifies) {coloring : Fin 73 → Fin 4} (hvalid : PartsGadgetValid coloring) (hroots : PartsGadgetExtends coloring tree.roots) : False

A routed family of verified certificates rules out its normalized roots.