Erdős 97 convex-octagon formalization: Radius

def Erdos97Octagon.OctagonIncidence.Mutual (Q : OctagonIncidence) (a b : Vertex) : Prop

Two centres are mutually selected.

Equations

• Q.Mutual a b = (b ∈ Q.targets a ∧ a ∈ Q.targets b)

def Erdos97Octagon.OctagonIncidence.SameComponent (Q : OctagonIncidence) (a b : Vertex) : Prop

Two centres lie in the same connected component of mutual selections.

Equations

• Q.SameComponent a b = Relation.ReflTransGen Q.Mutual a b

def Erdos97Octagon.OctagonIncidence.LabelledEdge (Q : OctagonIncidence) (root a b : Vertex) : Prop

An undirected pair is labelled by the radius of a mutual component when one endpoint in that component selects the other.

Equations

• Q.LabelledEdge root a b = (Q.SameComponent root a ∧ b ∈ Q.targets a ∨ Q.SameComponent root b ∧ a ∈ Q.targets b)

theorem Erdos97Octagon.exists_positive_radii {p : Vertex → Plane} (hp : Function.Injective p) (Q : OctagonIncidence) (hR : Realises p Q) : ∃ (radius : Vertex → ℝ), (∀ (v : Vertex), 0 < radius v) ∧ ∀ (v w : Vertex), w ∈ Q.targets v → dist (p v) (p w) = radius v

An injective realisation admits a positive radius at every centre.

theorem Erdos97Octagon.radius_eq_of_mutual {p : Vertex → Plane} {Q : OctagonIncidence} {radius : Vertex → ℝ} (hR : ∀ (v w : Vertex), w ∈ Q.targets v → dist (p v) (p w) = radius v) {a b : Vertex} (hab : Q.Mutual a b) : radius a = radius b

Mutual centres have equal radii in any realisation.

theorem Erdos97Octagon.radius_eq_of_sameComponent {p : Vertex → Plane} {Q : OctagonIncidence} {radius : Vertex → ℝ} (hR : ∀ (v w : Vertex), w ∈ Q.targets v → dist (p v) (p w) = radius v) {a b : Vertex} (hab : Q.SameComponent a b) : radius a = radius b

Radii are constant along a mutual connected component.

theorem Erdos97Octagon.dist_eq_radius_of_labelledEdge {p : Vertex → Plane} {Q : OctagonIncidence} {radius : Vertex → ℝ} (hR : ∀ (v w : Vertex), w ∈ Q.targets v → dist (p v) (p w) = radius v) {root a b : Vertex} (hab : Q.LabelledEdge root a b) : dist (p a) (p b) = radius root

A labelled edge has the radius of its mutual component.