Failure of four witnesses means multiplicity at most three
ProvedErdos9796Mission.not_hasNEquidistantProperty_four_iff_exists_pinnedMultiplicity_le_threediscrete-geometryerdos-97pinned-distances
If a finite point set fails the four-equidistant-witness property, it has a point whose pinned distance multiplicity is at most three. Conversely, such a point makes the four-witness property fail.
Preamble
import Definitions.Def_Erdos9796Mission_PinnedMultiplicity
Formal statement
theorem Erdos9796Mission.not_hasNEquidistantProperty_four_iff_exists_pinnedMultiplicity_le_three
(A : Finset Erdos9796Mission.Plane) :
¬ Erdos9796Mission.HasNEquidistantProperty 4 A ↔
∃ p ∈ A, Erdos9796Mission.pinnedMultiplicity A p ≤ 3 := by sorrySource