Prove2Me

Deleting an unused witness point preserves four equidistant neighbours

Proved
Problem97.K4_delete_of_indeg_zero

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

deletiondescentdiscrete-geometryerdos-97witness-systems

Let A be a nonempty finite planar set in strictly convex position with four equidistant neighbours at every point, and let S be a witness system. If x belongs to A and to none of the selected witness classes, then deleting x leaves a nonempty strictly convex set in which every point still has four equidistant neighbours.

Preamble
/- Rehosted from Erdos9796Proof.P97.K4WitnessDeletion at source commit
   387e5b44ae26906725a4898b0a01c2d7345ddb38. -/
import Definitions.Def_Problem97_IsWitnessSystem
import Definitions.Def_Erdos9796Counting_Adapter
import Definitions.Def_Erdos9796Counting_Foundation

open scoped EuclideanGeometry
open Finset

open Problem97
Formal statement
theorem Problem97.K4_delete_of_indeg_zero {A : Finset ℝ²} (hne : A.Nonempty)
    (hconv : ConvexIndep A) (hK4 : HasNEquidistantProperty 4 A)
    {S : ℝ² → Finset ℝ²} (hS : IsWitnessSystem A S)
    {x : ℝ²} (hxA : x ∈ A) (hindeg0 : ∀ y ∈ A, x ∉ S y) :
    (A.erase x).Nonempty ∧ ConvexIndep (A.erase x) ∧
      HasNEquidistantProperty 4 (A.erase x) := by sorry
Source
https://github.com/mysticflounder/erdos-97-96-formalization/blob/387e5b44ae26906725a4898b0a01c2d7345ddb38/lean/Erdos9796Proof/P97/K4WitnessDeletion.lean#L43-L67

View graph