The outer face

Exactly one face of a finite plane graph is unbounded.

The plane fact this needs is not "the exterior of a large disk is connected" but the exterior of a square, and that one is elementary — Plane.isConnected_beyondSquare, four convex half-planes with consecutive ones sharing a corner. The disk version is what would have needed a traversal of the circle, which a trigonometry-free development withholds.

No face is produced as data: a face is named by a point of it, as Graph.face always has been, so "the outer face" is "the face through any point far enough out".

Blueprint

• exists_unbounded_face — some face is unbounded.
• unbounded_face_unique — any two unbounded faces coincide.
• beyondSquare_subset_face — an unbounded face swallows the whole outside of any square containing the drawing. This is the working form: it is how one proves a given point lies in the outer face.

theorem Graph.isBounded_closedSquare (r : ℝ) : Bornology.IsBounded (Schoenflies.Plane.closedSquare 0 r)

A closed axis-parallel square is bounded: it sits inside a Euclidean ball of radius √2 · r, by the norm comparison.

theorem Graph.IsDrawing.exists_closedSquare {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} [G.Finite] (h : G.IsDrawing drawing) : ∃ (r : ℝ), 0 ≤ r ∧ G.pointSet drawing ⊆ Schoenflies.Plane.closedSquare 0 r

A square containing the whole drawing.

theorem Graph.beyondSquare_subset_exterior {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {r : ℝ} (hr : G.pointSet drawing ⊆ Schoenflies.Plane.closedSquare 0 r) : Schoenflies.Plane.beyondSquare r ⊆ G.exterior drawing

Outside a square containing the drawing, every point is in the exterior.

theorem Graph.beyondSquare_subset_face {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {r : ℝ} (hr : G.pointSet drawing ⊆ Schoenflies.Plane.closedSquare 0 r) {base : Schoenflies.Plane} (hbase : base ∈ Schoenflies.Plane.beyondSquare r) : Schoenflies.Plane.beyondSquare r ⊆ G.face drawing base

The outside of a containing square lies wholly inside one face — the face through any of its points. This is the working form of "there is an outer face".

theorem Graph.not_isBounded_beyondSquare (r : ℝ) : ¬Bornology.IsBounded (Schoenflies.Plane.beyondSquare r)

The outside of a square is unbounded: it contains points of every size.

theorem Graph.exists_unbounded_face {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} [G.Finite] (h : G.IsDrawing drawing) : ∃ base ∈ G.exterior drawing, ¬Bornology.IsBounded (G.face drawing base)

Some face is unbounded.

theorem Graph.unbounded_face_unique {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} [G.Finite] (h : G.IsDrawing drawing) {b c : Schoenflies.Plane} (hbu : ¬Bornology.IsBounded (G.face drawing b)) (hcu : ¬Bornology.IsBounded (G.face drawing c)) : G.face drawing b = G.face drawing c

Any two unbounded faces coincide: an unbounded face escapes every containing square, so it swallows the whole outside and is named by any point of it.