Five equidistant neighbours give the fifty-five total-count bound at nine points
ProvedProblem97.fifty_five_le_iCount_of_card_nine_K4_of_five_equidistantcountingdiscrete-geometryerdos-97finite-nineisosceles-triangles
If A has nine points, every point has four equidistant witnesses, and one apex has at least five equidistant neighbours at one radius, then the total isosceles count of A is at least fifty-five.
Preamble
/- Copyright (c) 2026 Adam McKenna. All rights reserved. SPDX-License-Identifier: Apache-2.0 Author: Adam McKenna <adam@mysticflounder.ai> -/ import Definitions.Def_Erdos9796Counting_Foundation import Definitions.Def_Erdos9796Counting_IsoscelesCount open scoped EuclideanGeometry open Problem97 /-! # Fifty-five total isosceles pairs from the five-equidistant shape In a nine-point configuration with four equidistant neighbors at every vertex, five equidistant neighbors at one apex force the total isosceles count to be at least `55`. The statement is rehosted from `Erdos9796Proof.P97.IsoscelesCount` at source commit `bd8528ea10a12da2c84a10cc5897e36681c2e75d`. The counting method is attributed to Adrian Dumitrescu (2006); the Lean formalization is by Adam McKenna. -/
Formal statement
theorem Problem97.fifty_five_le_iCount_of_card_nine_K4_of_five_equidistant
{A : Finset ℝ²}
(hcard : A.card = 9) (hK4 : HasNEquidistantProperty 4 A)
{p : ℝ²} (hpA : p ∈ A) {S : Finset ℝ²}
(hScard : 5 ≤ S.card)
(hSsub : S ⊆ A.erase p)
(hSdist : ∃ r : ℝ, ∀ q ∈ S, dist p q = r) :
55 ≤ iCount A := by sorrySource