Erdős 97 convex-octagon formalization: Geometry Reduction

def Erdos97Octagon.HasFourEquidistant (p : Vertex → Plane) (v : Vertex) : Prop

A vertex has four other labelled vertices at one common distance.

Equations

• Erdos97Octagon.HasFourEquidistant p v = ∃ (S : Finset Erdos97Octagon.Vertex), S.card = 4 ∧ v ∉ S ∧ ∃ (r : ℝ), ∀ w ∈ S, dist (p v) (p w) = r

def Erdos97Octagon.Realises (p : Vertex → Plane) (Q : OctagonIncidence) : Prop

A labelled incidence system is realised by equal-distance rows in the plane.

Equations

• Erdos97Octagon.Realises p Q = ∀ (v : Erdos97Octagon.Vertex), ∃ (r : ℝ), ∀ w ∈ Q.targets v, dist (p v) (p w) = r

theorem Erdos97Octagon.three_collinear_not_convexIndependent {p : Vertex → Plane} (hC : ConvexIndependent ℝ p) {i j k : Vertex} (hij : i ≠ j) (hik : i ≠ k) (hjk : j ≠ k) (hCol : Collinear ℝ {p i, p j, p k}) : False

Three distinct members of a convex-independent family cannot be collinear.

theorem Erdos97Octagon.equidistantCentres_card_le_two {p : Vertex → Plane} (hC : ConvexIndependent ℝ p) {a b : Vertex} (hab : a ≠ b) : {v : Vertex | dist (p v) (p a) = dist (p v) (p b)}.card ≤ 2

At most two vertices of a convex-independent planar family are equidistant from any fixed pair of distinct vertices.

theorem Erdos97Octagon.pairSparse_of_realises {p : Vertex → Plane} (hC : ConvexIndependent ℝ p) (Q : OctagonIncidence) (hR : Realises p Q) : Q.PairSparse

A realisation in convex position has pair multiplicity at most two.

theorem Erdos97Octagon.incidence_of_all_hasFour {p : Vertex → Plane} (h : ∀ (v : Vertex), HasFourEquidistant p v) : ∃ (Q : OctagonIncidence), Realises p Q

Failure at every vertex canonically yields a four-target incidence system.

theorem Erdos97Octagon.reduction_of_all_hasFour {p : Vertex → Plane} (hC : ConvexIndependent ℝ p) (h : ∀ (v : Vertex), HasFourEquidistant p v) : ∃ (Q : OctagonIncidence), Realises p Q ∧ Q.PairSparse ∧ Q.Balanced

Any failed convex octagon produces a balanced, pair-sparse incidence system.