Aggregated kernel and routing checks for the hard normalized cases.

theorem HadwigerNelsonBounds.partsGadgetHardCertificates_verify (index : Fin 31) : (partsGadgetHardCertificates index).Verifies

Every hard-case leaf certificate has been kernel checked.

theorem HadwigerNelsonBounds.partsGadgetHardCaseTree_verifiesRouting : partsGadgetHardCaseTree.VerifiesRouting partsGadgetHardCertificates

The case router covers every unblocked normalized color.