Erdős 97 convex-octagon formalization: Obstructions #
theorem
Erdos97Octagon.no_labelled_k4
{p : Vertex → Plane}
(hp : Function.Injective p)
{Q : OctagonIncidence}
(hR : Realises p Q)
{root a b c d : Vertex}
(had : a ≠ d)
(hab : Q.LabelledEdge root a b)
(hac : Q.LabelledEdge root a c)
(had' : Q.LabelledEdge root a d)
(hbc : Q.LabelledEdge root b c)
(hbd : Q.LabelledEdge root b d)
(hcd : Q.LabelledEdge root c d)
:
A four-clique in one radius-labelled graph is impossible in the plane.
theorem
Erdos97Octagon.no_labelled_hub_pentagon
{p : Vertex → Plane}
(hp : Function.Injective p)
{Q : OctagonIncidence}
(hR : Realises p Q)
{root o a b c d e : Vertex}
(hoa : Q.LabelledEdge root o a)
(hob : Q.LabelledEdge root o b)
(hoc : Q.LabelledEdge root o c)
(hod : Q.LabelledEdge root o d)
(hoe : Q.LabelledEdge root o e)
(hab : Q.LabelledEdge root a b)
(hbc : Q.LabelledEdge root b c)
(hcd : Q.LabelledEdge root c d)
(hde : Q.LabelledEdge root d e)
(hea : Q.LabelledEdge root e a)
:
A hub and a five-cycle in one radius-labelled graph are impossible.
theorem
Erdos97Octagon.no_labelled_cycle_square_strip
{p : Vertex → Plane}
(hp : Function.Injective p)
{Q : OctagonIncidence}
(hR : Realises p Q)
{root o x1 x2 x3 x4 x5 x6 : Vertex}
(e01 : Q.LabelledEdge root o x1)
(e02 : Q.LabelledEdge root o x2)
(e06 : Q.LabelledEdge root o x6)
(e12 : Q.LabelledEdge root x1 x2)
(e13 : Q.LabelledEdge root x1 x3)
(e23 : Q.LabelledEdge root x2 x3)
(e24 : Q.LabelledEdge root x2 x4)
(e34 : Q.LabelledEdge root x3 x4)
(e35 : Q.LabelledEdge root x3 x5)
(e45 : Q.LabelledEdge root x4 x5)
(e46 : Q.LabelledEdge root x4 x6)
(e56 : Q.LabelledEdge root x5 x6)
:
A seven-vertex cycle-square strip in one radius-labelled graph is impossible.