Open geometric core: critical-radius cover has at most nine vertices
OpenErdos9796Mission.critical_radius_cover_card_le_nineThis is an open geometric subproblem proposed for the removable-vertex reduction; no proof of this bound is claimed.
Let A be a finite convexly independent set in the Euclidean plane, and write C_A(p,r) for its points at distance r from p. Assume every point of A has at least four other points at some common positive distance. Assume also that every x in A belongs to a critical circle centered at a different point p of A: its radius r is positive, its complete distance class has exactly four points, and it is the only positive radius at p with at least four points. Under these hypotheses the proposed conclusion is
The all-centers-rich condition is separate and essential to the proposed statement: coverage by selected circles alone is not asserted to imply this bound. The conclusion bounds the whole set, not just one distance class. This child is stronger than the original global-minimality descent formulation, and its geometric conclusion remains unproved. It contains no numerical search certificate or hidden finite-cardinality restriction.
import Definitions.Def_Erdos9796Mission open Erdos9796Mission open Classical
theorem Erdos9796Mission.critical_radius_cover_card_le_nine
(A : Finset Plane) (hconv : ConvexIndep (A : Set Plane))
(hrich : HasNEquidistantProperty 4 A)
(hcover : ∀ x ∈ A, ∃ p ∈ A.erase x, ∃ r : ℝ,
0 < r ∧ dist p x = r ∧
(A.filter (fun q => dist p q = r)).card = 4 ∧
∀ s : ℝ, 0 < s →
4 ≤ (A.filter (fun q => dist p q = s)).card → s = r) :
A.card ≤ 9 := by sorry