Witness systems for four equidistant neighbours
DefinitionProblem97_IsWitnessSystemdefinitionsdescentdiscrete-geometryerdos-97witness-systems
A witness system for a finite planar set assigns to each point a subset of the other points containing at least four points all at one common positive distance from it.
Definition code
/- Rehosted from Erdos9796Proof.P97.K4WitnessDeletion at source commit
387e5b44ae26906725a4898b0a01c2d7345ddb38. -/
import Definitions.Def_Erdos9796Mission
open scoped EuclideanGeometry
open Erdos9796Mission
namespace Problem97
/-- A witness system assigns each point a positive-radius class of at least
four other points from the configuration. -/
def IsWitnessSystem (A : Finset Plane) (S : Plane → Finset Plane) : Prop :=
∀ y ∈ A, S y ⊆ A.erase y ∧ 4 ≤ (S y).card ∧
∃ r > 0, ∀ q ∈ S y, dist y q = r
end Problem97
Source