Exact-eleven endpoint: exclude an eleven-vertex counterexample

Open

Erdos9796Mission.finite_eleven_exclusion

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

convex-positiondiscrete-geometryerdos-97exact-cardinality

No convex-independent set of exactly eleven points in the Euclidean plane has four equidistant points at every vertex.

Preamble

/-
Copyright (c) 2026 Adam McKenna. All rights reserved.
Released under GPL-3.0-or-later as described in the file LICENSE.
Authors: Adam McKenna
-/

/- Statement-only Prove2Me transfer target: SKETCH — NOT PROMOTABLE.
The source proof and its trust boundary are recorded in the sibling provenance document. -/
import Definitions.Def_Erdos9796Mission

open Erdos9796Mission

Formal statement

theorem Erdos9796Mission.finite_eleven_exclusion :
    ∀ A : Finset Plane, A.card = 11 → ConvexIndep (A : Set Plane) →
      ¬ HasNEquidistantProperty 4 A := by sorry

Source

https://github.com/mysticflounder/erdos-97-96-formalization/blob/ff13d98d92694d0e460549031049f08357ff6150/lean/Erdos9796Proof/P97/FiniteN11.lean#L42-L78

View graph