Base case: exclude a nine-vertex counterexample

Proved

Erdos9796Mission.finite_nine_exclusion

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

convex-positiondiscrete-geometryerdos-97-96unit-distances

For every set $A$ of exactly nine points in strictly convex position in the Euclidean plane, some vertex has no four other vertices at a common positive distance.

|A|=9\quad\Longrightarrow\quad\exists p\in A\;\forall r>0:\;|\{q\in A:\|p-q\|=r\}|\le3.

This is the exact-cardinality base case used by the repository's descent strategy. Its existing proof is separate from the unresolved large-cardinality descent.

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.finite_nine_exclusion :
    ∀ A : Finset Plane, A.card = 9 → ConvexIndep (A : Set Plane) → ¬ HasNEquidistantProperty 4 A := by sorry

Source

https://github.com/mysticflounder/erdos-97-96-formalization/blob/757d852766f377f7c1a0ffeeef6d3526bc0cb7a4/lean/Erdos9796Proof/P97/N9Endpoint/Closure.lean#L56

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$ has exactly $9$ elements and every point $a\in A$ is outside the real convex hull of $A\setminus\{a\}$ , then it is false that every point $p\in A$ has a positive real radius $r>0$ for which the filtered set $\{q\in A : \operatorname{dist}(p,q)=r\}$ has cardinality at least $4$ .

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