Aggregated central-inversion facts for the finite gadget.

theorem HadwigerNelsonBounds.partsGadgetNegation_neighbor {vertex neighbor : Fin 73} (hadj : neighbor ∈ partsGadgetNeighbors vertex) : partsGadgetNegation neighbor ∈ partsGadgetNeighbors (partsGadgetNegation vertex)

theorem HadwigerNelsonBounds.partsGadgetNegation_triple {vertex : Fin 73} {pair : Fin 73 × Fin 73} (hpair : pair ∈ partsGadgetTriplePairs vertex) : (partsGadgetNegation pair.1, partsGadgetNegation pair.2) ∈ partsGadgetTriplePairs (partsGadgetNegation vertex) ∨ (partsGadgetNegation pair.2, partsGadgetNegation pair.1) ∈ partsGadgetTriplePairs (partsGadgetNegation vertex)

theorem HadwigerNelsonBounds.partsGadgetTriangleWitness_valid {vertex : Fin 73} {witness : PartsGadgetTriangleWitnessData} (hwitness : witness ∈ partsGadgetTriangleWitnesses vertex) : witness.Valid vertex