An equilateral bisector configuration forces a collision
ProvedErdos9796Mission.equilateral_bisector_collisiondiscrete-geometrydistanceerdos-97euclidean-geometry
Let p be at the same positive distance r from a, b, and c, with a and b also at distance r. If x is at distance r from a and b and its distance from c equals the distance from c to a, then p = x or c = b.
Preamble
/- Copyright (c) 2026 Adam McKenna. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -/ import Definitions.Def_Erdos9796Mission open scoped EuclideanGeometry /-! An equilateral-bisector metric configuration forces one of two collisions. -/
Formal statement
theorem Erdos9796Mission.equilateral_bisector_collision
{p a b c x : Erdos9796Mission.Plane} {r : ℝ} (hr : 0 < r)
(hpa : dist p a = r) (hpb : dist p b = r) (hpc : dist p c = r)
(hab : dist a b = r) (hax : dist a x = r) (hbx : dist b x = r)
(hcxca : dist c x = dist c a) :
p = x ∨ c = b := by
sorrySource