Deleting a removable vertex gives a smaller counterexample
ProvedErdos9796Mission.smaller_counterexample_of_removabledescentdiscrete-geometryerdos-97
Let A be a finite planar point set in strictly convex position with at least two points. If A has a vertex whose deletion preserves four equidistant witnesses at every remaining vertex, then there exists a nonempty point set with fewer points than A that remains in strictly convex position and retains the four-witness property.
Preamble
import Definitions.Def_Erdos9796Mission_RemovableVertex open Erdos9796Mission
Formal statement
theorem Erdos9796Mission.smaller_counterexample_of_removable
{A : Finset Plane} (hconv : ConvexIndep (A : Set Plane))
{x : Plane} (hrem : IsRemovableVertex A x) (hcard : 1 < A.card) :
∃ B : Finset Plane, B.Nonempty ∧ B.card < A.card ∧
ConvexIndep (B : Set Plane) ∧ HasNEquidistantProperty 4 B := by sorrySource