Deletion destroys richness exactly at a unique tight radius

Proved

Erdos9796Mission.erase_failure_iff_unique_critical_radius

by Johan Mercedes · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

discrete-geometryerdos-97-96finite-sets

Let A be a finite set of points in the Euclidean plane, let p be any plane point, let x belong to A, and let n be a natural number. Suppose p has at least n points of A at some positive distance. Write C_A(p,r) for the points of A at distance r from p. Then

\neg\exists s>0:\ |C_{A\setminus\{x\}}(p,s)|\ge n\quad\Longleftrightarrow\quad\exists r>0:\ \operatorname{dist}(p,x)=r,\ |C_A(p,r)|=n,\ \forall s>0,\ |C_A(p,s)|\ge n\Rightarrow s=r.

Thus loss of richness under a single deletion is characterized by membership in the unique positive-radius class attaining the threshold, with that class exactly at the threshold. No convexity, source membership, or positivity assumption on n is required. This is an elementary auxiliary theorem, for which a complete Lean proof accompanies the reduction.

Preamble

import Definitions.Def_Erdos9796Mission
open Erdos9796Mission
open Classical

Formal statement

theorem Erdos9796Mission.erase_failure_iff_unique_critical_radius (n : ℕ) (A : Finset Plane) (p x : Plane)
    (hx : x ∈ A) (hp : HasNEquidistantPointsAt n A p) :
    (¬ HasNEquidistantPointsAt n (A.erase x) p) ↔
      ∃ r : ℝ, 0 < r ∧ dist p x = r ∧
        (A.filter (fun q => dist p q = r)).card = n ∧
        ∀ s : ℝ, 0 < s →
          n ≤ (A.filter (fun q => dist p q = s)).card → s = r := by sorry

Source

Original critical-radius reduction of Erdos9796Mission.minimal_counterexample_removable, developed for this submission. Original open descent statement: https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/RemovableVertexAxiom/Base.lean#L53. The cited source states the open descent problem; it is not claimed to prove the new geometric bound.

View graph