Face cycles: the proof

lem:face-cycles — every face of a finite 2-connected polygonal plane graph has a cycle as its boundary and is one of the two complementary regions of that cycle. Schoenflies/FaceCycles.lean built the base cycle, its 2-connectivity, and the topology of adding an ear; this module runs the induction of the blueprint's proof on top of them.

READ THIS FIRST: what is assumed

Graph.face_cycles carries a hypothesis, Schoenflies.CrosscutSplitsRegion, which nothing proves. It is the exhaustion clause of thm:polygonal-crosscut — "the crosscut replaces F by exactly two regions" — stated for a crosscut whose two endpoints are arbitrary points of the curve. Everything else in the blueprint's proof is discharged here without hypotheses, and each of those pieces is a standalone theorem below.

main's Theorem 2.8 does not discharge it, and the obstruction is not a missing bridge. Schoenflies.IsPolygonalCrosscut states its two splitting hypotheses against ClosedPolygon.arcPieces C a k, which cuts the polygon's edge list at two of its vertices; and Schoenflies.ClosedPolygon.isCornerAt_vertex says every vertex of every realization of a curve is a corner of it. In the induction below the two cut points are the ear's endpoints — graph vertices at which the two cycle edges may leave along opposite rays, so that the boundary curve runs straight through the cut point. Such a point is a vertex of no ClosedPolygon with that carrier, and Schoenflies.exists_closedPolygon_split (whose IsCornerAt hypotheses are therefore not an artefact) cannot be applied.

There is a second, independent reason, and it bites even when both cut points are corners. IsPolygonalCrosscut.edges₁ asks for SameEdges J₁.pieces (C.arcPieces a k ++ K), a multiset equality of unoriented segments. The list on the right has two pieces ending at the cut point q — the arc's last and the crosscut's first. If those two are collinear, the curve J₁ = A₁ ∪ P runs straight through q, so q is a vertex of no ClosedPolygon with that carrier and no piece of J₁.pieces ends there: the multiset equality is unsatisfiable. Since the crosscut may perfectly well leave a cut vertex along the ray opposite the arriving arc edge, edges₁ and edges₂ are not dischargeable as stated. Deleting the redundant vertex — Schoenflies.PrePolygon.deleteLast — repairs the realization and breaks SameEdges in the same move.

Closing the gap therefore means restating Theorem 2.8 with the edge lists related by parity rather than by SameEdges, for a split made at arbitrary points of the curve. The tools exist: Schoenflies.parity_split is already stated for arbitrary lists, and Schoenflies.parity_subdivide (Lemma 2.1) absorbs the difference between a merged piece and its two halves. What is missing is the parity theory of presentations carrying redundant vertices — Schoenflies.parity_eq_one_iff for Schoenflies.PrePolygon rather than only for ClosedPolygon, obtained by carrying the parity along the normalization induction of Schoenflies.PrePolygon.exists_closedPolygon_of_prePolygon. That is a separate module.

Main results

• The realisation of a cycle is a separating curve (Graph.IsDrawing.cycle_isSeparating), which is what the base case needed and what main could not say. It composes Graph.IsDrawing.cycle_isJordanCurve with Schoenflies.exists_closedPolygon and Schoenflies.ClosedPolygon.isSeparating_carrier. The polygonality half needed a bridge that main did not have: Schoenflies.IsPolygonal is the carrier of one vertex list, so a union of edge arcs is polygonal only once each arc is known to be a polyline running from one of its ends to the other (Schoenflies.IsArcBetween.exists_poly_eq, which rests on the arc uniqueness Schoenflies.IsArcBetween.eq_of_subset).
• The base case (Graph.IsDrawing.hasFaceCycles_cycleGraph): the cycle subgraph occupies exactly the cycle's realisation, so its faces are the two regions of that curve.
• Cutting a cycle at two of its vertices (Graph.IsCycleThrough.split_at) and splicing an ear onto an arc (Graph.exists_spliced_cycle) — the combinatorics of "both bounded by cycles" — together with the geometric reading of the split (Graph.IsDrawing.arcs_of_split).
• The step's topology: the enlarged exterior is the old one minus the ear (Graph.IsDrawing.pointSet_pathGraphOf), a face the ear misses survives with its cycle (Graph.IsFaceCycle.mono), and the face the ear cuts is cut only inside itself (Schoenflies.connectedComponentIn_diff).

For the integrator

Graph.IsPath.append, Graph.IsPath.split_meet, Graph.IsWalk.walkVertices_eq_covered, Graph.IsWalk.walkVertices_reverse_eq, Graph.coveredVertices_congr_of_le, Graph.walkVertices_congr_of_le and Graph.edgesCover_append / …_perm / …_reverse are general and belong in Schoenflies/Graph/Walk.lean and Schoenflies/Graph/CycleJordan.lean. Schoenflies.IsArcBetween.eq_of_subset belongs in Schoenflies/Subarc.lean and Schoenflies.poly_append_join in Schoenflies/PolyPath.lean.

Blueprint

• Schoenflies.IsArcBetween.eq_of_subset, Schoenflies.IsArcBetween.exists_poly_eq, Graph.IsDrawing.exists_poly_eq_edgesCover, Graph.IsDrawing.isPolygonal_edgesCover — §1, the polygonality of what a walk draws.
• Graph.IsDrawing.cycle_isSeparating — thm:polygonal-jordan for the realisation of a cycle: "This is true for the initial cycle by Theorem thm:polygonal-jordan."
• Graph.IsFaceCycle, Graph.HasFaceCycles — the conclusion of lem:face-cycles, at one face and at all of them.
• Graph.IsDrawing.hasFaceCycles_cycleGraph — the base case.
• Graph.IsCycleThrough.split_at, Graph.IsDrawing.arcs_of_split, Graph.exists_spliced_cycle — "Theorem thm:polygonal-crosscut replaces F by exactly two regions, both bounded by cycles", combinatorially.
• Schoenflies.CrosscutSplitsRegion — the assumed exhaustion clause of thm:polygonal-crosscut at arbitrary cut points.
• Graph.IsDrawing.hasFaceCycles_union — one ear.
• Graph.face_cycles — lem:face-cycles, modulo Schoenflies.CrosscutSplitsRegion.

An arc inside an arc with the same ends is the whole of it

theorem Schoenflies.IsArcBetween.eq_of_subset {A B : Set Plane} {p q : Plane} (hA : IsArcBetween A p q) (hB : IsArcBetween B p q) (hBA : B ⊆ A) : B = A

An arc between two points contained in an arc between the same two points is all of it. Removing an interior point of the ambient arc splits it into two relatively open halves; a connected subset containing both ends would have to meet both and therefore their empty intersection.

Concatenating polylines

theorem Schoenflies.poly_append_join {as : List Plane} (h₁ : as ≠ []) {bs : List Plane} (h₂ : bs ≠ []) : poly (as ++ bs) = poly as ∪ segment ℝ (as.getLast h₁) (bs.head h₂) ∪ poly bs

Appending two vertex lists joins their carriers by one segment. The segment runs from the last vertex of the first list to the first vertex of the second, and is degenerate — hence contributes nothing — exactly when the two lists already share that vertex.

theorem Schoenflies.poly_append_of_eq {as bs : List Plane} (h₁ : as ≠ []) (h₂ : bs ≠ []) (h : as.getLast h₁ = bs.head h₂) : poly (as ++ bs) = poly as ∪ poly bs

Two polylines meeting end to head concatenate. The joining segment collapses to the shared vertex.

A component survives the removal of a set

The face of the enlarged graph through a point of an old face is a component of that old face with the ear removed — not merely of the whole old exterior with the ear removed. No topology is needed: a component of the small set is preconnected inside the big one, and back again.

theorem Schoenflies.connectedComponentIn_diff (S P : Set Plane) (z : Plane) : connectedComponentIn (S \ P) z = connectedComponentIn (connectedComponentIn S z \ P) z

Cutting inside one component. The component of z in S ∖ P sees only the component of z in S.

A polygonal arc is a polyline running from one end to the other

theorem Schoenflies.IsArcBetween.exists_poly_eq {A : Set Plane} {p q : Plane} (harc : IsArcBetween A p q) (hpoly : IsPolygonal A) (hpq : p ≠ q) : ∃ (vs : List Plane) (h : vs ≠ []), vs.head h = p ∧ vs.getLast h = q ∧ poly vs = A

A polygonal arc is poly of a vertex list running from one of its ends to the other. Schoenflies.exists_simple_poly_of_isPolygonal produces a simple polygonal arc inside the set between the two points; being an arc between the same two ends it is the whole of it, by Schoenflies.IsArcBetween.eq_of_subset.

Cutting and joining paths

Two general facts about paths that Schoenflies/Graph/Walk.lean does not have, and that the splitting of a cycle at two of its vertices runs on. The integrator should hoist both into Schoenflies/Graph/Walk.lean, next to Graph.IsPath.split, which is the weaker form of the second.

theorem Graph.IsPath.append {α : Type u_1} {β : Type u_2} {G : Graph α β} {u w v : α} {W₁ W₂ : List β} : G.IsPath u W₁ w → G.IsPath w W₂ v → (∀ y ∈ G.walkVertices u W₁, y ∈ G.walkVertices w W₂ → y = w) → G.IsPath u (W₁ ++ W₂) v

Two paths meeting only at the junction concatenate. The freshness clause of the joined path is the freshness of the first together with the meeting condition: a vertex the second half visits and the first half departs from would be the junction, which the first half has already arrived at.

theorem Graph.IsPath.split_meet {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v x : α} {W : List β} (h : G.IsPath u W v) (hx : x ∈ G.walkVertices u W) : ∃ (W₁ : List β) (W₂ : List β), W = W₁ ++ W₂ ∧ G.IsPath u W₁ x ∧ G.IsPath x W₂ v ∧ ∀ y ∈ G.walkVertices u W₁, y ∈ G.walkVertices x W₂ → y = x

A path splits at any vertex it visits, and the two halves meet only there. This is Graph.IsPath.split with the meeting condition in place of its weaker last clause.

theorem Graph.IsWalk.walkVertices_eq_covered {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} (h : G.IsWalk u W v) (hne : W ≠ []) : G.walkVertices u W = G.coveredVertices W

The source of a nonempty walk is an end of its first edge, so a nonempty walk visits no vertex its edges do not cover.

theorem Graph.IsWalk.walkVertices_reverse_eq {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} (h : G.IsWalk u W v) (hne : W ≠ []) : G.walkVertices v W.reverse = G.walkVertices u W

Running a nonempty walk backwards changes neither the edges nor the vertices it visits.

Cutting a cycle at two of its vertices

The cycle is X ++ Y ++ Z closed up by the edge e, cut at the two vertices c (between X and Y) and d (between Y and Z). One arc is Y; the other runs Z, then the closing edge, then X. Both cases of "which of the two named vertices comes first along the detour" feed this one lemma.

theorem Graph.IsCycleThrough.split_aux {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} {u v c d : α} {D X Y Z : List β} (hc : G.IsCycleThrough e u v D) (hD : D = X ++ (Y ++ Z)) (hX : G.IsPath u X c) (hY : G.IsPath c Y d) (hZ : G.IsPath d Z v) (hcd : c ≠ d) (hM1 : ∀ y ∈ G.walkVertices u X, y ∈ G.walkVertices c (Y ++ Z) → y = c) (hM2 : ∀ y ∈ G.walkVertices c Y, y ∈ G.walkVertices d Z → y = d) : G.IsPath d (Z ++ e :: X) c ∧ (Y ++ (Z ++ e :: X)).Perm (e :: D) ∧ ∀ y ∈ G.walkVertices c Y, y ∈ G.walkVertices d (Z ++ e :: X) → y = c ∨ y = d

The complementary arc of a cut cycle, together with the two facts a geometric consumer needs: that the two arcs between them use every edge of the cycle exactly once, and that they visit no common vertex but the two cut points.

theorem Graph.IsCycleThrough.split_at {α : Type u_1} {β : Type u_2} {G : Graph α β} {e : β} {u v a b : α} {D : List β} (hc : G.IsCycleThrough e u v D) (ha : a ∈ G.walkVertices u D) (hb : b ∈ G.walkVertices u D) (hab : a ≠ b) : ∃ (D₁ : List β) (D₂ : List β), G.IsPath a D₁ b ∧ G.IsPath b D₂ a ∧ (D₁ ++ D₂).Perm (e :: D) ∧ ∀ y ∈ G.walkVertices a D₁, y ∈ G.walkVertices b D₂ → y = a ∨ y = b

A cycle cut at two of its vertices is two paths between them. The two arcs use every edge of the cycle exactly once — that is what the permutation says — and they have no vertex in common but the two cut points. This is the combinatorial half of "the ear is a crosscut of the face": the geometric half reads the two arcs of the Jordan curve off it.

Splicing an ear onto an arc

The blueprint's "the crosscut replaces F by exactly two regions, both bounded by cycles": the two new cycles are the two arcs of the old one, each closed up by the ear. This is the combinatorial construction of one of them.

theorem Graph.coveredVertices_congr_of_le {α : Type u_1} {β : Type u_2} {W : List β} {H G : Graph α β} (hHG : H ≤ G) (hW : ∀ f ∈ W, f ∈ H.edgeSet) : G.coveredVertices W = H.coveredVertices W

Incidence along edges of a subgraph is the same in the subgraph as in the graph, so the vertices a walk visits do not depend on which of the two it is read in.

theorem Graph.walkVertices_congr_of_le {α : Type u_1} {β : Type u_2} {u : α} {W : List β} {H G : Graph α β} (hHG : H ≤ G) (hW : ∀ f ∈ W, f ∈ H.edgeSet) : G.walkVertices u W = H.walkVertices u W

theorem Graph.exists_spliced_cycle {α : Type u_1} {β : Type u_2} {B G : Graph α β} (hBG : B ≤ G) {a b : α} {D₁ D' : List β} (hD1 : B.IsPath a D₁ b) (hear : G.IsPath a D' b) (hab : a ≠ b) (hnew : ∀ g ∈ D', g ∉ B.edgeSet) (hint : ∀ y ∈ G.walkVertices a D', y ≠ a → y ≠ b → y ∉ B.vertexSet) : ∃ (f : β) (x : α) (y : α) (T : List β), (B.union (G.pathGraphOf a D')).IsCycleThrough f x y T ∧ (f :: T).Perm (D₁ ++ D')

The cycle an ear splices onto an arc of the old cycle. The closed walk runs along the arc and back along the ear; presented as Graph.IsCycleThrough, its named edge is the ear's first, and its detour is the arc followed by the rest of the ear reversed.

What a walk of a polygonal plane graph draws

theorem Graph.IsDrawing.exists_poly_eq_edgesCover {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {u v : Schoenflies.Plane} {W : List β} (h : G.IsDrawing drawing) (hpoly : ∀ e ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing e)) (hW : G.IsWalk u W v) (hne : W ≠ []) : ∃ (vs : List Schoenflies.Plane) (hv : vs ≠ []), vs.head hv = u ∧ vs.getLast hv = v ∧ Schoenflies.poly vs = edgesCover drawing W

The realisation of a walk with polygonal edges is a polyline from its source to its target. The induction is along the walk: the first edge contributes its own vertex list, and the two lists are joined at the waypoint, which is the last vertex of the first and the first vertex of the rest.

The realisation of a cycle is a separating curve

This is the composition the base case of lem:face-cycles needs, and the one thing that was missing from it: Graph.IsDrawing.cycle_isJordanCurve says the realisation is a Jordan curve and Graph.IsDrawing.isPolygonal_edgesCover says it is polygonal, and Schoenflies.exists_closedPolygon — the realization theorem — turns that pair into a Schoenflies.ClosedPolygon, whose carrier Schoenflies.ClosedPolygon.isSeparating_carrier knows to separate the plane. Nothing here inspects the polygon; it is used and discarded.

theorem Graph.IsCycleThrough.isWalk_cons {β : Type u_1} {α : Type u_2} {G : Graph α β} {e : β} {u v : α} {D : List β} (hc : G.IsCycleThrough e u v D) : G.IsWalk v (e :: D) v

Going round the cycle the other way: the edge, then the detour, is a closed walk at the edge's far end. This is the walk whose edge list is e :: D, the list every statement about the realisation of a cycle is phrased with.

theorem Graph.IsDrawing.cycle_isSeparating {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsDrawing drawing) (hpoly : ∀ e ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing e)) {e : β} {u v : Schoenflies.Plane} {D : List β} (hc : G.IsCycleThrough e u v D) : Schoenflies.IsSeparating (edgesCover drawing (e :: D))

The realisation of a cycle of a polygonal plane graph is a separating Jordan curve. Schoenflies.IsSeparating is Definition 2.4: the complement has exactly two regions, one bounded and one unbounded, each with the curve as its boundary.

What a subgraph spanned by a walk occupies

theorem Graph.IsDrawing.inc_mem_edgeArc {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {e : β} (h : G.IsDrawing drawing) {x : Schoenflies.Plane} (hinc : G.Inc e x) : x ∈ edgeArc drawing e

An end of an edge lies on that edge's arc.

theorem Graph.IsDrawing.pointSet_pathGraphOf {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {u v : Schoenflies.Plane} {W : List β} (h : G.IsDrawing drawing) (hW : G.IsWalk u W v) (hne : W ≠ []) : (G.pathGraphOf u W).pointSet drawing = edgesCover drawing W

The subgraph spanned by a nonempty walk occupies exactly what the walk draws. Its vertices are ends of its edges, so they add nothing to the union of the edge arcs.

theorem Graph.IsDrawing.pointSet_cycleGraph {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsDrawing drawing) {e : β} {u v : Schoenflies.Plane} {D : List β} (hc : G.IsCycleThrough e u v D) : (G.cycleGraph u e D).pointSet drawing = edgesCover drawing (e :: D)

The cycle subgraph occupies exactly what the cycle draws.

The conclusion of lem:face-cycles, at one face

structure Graph.IsFaceCycle {β : Type u_1} (G : Graph Schoenflies.Plane β) (drawing : β → ℝ → Schoenflies.Plane) (z : Schoenflies.Plane) (e : β) (u v : Schoenflies.Plane) (D : List β) : Prop

A face bounded by a named cycle. The face face G drawing z is one of the two regions of the complement of the realisation of the cycle e :: D — which is the blueprint's "every face … has a cycle as its boundary and is one of the two complementary regions of that cycle". The cycle is a parameter rather than an existential so that a consumer that has produced one keeps it.

• isCycle : G.IsCycleThrough e u v D

  The named data really is a cycle of the graph.

• isSeparating : Schoenflies.IsSeparating (edgesCover drawing (e :: D))

  Its realisation separates the plane into exactly two regions.

• isRegionOf : Schoenflies.IsRegionOf (edgesCover drawing (e :: D)) (G.face drawing z)

  The face is one of those two.

theorem Graph.IsFaceCycle.frontier_eq {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {z : Schoenflies.Plane} {e : β} {u v : Schoenflies.Plane} {D : List β} (h : G.IsFaceCycle drawing z e u v D) : frontier (G.face drawing z) = edgesCover drawing (e :: D)

"has a cycle as its boundary": the frontier of the face is the realisation.

theorem Graph.IsFaceCycle.eq_inside_or_outside {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {z : Schoenflies.Plane} {e : β} {u v : Schoenflies.Plane} {D : List β} (h : G.IsFaceCycle drawing z e u v D) : G.face drawing z = Schoenflies.inside (edgesCover drawing (e :: D)) ∨ G.face drawing z = Schoenflies.outside (edgesCover drawing (e :: D))

The face is the interior or the exterior of its boundary cycle.

theorem Graph.IsFaceCycle.eq_inside_of_isBounded {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {z : Schoenflies.Plane} {e : β} {u v : Schoenflies.Plane} {D : List β} (h : G.IsFaceCycle drawing z e u v D) (hbdd : Bornology.IsBounded (G.face drawing z)) : G.face drawing z = Schoenflies.inside (edgesCover drawing (e :: D))

"In particular, every bounded face is the interior of its boundary cycle." The other region of a separating curve is the unbounded one.

theorem Graph.IsFaceCycle.mono {β : Type u_1} {G B : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {z : Schoenflies.Plane} {e : β} {u v : Schoenflies.Plane} {D : List β} (h : B.IsFaceCycle drawing z e u v D) (hBG : B ≤ G) (hface : G.face drawing z = B.face drawing z) : G.IsFaceCycle drawing z e u v D

A face bounded by a cycle of a subgraph is bounded by the same cycle of the whole graph, provided the face itself is unchanged — which is the shape the induction step needs when it carries a face past an ear that does not touch it.

def Graph.HasFaceCycles {β : Type u_1} (G : Graph Schoenflies.Plane β) (drawing : β → ℝ → Schoenflies.Plane) : Prop

lem:face-cycles, as a property of a plane graph: every face has a cycle as its boundary and is one of the two complementary regions of that cycle.

Equations

• G.HasFaceCycles drawing = ∀ z ∈ G.exterior drawing, ∃ (e : β) (u : Schoenflies.Plane) (v : Schoenflies.Plane) (D : List β), G.IsFaceCycle drawing z e u v D

The base case: the faces of a single cycle

"This is true for the initial cycle by Theorem thm:polygonal-jordan." The cycle subgraph occupies exactly the cycle's realisation, so its faces are literally the components of the complement of that curve, and the curve is separating.

theorem Graph.IsDrawing.hasFaceCycles_cycleGraph {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsDrawing drawing) (hpoly : ∀ e ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing e)) {e : β} {u v : Schoenflies.Plane} {D : List β} (hc : G.IsCycleThrough e u v D) : (G.cycleGraph u e D).HasFaceCycles drawing

The base case of lem:face-cycles. Both faces of the graph consisting of one cycle are regions of that cycle.

The two arcs a cycle is cut into, as sets

The combinatorial split of Graph.IsCycleThrough.split_at becomes the geometric one: the two arcs of the Jordan curve between the two cut vertices. The drawing condition is used once, to turn "the two edge lists are disjoint" into "the two arcs meet only at vertices".

theorem Graph.IsDrawing.mem_walkVertices_of_mem_edgesCover {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsDrawing drawing) {e : β} {u v z : Schoenflies.Plane} {D : List β} (hc : G.IsCycleThrough e u v D) (hzV : z ∈ G.vertexSet) (hz : z ∈ edgesCover drawing (e :: D)) : z ∈ G.walkVertices u D

A vertex of the graph lying on the realisation of a cycle is a vertex of that cycle.

theorem Graph.IsDrawing.arcs_of_split {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsDrawing drawing) {a b : Schoenflies.Plane} {D₁ D₂ : List β} (h₁ : G.IsPath a D₁ b) (h₂ : G.IsPath b D₂ a) (hab : a ≠ b) (hdisj : ∀ g ∈ D₁, g ∉ D₂) (hmeet : ∀ y ∈ G.walkVertices a D₁, y ∈ G.walkVertices b D₂ → y = a ∨ y = b) : Schoenflies.IsArcBetween (edgesCover drawing D₁) a b ∧ Schoenflies.IsArcBetween (edgesCover drawing D₂) b a ∧ edgesCover drawing D₁ ∩ edgesCover drawing D₂ = {a, b}

The realisation of a cycle, cut at two of its vertices, is two arcs meeting exactly there. The hypotheses are the output of Graph.IsCycleThrough.split_at, read in the plane.

The obligation this module does not discharge

Read this before using Graph.face_cycles. Everything below the base case is proved modulo one hypothesis, Schoenflies.CrosscutSplitsRegion, and the final theorem carries it as an argument. It is the exhaustion clause of thm:polygonal-crosscut — Theorem 2.8, in the shape Schoenflies.IsPolygonalCrosscut.region_eq and Schoenflies.IsPolygonalCrosscut.cell_isComponent₁ already have it — at a crosscut whose two endpoints are arbitrary points of the curve.

main's Theorem 2.8 cannot be applied here, and the reason is not a missing bridge. Its hypotheses edges₁/edges₂ are stated against ClosedPolygon.arcPieces C a k, which splits the polygon's edge list at two of its vertices; and by Schoenflies.ClosedPolygon.isCornerAt_vertex every vertex of every realization of a curve is a corner of it. In the induction below the two cut points are the ear's endpoints, which are graph vertices at which the two cycle edges may perfectly well leave along opposite rays — the curve then runs straight through the cut point, which is therefore a vertex of no ClosedPolygon with that carrier, and no realization theorem can supply one. Discharging this hypothesis needs Theorem 2.8 restated for an edge-list split made at arbitrary points, which in turn needs the parity theory for polygon presentations carrying redundant vertices (Schoenflies.PrePolygon) rather than only for ClosedPolygon. That is a separate module.

def Schoenflies.CrosscutSplitsRegion : Prop

The exhaustion clause of the polygonal crosscut theorem, at arbitrary cut points. J is a separating polygonal curve cut by the points p, q into the arcs A₁, A₂; P is a polygonal crosscut from p to q meeting J only there and running inside the region Ω. The claim is that every component of Ω ∖ P is a region of A₁ ∪ P or of A₂ ∪ P — the blueprint's "Theorem 2.8 replaces F by exactly two regions, both bounded by cycles".

This is assumed, not proved; see the section docstring for why main's Theorem 2.8 does not apply.

Equations

• One or more equations did not get rendered due to their size.

What a list of edges draws depends only on which edges are on it

theorem Graph.edgesCover_append {β : Type u_1} (drawing : β → ℝ → Schoenflies.Plane) (W₁ W₂ : List β) : edgesCover drawing (W₁ ++ W₂) = edgesCover drawing W₁ ∪ edgesCover drawing W₂

theorem Graph.edgesCover_perm {β : Type u_1} {drawing : β → ℝ → Schoenflies.Plane} {W₁ W₂ : List β} (hp : W₁.Perm W₂) : edgesCover drawing W₁ = edgesCover drawing W₂

theorem Graph.edgesCover_reverse {β : Type u_1} (drawing : β → ℝ → Schoenflies.Plane) (W : List β) : edgesCover drawing W.reverse = edgesCover drawing W

The induction step: one ear

"Suppose it holds for the current graph and add the next geometric ear. Its interior is connected and disjoint from the current graph, so it lies in one current face F … the ear is therefore a crosscut of that side, and Theorem thm:polygonal-crosscut replaces F by exactly two regions, both bounded by cycles; all other faces are unchanged."

Everything here is proved, except that the appeal to Theorem 2.8 is to the hypothesis Schoenflies.CrosscutSplitsRegion instead.

theorem Graph.IsDrawing.hasFaceCycles_union {β : Type u_1} {G B : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {a b : Schoenflies.Plane} [G.Finite] (h : G.IsDrawing drawing) (hobl : Schoenflies.CrosscutSplitsRegion) (hpoly : ∀ g ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing g)) (hBG : B ≤ G) (hmot : B.HasFaceCycles drawing) {D' : List β} (hpath : G.IsPath a D' b) (hab : a ≠ b) (ha : a ∈ B.vertexSet) (hb : b ∈ B.vertexSet) (hint : ∀ y ∈ G.walkVertices a D', y ≠ a → y ≠ b → y ∉ B.vertexSet) (hnew : ∀ g ∈ D', g ∉ B.edgeSet) : (B.union (G.pathGraphOf a D')).HasFaceCycles drawing

One ear. Given lem:face-cycles for the current subgraph, it holds for the subgraph enlarged by an ear — modulo Schoenflies.CrosscutSplitsRegion.

lem:face-cycles

"The cycle C is 2-connected, so Lemma lem:relative-ear builds the graph from C. We prove by induction that every face is exactly one of the two regions bounded by its boundary cycle."

theorem Graph.face_cycles {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} [G.Finite] (hobl : Schoenflies.CrosscutSplitsRegion) (h : G.IsDrawing drawing) (hpoly : ∀ g ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing g)) (hG : G.IsTwoConnected) : G.HasFaceCycles drawing

lem:face-cycles (face cycles). Every face of a finite 2-connected polygonal plane graph has a cycle as its boundary and is one of the two complementary regions of that cycle.

The statement carries the hypothesis Schoenflies.CrosscutSplitsRegion, which is not proved anywhere: it is the exhaustion clause of thm:polygonal-crosscut at a crosscut whose endpoints need not be corners of the curve, and main's Theorem 2.8 cannot supply it — see the docstring of Schoenflies.CrosscutSplitsRegion. Everything else in the blueprint's proof is discharged here: the base cycle and its 2-connectivity (Schoenflies/FaceCycles.lean), that its realisation separates the plane (Graph.IsDrawing.cycle_isSeparating), that the ear lies in one face and is a crosscut of it, that all other faces are unchanged, and that the two new faces are bounded by the two cycles the ear splices onto the two arcs of the old one.