Critical-radius cover bound from a tight center

Open

Erdos9796Mission.critical_cover_card_le_nine_of_tight_center

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

convex-positiondiscrete-geometryerdos-97-96

Let $A$ be a finite set of points in strictly convex position in the Euclidean plane. Assume every vertex of $A$ has at least four other points of $A$ at some common positive distance, and that every point of $A$ is covered by a critical circle centered at another point of $A$ (an exact four-point distance class that is unique at its center). Assume moreover a distinguished tight pair: a center $p_0 \in A$ and a radius $r_0 > 0$ with

|\{q \in A : \mathrm{dist}(p_0, q) = r_0\}| = 4,

and such that no other positive radius at $p_0$ carries four or more points of $A$ . Then

|A| \le 9.

This is the geometric core of the critical-radius cover bound, with the covering witness made explicit. Its proof needs the convex-position geometry of exact four-point circles and is left open.

Formalization Note Strict convex position is ConvexIndep, and the four-witness property is HasNEquidistantProperty 4.

Closed by the mission owner on 2026-09-13 after the Kruer–Kohlmeyer–Price negative resolution of Erdős 96 and 97. No further work is requested on this historical project task. This retirement is administrative and does not assert that this individual lemma is false. The resolution is recorded on Erdos9796Mission.problem97, Erdos9796Mission.problem96, and Erdos9796Mission.combined.

Preamble

import Definitions.Def_Erdos9796Mission
open Erdos9796Mission
open Classical

Formal statement

theorem Erdos9796Mission.critical_cover_card_le_nine_of_tight_center
    (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)
    (p₀ : Plane) (hp₀ : p₀ ∈ A) (r₀ : ℝ) (h0 : 0 < r₀)
    (hexact : (A.filter (fun q => dist p₀ q = r₀)).card = 4)
    (huniq : ∀ s : ℝ, 0 < s →
      4 ≤ (A.filter (fun q => dist p₀ q = s)).card → s = r₀) :
    A.card ≤ 9 := by sorry

Source

Decomposition of Erdos9796Mission.critical_radius_cover_card_le_nine (open frontier leaf of Prove2Me mission Erdős Problems 97 and 96), 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

View graph