Face cycles: the base cycle, and the faces of a plane graph that grows by ears

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 — is proved by growing the graph from a cycle by ears (Graph.IsTwoConnected.ear_decomposition) and applying thm:polygonal-crosscut at each step. This file supplies everything in that proof that is not the crosscut application itself. The lemma is not proved here; see "What is missing" below, which says exactly what is in the way.

The base cycle

The blueprint's first paragraph, in full. "First choose a cycle of length at least three. Such a cycle exists: under our convention the graph has at least three vertices, and every vertex has at least two distinct neighbors. Indeed, if a vertex v had only one distinct neighbor w, then deleting w would isolate v from some third vertex, contrary to 2-connectivity. Now take a maximal simple path. An endpoint has a neighbor on the path other than its predecessor, and the resulting closed subpath is a cycle of length at least three."

Graph.IsTwoConnected.exists_adj_ne is the two-neighbours sentence; "take a maximal simple path" is Graph.exists_longest_path, already in Schoenflies/Graph/Tree.lean and not rebuilt here; and Graph.IsTwoConnected.exists_long_cycle is the conclusion, packaged as Graph.IsLongCycle, a cycle together with a named third vertex. Naming the third vertex rather than counting is what both consumers want: the counting clause of Graph.IsTwoConnected, and — later — the non-degeneracy of the polygon the cycle draws.

Graph.cycleGraph is that cycle as a subgraph, and Graph.IsLongCycle.isTwoConnected is "the cycle C is 2-connected, so Lemma lem:relative-ear builds the graph from C". This is the one place "length at least three" is used: a two-vertex cycle is a Graph.banana, and Graph.not_isTwoConnected_banana says it is not 2-connected.

One step of the induction

Adding an ear removes the ear's own point set from the exterior and changes nothing else: Graph.pointSet_union, Graph.exterior_union and Graph.face_union_eq_of_disjoint are "all other faces are unchanged".

Graph.IsDrawing.exists_face_of_ear is "its interior is connected and disjoint from the current graph, so it lies in one current face F": the ear's realisation without its two ends is the interior of an arc, hence connected (Schoenflies.IsArcBetween.isConnected_diff), and it misses the drawing of the current subgraph altogether (Graph.IsDrawing.edgesCover_inter_pointSet). Graph.IsDrawing.ends_mem_frontier_face is the next sentence, "the ear's two endpoints are limits of its interior, which lies in F, so they lie on ∂F" — which is what makes the ear a crosscut of that face.

Graph.IsDrawing.mono — a subgraph of a plane graph is a plane graph, with the same drawing — is what lets the induction talk about the faces of the current subgraph at all.

An interface repair

Graph.IsTwoConnected.ear_decomposition hands its step the ear's path but not the clause ∀ g ∈ D, g ∉ E(B), which Graph.IsTwoConnected.relative_ear_exists proves and which Graph.IsTwoConnected.relative_grows_by_ear drops on the way. A geometric consumer needs it: without it the ear may be drawn right on top of the current subgraph, and Graph.IsDrawing.edgesCover_inter_pointSet is false. Graph.ear_edges_notMem_or_union_eq recovers it in the only form available from the outside — either every edge of the ear is new, or the ear is a single edge the subgraph already had and the enlarged graph is the old graph, so the step has nothing to prove. The better fix is for the integrator to add the clause to relative_grows_by_ear and to ear_decomposition; that would make this lemma unnecessary.

What is missing

The crosscut application, and therefore lem:face-cycles itself. thm:polygonal-crosscut is available as Schoenflies.IsPolygonalCrosscut and Schoenflies.polygonal_crosscut, whose hypotheses are stated for Schoenflies.ClosedPolygons: an explicit cyclic vertex list with vertex_inj, edges_meet and corner (no two consecutive edges collinear). The realisation of a graph cycle arrives here as a set — Graph.edgesCover drawing (e :: D) — which Graph.IsDrawing.cycle_isJordanCurve knows to be a Jordan curve and Graph.polygonal_redrawing knows to be polygonal. Turning such a set into a ClosedPolygon (enumerate its vertices cyclically, delete the redundant collinear ones, and derive vertex_inj and edges_meet from simplicity) is a construction main does not have, and the same construction is needed again for the two curves Aᵢ ∪ P that the crosscut produces. Nothing below pretends to it, and no statement below is weaker than its blueprint counterpart.

Namespace

Root Graph, as fixed by Schoenflies/Graph/Walk.lean. The two arc lemmas are stated in Schoenflies, where the rest of the arc theory lives.

Blueprint

• Graph.IsTwoConnected.exists_adj_ne — "every vertex has at least two distinct neighbors".
• Graph.IsLongCycle, Graph.IsTwoConnected.exists_long_cycle — "the resulting closed subpath is a cycle of length at least three".
• Graph.cycleGraph, Graph.IsLongCycle.isTwoConnected — "the cycle C is 2-connected, so Lemma lem:relative-ear builds the graph from C".
• Graph.ear_edges_notMem_or_union_eq — the ear's edges are new, or the ear is not an ear.
• Graph.pointSet_union, Graph.exterior_union, Graph.face_union_subset, Graph.face_union_eq_of_disjoint — "all other faces are unchanged".
• Graph.IsDrawing.mono — the current subgraph is itself a plane graph.
• Schoenflies.IsArcBetween.isConnected_diff, Schoenflies.IsArcBetween.left_mem_closure_diff, …right_mem_closure_diff, Graph.IsDrawing.edgesCover_inter_pointSet, Graph.IsDrawing.exists_face_of_ear, Graph.IsDrawing.ends_mem_frontier_face — "its interior is connected and disjoint from the current graph, so it lies in one current face F … the ear's two endpoints are limits of its interior, which lies in F, so they lie on ∂F; the ear is therefore a crosscut of that side".

Two distinct neighbours

theorem Graph.IsTwoConnected.exists_adj_ne {α : Type u_1} {β : Type u_2} {G : Graph α β} {v : α} (h : G.IsTwoConnected) (hnl : ∀ ⦃g : β⦄ ⦃x : α⦄, ¬G.IsLoopAt g x) (hv : v ∈ G.vertexSet) (w : α) : ∃ (x : α), G.Adj v x ∧ x ≠ w

A vertex of a loopless 2-connected graph has a neighbour other than any prescribed vertex — in particular it has two distinct neighbours, and neither is itself.

The base cycle

"Take a maximal simple path" is Graph.exists_longest_path, already in Schoenflies/Graph/Tree.lean — it is what the three-leaf lemma runs on — so nothing here rebuilds it.

theorem Graph.IsPath.eq_nil_of_eq {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} {W : List β} (h : G.IsPath u W u) : W = []

A path from a vertex back to itself is empty. The first step would depart from the vertex the rest of the path arrives at, which the freshness clause forbids.

structure Graph.IsLongCycle {α : Type u_1} {β : Type u_2} (G : Graph α β) (e : β) (u v : α) (D : List β) (w : α) : Prop

A cycle with at least three vertices — the blueprint's "cycle of length at least three". The third vertex is named rather than counted, because that is what both consumers want.

• isCycle : G.IsCycleThrough e u v D

  The edge and the detour form a cycle.

• mem : w ∈ G.walkVertices u D

  The detour visits a third vertex …

• ne_left : w ≠ u

  … distinct from the source of the edge …

• ne_right : w ≠ v

  … and from its target.

theorem Graph.IsLongCycle.isLink {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v w : α} {e : β} {D : List β} (h : G.IsLongCycle e u v D w) : G.IsLink e u v

theorem Graph.IsLongCycle.isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v w : α} {e : β} {D : List β} (h : G.IsLongCycle e u v D w) : G.IsPath u D v

theorem Graph.IsLongCycle.notMem {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v w : α} {e : β} {D : List β} (h : G.IsLongCycle e u v D w) : e ∉ D

theorem Graph.IsLongCycle.ne {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v w : α} {e : β} {D : List β} (h : G.IsLongCycle e u v D w) : u ≠ v

The two ends of the edge are distinct: otherwise the detour would be a path from a vertex to itself, hence empty, and would visit no third vertex.

theorem Graph.IsTwoConnected.exists_long_cycle {α : Type u_1} {β : Type u_2} {G : Graph α β} [G.Finite] (h : G.IsTwoConnected) (hnl : ∀ ⦃g : β⦄ ⦃x : α⦄, ¬G.IsLoopAt g x) : ∃ (g : β) (u : α) (x : α) (D : List β) (w : α), G.IsLongCycle g u x D w

"The resulting closed subpath is a cycle of length at least three." A finite loopless 2-connected graph has a cycle with three distinct vertices.

Take a maximal path u —W→ v. Its source u has a neighbour x other than the vertex w₀ the path first steps to (Graph.IsTwoConnected.exists_adj_ne), and x lies on the path: otherwise the edge to it could be prepended, contradicting maximality. Cutting the path at x gives a path from u to x whose first step is still to w₀, and the chord closes it into a cycle through u, w₀ and x. The chord is not an edge of that piece: an edge at u in the tail is what the path's freshness clause forbids, and the first edge is not the chord because their far ends differ.

The cycle as a subgraph, and its 2-connectivity

Graph.IsTwoConnected.ear_decomposition starts from a 2-connected subgraph. The subgraph the blueprint starts from is the base cycle, and this section builds it and proves it 2-connected. This is the one place where "length at least three" is used: a two-vertex cycle is a Graph.banana, and Graph.not_isTwoConnected_banana says it is not 2-connected.

theorem Graph.pathGraphOf_mono {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} {D W : List β} (h : W ⊆ D) : G.pathGraphOf u W ≤ G.pathGraphOf u D

A path graph grows with its edge list. General, and not in Schoenflies/Graph/PathGraph.lean; the integrator may want to hoist it.

def Graph.cycleGraph {α : Type u_1} {β : Type u_2} (G : Graph α β) (u : α) (e : β) (D : List β) : Graph α β

The subgraph of G drawn by a cycle: the detour followed by the edge, as a closed walk. Exported as the object rather than hidden behind an existential — the consumer of lem:face-cycles needs the graph itself, to feed it to the ear decomposition.

Equations

• G.cycleGraph u e D = G.pathGraphOf u (D ++ [e])

theorem Graph.pathGraphOf_le_cycleGraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} {e : β} {D : List β} : G.pathGraphOf u D ≤ G.cycleGraph u e D

The detour spans a path subgraph of the cycle.

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

Going round: the detour and then the edge is a closed walk at the source.

theorem Graph.IsCycleThrough.walkVertices_round {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {D : List β} (hc : G.IsCycleThrough e u v D) : G.walkVertices u (D ++ [e]) = G.walkVertices u D

Closing the cycle adds no vertex: both ends of the edge are already on the detour.

theorem Graph.IsCycleThrough.cycleGraph_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {D : List β} (hc : G.IsCycleThrough e u v D) : (G.cycleGraph u e D).vertexSet = G.walkVertices u D

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

theorem Graph.IsCycleThrough.cycleGraph_edgeSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {D : List β} (hc : G.IsCycleThrough e u v D) : (G.cycleGraph u e D).edgeSet = {f : β | f ∈ D ++ [e]}

theorem Graph.IsCycleThrough.left_mem_cycleGraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {D : List β} (hc : G.IsCycleThrough e u v D) : u ∈ (G.cycleGraph u e D).vertexSet

theorem Graph.IsCycleThrough.right_mem_cycleGraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {e : β} {D : List β} (hc : G.IsCycleThrough e u v D) : v ∈ (G.cycleGraph u e D).vertexSet

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

The edge of the cycle really is an edge of the cycle graph, joining the same two ends.

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

The cycle graph is connected: every vertex it has is visited by the detour, and the detour's own prefix runs there from the source.

theorem Graph.IsLongCycle.mem_cycleGraph {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v w : α} {e : β} {D : List β} (h : G.IsLongCycle e u v D w) : w ∈ (G.cycleGraph u e D).vertexSet

theorem Graph.IsLongCycle.isTwoConnected {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v w : α} {e : β} {D : List β} (h : G.IsLongCycle e u v D w) : (G.cycleGraph u e D).IsTwoConnected

A cycle with three vertices is 2-connected, which is what Graph.IsTwoConnected.ear_decomposition asks of its starting subgraph.

Delete a vertex c. One of the two ends of the cycle's edge survives, and it is the hub: every remaining vertex reaches an end of the detour inside the detour (Graph.IsPathGraph.reaches_an_end), an end which — having been reached after the deletion — survived it too, so the cycle's edge is still there to carry it the rest of the way.

An ear that is not new

Graph.IsTwoConnected.ear_decomposition hands its step the ear's path but not the clause ∀ g ∈ D, g ∉ E(B) that Graph.IsTwoConnected.relative_ear_exists proves and that Graph.IsTwoConnected.relative_grows_by_ear drops. A geometric consumer needs it: the ear's drawing has to miss the drawing of the current subgraph, and an edge shared with B would sit right on it.

It is recoverable, and this section recovers it. An edge of the ear that B already has must join the ear's two ends; the ear is then that single edge, and the enlarged graph is the old one, so the step has nothing to prove. The integrator may prefer to add the clause to relative_grows_by_ear and to ear_decomposition instead — that is the better fix, and it makes this section unnecessary.

theorem Graph.IsPath.eq_cons_of_inc_left {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {g : β} {D : List β} (h : G.IsPath u D v) (hg : g ∈ D) (hinc : G.Inc g u) : ∃ (w : α) (T : List β), D = g :: T ∧ G.IsLink g u w ∧ G.IsPath w T v

An edge of a path incident to its source is the path's first edge, in the form that decomposes the path — Graph.IsPath.eq_head_of_inc_source says the same about a list already known to be a cons, and is what does the work here.

theorem Graph.IsPath.eq_singleton_of_edge_mem {α : Type u_1} {β : Type u_2} {G B : Graph α β} {u v : α} {g : β} {D : List β} (hBG : B ≤ G) (hpath : G.IsPath u D v) (huv : u ≠ v) (hint : ∀ y ∈ G.walkVertices u D, y ≠ u → y ≠ v → y ∉ B.vertexSet) (hg : g ∈ D) (hgB : g ∈ B.edgeSet) : D = [g] ∧ G.IsLink g u v

An edge of an ear that the subgraph already has is the whole ear. Both ends of such an edge lie in the subgraph, so the ear's freshness clause makes them the ear's own two ends; the edge is then the ear's first edge and its far end is the ear's target, so nothing follows it.

theorem Graph.ear_edges_notMem_or_union_eq {α : Type u_1} {β : Type u_2} {G B : Graph α β} {u v : α} {D : List β} (hBG : B ≤ G) (hpath : G.IsPath u D v) (huv : u ≠ v) (hu : u ∈ B.vertexSet) (hv : v ∈ B.vertexSet) (hint : ∀ y ∈ G.walkVertices u D, y ≠ u → y ≠ v → y ∉ B.vertexSet) : (∀ g ∈ D, g ∉ B.edgeSet) ∨ B.union (G.pathGraphOf u D) = B

Either every edge of the ear is new, or the ear changes nothing. The disjunction the step of Graph.IsTwoConnected.ear_decomposition has to open before it can do any geometry.

The faces of a graph that grows

Adding an ear removes the ear's own point set from the exterior and changes nothing else. That is the whole of "all other faces are unchanged", and the half of "its interior is connected and disjoint from the current graph, so it lies in one current face F" that is pure topology.

@[simp]

theorem Graph.pointSet_union {β : Type u_3} (B P : Graph Schoenflies.Plane β) (drawing : β → ℝ → Schoenflies.Plane) : (B.union P).pointSet drawing = B.pointSet drawing ∪ P.pointSet drawing

What a union of two plane graphs occupies is what the two of them occupy.

theorem Graph.exterior_union {β : Type u_3} (B P : Graph Schoenflies.Plane β) (drawing : β → ℝ → Schoenflies.Plane) : (B.union P).exterior drawing = B.exterior drawing \ P.pointSet drawing

Adding a graph removes exactly its own point set from the exterior.

theorem Graph.face_union_subset {β : Type u_3} {B P : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {z : Schoenflies.Plane} : (B.union P).face drawing z ⊆ B.face drawing z

A face of the enlarged graph lies inside a face of the old one.

theorem Graph.face_union_eq_of_disjoint {β : Type u_3} {B P : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {z : Schoenflies.Plane} (hz : z ∈ B.exterior drawing) (hdis : Disjoint (B.face drawing z) (P.pointSet drawing)) : (B.union P).face drawing z = B.face drawing z

"All other faces are unchanged." A face the ear does not touch survives the ear.

theorem Graph.exists_face_of_isPreconnected {β : Type u_3} {B : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {S : Set Schoenflies.Plane} (hS : IsPreconnected S) (hSne : S.Nonempty) (hsub : S ⊆ B.exterior drawing) : ∃ z ∈ B.exterior drawing, S ⊆ B.face drawing z

"Its interior is connected and disjoint from the current graph, so it lies in one current face." The topological half: a nonempty preconnected subset of the exterior lies in one face.

The ear lies in one face

The blueprint's "its interior is connected and disjoint from the current graph, so it lies in one current face F", in full.

theorem Graph.IsDrawing.edgesCover_inter_pointSet {β : Type u_3} {G B : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {a b : Schoenflies.Plane} {D : List β} (hG : G.IsDrawing drawing) (hBG : B ≤ G) (hpath : G.IsPath a D b) (hint : ∀ y ∈ G.walkVertices a D, y ≠ a → y ≠ b → y ∉ B.vertexSet) (hnew : ∀ g ∈ D, g ∉ B.edgeSet) : edgesCover drawing D ∩ B.pointSet drawing ⊆ {a, b}

The ear's realisation meets the drawing of the current subgraph only in the ear's two ends. Two cases, and both come down to the ear's freshness clause: a point of the ear on a vertex of B is an end of the edge of the ear it lies on (Graph.IsDrawing.vertex_mem_edgeArc), and a point of the ear on an edge of B is a vertex incident with both (Graph.IsDrawing.edge_inter) — the two edges being distinct because no edge of the ear belongs to B. Either way the point is a vertex of B that the ear visits, which the freshness clause makes one of the ear's two ends.

theorem Graph.IsDrawing.exists_face_of_ear {β : Type u_3} {G B : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {a b : Schoenflies.Plane} {D : List β} (hG : G.IsDrawing drawing) (hBG : B ≤ G) (hpath : G.IsPath a D b) (hab : a ≠ b) (hint : ∀ y ∈ G.walkVertices a D, y ≠ a → y ≠ b → y ∉ B.vertexSet) (hnew : ∀ g ∈ D, g ∉ B.edgeSet) : ∃ z ∈ B.exterior drawing, edgesCover drawing D \ {a, b} ⊆ B.face drawing z

"Its interior is connected and disjoint from the current graph, so it lies in one current face F." The ear's realisation without its two ends is an arc's interior, hence connected, and it misses the drawing of B altogether, so it lies in a single face.

A subgraph of a plane graph is a plane graph

The induction speaks of the faces of the current subgraph, so every step needs the current subgraph to be a plane graph in its own right. Nothing has to be redrawn: the same drawing serves. General, and not in Schoenflies/Graph/Drawing.lean; the integrator may want to hoist it.

theorem Graph.IsDrawing.mono {β : Type u_3} {G B : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} (hG : G.IsDrawing drawing) (hBG : B ≤ G) : B.IsDrawing drawing

A subgraph of a plane graph is a plane graph, with the same drawing.

The ear's ends lie on the boundary of the face its interior lies in

theorem Graph.IsDrawing.ends_mem_frontier_face {β : Type u_3} {G B : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {z a b : Schoenflies.Plane} {D : List β} (hG : G.IsDrawing drawing) (hopen : IsOpen (B.face drawing z)) (hpath : G.IsPath a D b) (hab : a ≠ b) (ha : a ∈ B.vertexSet) (hb : b ∈ B.vertexSet) (hsub : edgesCover drawing D \ {a, b} ⊆ B.face drawing z) : a ∈ frontier (B.face drawing z) ∧ b ∈ frontier (B.face drawing z)

"The ear's two endpoints are limits of its interior, which lies in F, so they lie on ∂F." This is the hypothesis thm:polygonal-crosscut needs of a crosscut: its two ends are on the boundary curve of the region it cuts.