The polygonal redrawing of a finite plane graph

Bricks B7 and B8 of lem:polygonal-redrawing, and the headline theorem: every finite plane graph is drawn again, on the same abstract graph and the same vertices, with polygonal edges. Since the vertices of a plane graph are plane points and the redrawing leaves them where they are, the blueprint's "isomorphic plane drawing" is the identity isomorphism, and no Graph.IsIsomorphism is built or needed.

Three things the design did not have, and this module supplies

Simple polygonal paths. Graph.IsDrawing.edge_param asks for an injective parametrisation, and brick B6 delivers only a poly vertex list, which may cross itself. The blueprint's Lemma 1.1 makes the path simple "by subdividing at self-intersections and taking a simple path in the resulting finite graph"; Schoenflies/PolyPath.lean deferred that half, and without it brick B8 cannot discharge the drawing condition at all. IsArcList and PolyReaches.exists_arcList supply it, by an induction over the inductive relation rather than by an overlay graph: at each step the new segment is run backwards from its far end and stopped the first time it meets the polygon already built, and the old path is truncated there. That needs no plane geometry beyond exists_first_mem_Icc, and in particular no connectivity theorem for the overlay graph.

The contact point is on the frame. Graph.IsDrawing.exists_core states that the core meets the square about a vertex in exactly one point, but not that this point is on the square's boundary — and if it were interior the core would not lie in the plane minus the open squares, which is the carrier brick B5 speaks about, nor would the radial segment from the vertex reach it. Plane.supDist_eq_of_inter_eq_singleton closes the gap by connectedness: an interior contact point would make the core's trace on the square a nonempty proper clopen piece.

Radial arithmetic. That two radials of one square meet only at the centre, and that a radial meets the plane minus the open squares only at its far end, are both the statement that the sup distance to the centre is a faithful coordinate along a radius (Plane.supDist_lt_of_mem_segment, Plane.radial_meet). These are the "distinct radials in one square meet only at v" and "radials meet the replacement paths only at the designated boundary points" of brick B8's design, and neither is free.

Blueprint

Bricks B7 and B8 of lem:polygonal-redrawing (H6), and the lemma itself.

• Plane.supNorm_smul, Plane.supDist_add_smul, Plane.supDist_lt_of_mem_segment, Plane.segment_subset_closedSquare, Plane.radial_meet — the radial segments of brick B8.
• Plane.supDist_eq_of_inter_eq_singleton — a core's contact point lies on the frame of its square; the missing clause of brick B4.
• lastP, poly_snoc, IsArcList — a simple polygonal path, in the u :: t presentation that keeps every statement free of dependent nonemptiness proofs.
• isArcBetween_poly — the carrier of a simple polygonal path is an arc between its ends.
• IsArcList.truncate, IsArcList.snoc — cutting one at any of its points, and extending one by a segment that touches it only at its last vertex.
• PolyReaches.exists_arcList — every polygonal path contains a simple one; the deferred half of Lemma 1.1.
• Graph.polygonal_redrawing — lem:polygonal-redrawing, with bricks B7 and B8 inside its proof: the ε making the tubes about the cores pairwise disjoint, the component U e of the core inside its tube, and the assembly of radial, replacement path and radial.

Radial segments in a square

A segment from the centre of a square to a point of its boundary frame leaves the open square only at its far end, and two such segments in one square meet only at the centre. Those two facts are the whole of the "radials" half of brick B8, and both are statements about the sup distance scaling along a segment.

theorem Schoenflies.Plane.supNorm_smul (a : ℝ) (x : Plane) : (a • x).supNorm = |a| * x.supNorm

theorem Schoenflies.Plane.supDist_add_smul (c u : Plane) (t : ℝ) : (c + t • u).supDist c = |t| * u.supNorm

theorem Schoenflies.Plane.supDist_lt_of_mem_segment {c p x : Plane} (hpc : 0 < p.supDist c) (hx : x ∈ segment ℝ c p) (hne : x ≠ p) : x.supDist c < p.supDist c

Everything on the segment from c to p except p itself is strictly nearer to c than p is, in the sup metric. This is why a radial segment meets the frame of its square only at its far end.

theorem Schoenflies.Plane.openSquare_subset_closedSquare (c : Plane) (r : ℝ) : c.openSquare r ⊆ c.closedSquare r

A radial segment stays inside its square.

theorem Schoenflies.Plane.segment_subset_closedSquare {c p : Plane} {r : ℝ} (hr : 0 ≤ r) (hpc : p.supDist c ≤ r) : segment ℝ c p ⊆ c.closedSquare r

theorem Schoenflies.Plane.radial_meet {c c' p p' z : Plane} {r : ℝ} (hr : 0 < r) (hp : p.supDist c = r) (hp' : p'.supDist c' = r) (hpp' : p ≠ p') (hdisj : c ≠ c' → Disjoint (c.closedSquare r) (c'.closedSquare r)) (hz : z ∈ segment ℝ c p) (hz' : z ∈ segment ℝ c' p') : z = c

Two radials meet only at the centre. Two segments from the centres of two squares of a common radius r to points of their frames meet only where they can: if the centres are distinct the squares are disjoint, and if they agree the two far ends are pinned by the sup distance, which is injective along a radius.

Simple polygonal paths

poly vs is the carrier of a vertex list, and a general vertex list crosses itself. The drawing condition of a plane graph asks for an injective parametrisation, so what brick B8 needs is a vertex list whose carrier is an arc. IsArcList is exactly the condition that makes the concatenation of Schoenflies/Concatenate.lean apply at every step: consecutive vertices differ, and each segment meets the rest of the polygon only at the vertex they share.

The work of this section is PolyReaches.exists_arcList: any polygonal path inside a set contains a simple one with the same ends. That is the half of the blueprint's Lemma 1.1 which Schoenflies/PolyPath.lean deferred, and without it nothing downstream can discharge Graph.IsDrawing. The induction is over the inductive relation PolyReaches, and the step takes the first point at which the new segment, run backwards from its far end, meets the polygon already built, truncates there and appends.

def Schoenflies.lastP (u : Plane) (t : List Plane) : Plane

The last vertex of a nonempty vertex list, with the nonemptiness discharged by the cons. Carrying the list in the form u :: t removes every dependent proof argument from the statements below.

Equations

• Schoenflies.lastP u t = (u :: t).getLast ⋯

@[simp]

theorem Schoenflies.lastP_nil (u : Plane) : lastP u [] = u

@[simp]

theorem Schoenflies.lastP_cons (u v : Plane) (t : List Plane) : lastP u (v :: t) = lastP v t

theorem Schoenflies.lastP_append (u : Plane) (t : List Plane) (z : Plane) : lastP u (t ++ [z]) = z

theorem Schoenflies.lastP_mem_poly (u : Plane) (t : List Plane) : lastP u t ∈ poly (u :: t)

theorem Schoenflies.poly_snoc (u : Plane) (t : List Plane) (z : Plane) : poly (u :: (t ++ [z])) = poly (u :: t) ∪ segment ℝ (lastP u t) z

Appending one vertex, in the u :: t presentation.

def Schoenflies.IsArcList : List Plane → Prop

A simple polygonal path: consecutive vertices are distinct, and each segment meets the rest of the polygon exactly in the vertex where they are joined. That is precisely the hypothesis Schoenflies.IsArcBetween.concatenate asks for, one step at a time.

Equations

• Schoenflies.IsArcList [] = True
• Schoenflies.IsArcList [head] = True
• Schoenflies.IsArcList (u :: v :: rest) = (u ≠ v ∧ segment ℝ u v ∩ Schoenflies.poly (v :: rest) = {v} ∧ Schoenflies.IsArcList (v :: rest))

@[simp]

theorem Schoenflies.isArcList_nil : IsArcList []

@[simp]

theorem Schoenflies.isArcList_singleton (v : Plane) : IsArcList [v]

theorem Schoenflies.isArcList_cons_cons {u v : Plane} {rest : List Plane} : IsArcList (u :: v :: rest) ↔ u ≠ v ∧ segment ℝ u v ∩ poly (v :: rest) = {v} ∧ IsArcList (v :: rest)

theorem Schoenflies.isArcBetween_poly (u v : Plane) (rest : List Plane) : IsArcList (u :: v :: rest) → IsArcBetween (poly (u :: v :: rest)) u (lastP v rest)

The carrier of a simple polygonal path is an arc between its ends. The induction glues one segment at a time with Schoenflies.IsArcBetween.concatenate; the meeting hypothesis is the second clause of IsArcList.

theorem Schoenflies.IsArcList.truncate (u : Plane) (t : List Plane) : IsArcList (u :: t) → ∀ {w : Plane}, w ∈ poly (u :: t) → ∃ (t' : List Plane), IsArcList (u :: t') ∧ poly (u :: t') ⊆ poly (u :: t) ∧ lastP u t' = w

Truncation. A simple polygonal path may be cut at any point of its carrier: the piece up to that point is again a simple polygonal path, inside the original one.

theorem Schoenflies.IsArcList.snoc (u : Plane) (t : List Plane) : IsArcList (u :: t) → ∀ {z : Plane}, z ≠ lastP u t → segment ℝ (lastP u t) z ∩ poly (u :: t) = {lastP u t} → IsArcList (u :: (t ++ [z]))

Extension. A simple polygonal path may be extended by a segment that meets it only at its own last vertex.

theorem Schoenflies.PolyReaches.exists_arcList {S : Set Plane} {x y : Plane} (h : PolyReaches S x y) : ∃ (t : List Plane), IsArcList (x :: t) ∧ poly (x :: t) ⊆ S ∧ lastP x t = y

Every polygonal path contains a simple one. This is the half of Lemma 1.1 that Schoenflies/PolyPath.lean deferred, and the reason brick B8 can discharge the injectivity clause of Graph.IsDrawing.

The induction is on PolyReaches. At a step the new segment is run backwards from its far end and stopped the first time it touches the polygon already built — exists_first_mem_Icc of Schoenflies/Graph/VertexSquares.lean is exactly that. The old path is truncated there and the stub appended; the stub meets the truncation only at the join, because everything strictly before the stopping parameter misses the old polygon altogether.

The contact point of a core sits on the frame of its square

Graph.IsDrawing.exists_core says the core meets the square about v in exactly one point. That point is on the frame of the square and not in its interior, which is what puts the core in the plane minus the open squares and what makes the radial segment reach the core. The argument is connectedness, not the parametrisation: were the contact point interior, it would be a nonempty proper clopen piece of the core.

theorem Schoenflies.Plane.supDist_eq_of_inter_eq_singleton {K : Set Plane} {c p q : Plane} {r : ℝ} (hK : IsPreconnected K) (hp : K ∩ c.closedSquare r = {p}) (hq : q ∈ K) (hqc : q ∉ c.closedSquare r) : p.supDist c = r

If a connected set meets a closed square in exactly one point and is not contained in that square, the meeting point is on the frame: its sup distance to the centre is exactly the radius.

Bricks B7 and B8, and the redrawing itself

theorem Graph.exists_polygonal_arc_with_radials {U M : Set Schoenflies.Plane} {a b p q : Schoenflies.Plane} (hpath : Schoenflies.PolyReaches U p q) (hUM : U ⊆ M) (hAP : a ≠ p) (hBQ : b ≠ q) (hnear : ∀ z ∈ segment ℝ a p, z ∈ M → z = p) (hfar : ∀ z ∈ segment ℝ b q, z ∈ M → z = q) (hdisjoint : Disjoint (segment ℝ a p) (segment ℝ b q)) : ∃ (g : ℝ → Schoenflies.Plane), ContinuousOn g unitInterval ∧ Set.InjOn g unitInterval ∧ g 0 = a ∧ g 1 = b ∧ Schoenflies.IsPolygonal (g '' unitInterval) ∧ g '' unitInterval ⊆ segment ℝ a p ∪ U ∪ segment ℝ b q

Join a polygonal path to disjoint radial segments meeting its ambient carrier only at their endpoints. The graph redrawing applies this independently to each edge.

theorem Graph.polygonal_redrawing {β : Type u_1} (G : Graph Schoenflies.Plane β) [G.Finite] (drawing : β → ℝ → Schoenflies.Plane) (h : G.IsDrawing drawing) : ∃ (redrawing : β → ℝ → Schoenflies.Plane), G.IsDrawing redrawing ∧ ∀ e ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc redrawing e)

The polygonal redrawing of a finite plane graph (lem:polygonal-redrawing). A finite plane graph is drawn again, on the same abstract graph and the same vertices, with every edge a polygonal arc. The blueprint speaks of an isomorphic plane drawing; since the vertices of a plane graph are plane points and the redrawing leaves them where they are, the isomorphism is the identity and no Graph.IsIsomorphism appears.

The construction, in the order the proof takes it.

• The squares (brick B2). One radius r serves every vertex: the square about a vertex meets no other vertex, meets no arc of an edge it is not incident with, and distinct squares are disjoint.
• The cores (brick B4). Each edge's arc, cut back to what lies between its last exit from the square at one end and its first entry into the square at the other. A core carries no vertex, so distinct cores are disjoint; and — Plane.supDist_eq_of_inter_eq_singleton — its two contact points sit on the frames of the two squares, so the core lies in the plane M minus the open squares.
• The tubes (brick B7). One ε makes the ε-tubes about the cores pairwise disjoint, by compact separation and the single-bound lemma. U e is the connected component, inside M ∩ tube e, of the core; it is relatively open in M, so the strengthened brick B5 joins the two contact points by a polygonal path inside U e.
• The assembly (brick B8). The path is straightened to a simple one (Schoenflies.PolyReaches.exists_arcList), then a radial segment is prepended at each end. A radial meets M only at its far end and two radials meet only at their common centre, so the three pieces glue to an arc; Schoenflies.isArcBetween_poly produces the parametrisation that IsDrawing.edge_param demands.