Aggregated edge-geometry checks for the finite gadget.

theorem HadwigerNelsonBounds.partsGadget_edgeCase {vertex neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors vertex) : PartsGadgetEdgeCase vertex neighbor