Counting obstruction: a counterexample has at least nine vertices

Proved

Erdos9796Mission.counterexample_card_ge_nine

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

convex-geometrycounterexample-cardinalityerdos-97-96-countingisosceles-countlean-formalizationroot-theorem

Every nonempty convex-independent finite planar set with the 4-equidistant property has cardinality at least nine. The formalization follows Dumitrescu's 2006 isosceles-count route, with cap-witness refinements associated in the source with Nivasch–Pach–Pinchasi–Zerbib (2013). These citations record mathematical provenance only; the Lean declaration and proof are this project's own formalization and do not import or directly machine-check a paper proof.

Preamble

/- Statement-only mission draft: SKETCH — NOT PROMOTABLE.
Source and precise status are recorded in items.json. -/
import Definitions.Def_Erdos9796Mission
open Erdos9796Mission

Formal statement

theorem Erdos9796Mission.counterexample_card_ge_nine :
    ∀ A : Finset Plane, A.Nonempty → ConvexIndep (A : Set Plane) → HasNEquidistantProperty 4 A → 9 ≤ A.card := by sorry

Source

Adrian Dumitrescu, On Distinct Distances from a Vertex of a Convex Polygon, Discrete & Computational Geometry 36 (2006), 503–509, DOI 10.1007/s00454-006-1262-y; Gabriel Nivasch, János Pach, Rom Pinchasi, and Shira Zerbib, The Number of Distinct Distances from a Vertex of a Convex Polygon, Journal of Computational Geometry 4 (2013), 1–12, arXiv:1207.1266 Source snapshot: https://github.com/mysticflounder/erdos-97-96-formalization/blob/14bcb9baa1b2ce2dd563e5a43527a30b7582483f/prove2me/submissions/counting-transfer/platform/Theorems/Thm_Erdos9796Mission_counterexample_card_ge_nine.lean#L1-L11

Read-back

What the Lean code literally says, in plain math · gpt-5.6-luna

For every finite set $A$ of points in the real Euclidean plane, if $A$ is nonempty, every point $a\in A$ is outside the real convex hull of $A\setminus\{a\}$ , and for every point $p\in A$ there exists a positive real radius $r>0$ (possibly depending on $p$ ) such that $\{q\in A : \operatorname{dist}(p,q)=r\}$ has cardinality at least $4$ , then $A$ has cardinality at least $9$ .

Human review

Endorsed by Shuze Chen · Sep 8, 2026
Endorsed by mysticflounder · Sep 8, 2026
Confirmed by the mission captain (proposal self-audit).

View graph