Equidistant witnesses are a pinned-multiplicity lower bound
ProvedErdos9796Mission.hasNEquidistantPointsAt_iff_le_pinnedMultiplicitydiscrete-geometryerdos-97pinned-distances
For n > 0, a positive radius containing at least n points gives pinned distance multiplicity at least n; conversely, that multiplicity bound supplies a positive radius containing at least n points.
Preamble
import Definitions.Def_Erdos9796Mission_PinnedMultiplicity
Formal statement
theorem Erdos9796Mission.hasNEquidistantPointsAt_iff_le_pinnedMultiplicity
{A : Finset Erdos9796Mission.Plane} {p : Erdos9796Mission.Plane} {n : ℕ}
(hn : 0 < n) :
Erdos9796Mission.HasNEquidistantPointsAt n A p ↔
n ≤ Erdos9796Mission.pinnedMultiplicity A p := by sorrySource