The outer face of a chain of plane graphs

lem:outer-chain. Let Γ 0, …, Γ n (n ≥ 2, so at least three graphs) be finite 2-connected polygonal plane graphs, consecutive ones sharing at least two vertices and nonconsecutive ones disjoint. If a point x is in the outer face of every consecutive pair Γ p ∪ Γ (p+1), then it is in the outer face of Γ 0 ∪ ⋯ ∪ Γ n.

How the chain is formalised

The blueprint says "after subdividing common points into vertices". Here that is true by construction rather than by a theorem: the family shares one ambient edge type β and one drawing drawing : β → ℝ → Plane, and every member is a subgraph of a single plane graph G — see Graph.IsPlaneChain. Two members therefore agree about the ends of a shared edge, meet only where G lets them meet, and Γ p ∪ Γ q is Graph.union with nothing to check. The ambient G is allowed to be larger than the chain's own union; a consumer that has built all its pieces inside one polygonal overlay hands that overlay over as G.

Graph.chainUnion Γ i m is the block Γ i ∪ Γ (i+1) ∪ ⋯ ∪ Γ (i+m), indexed by its length m rather than by its right endpoint, so that the recursion is on m and the blueprint's "choose i ≤ j with j - i minimum" is a plain strong induction on m. A consecutive pair is chainUnion Γ p 1.

"x is in the outer face of H" is spelled, as everywhere in this development, as x is off the drawing and the face through it is unbounded — x ∈ exterior H drawing together with ¬ Bornology.IsBounded (face H drawing x). Graph.unbounded_face_unique is what makes that "the" outer face, and Graph.beyondSquare_subset_face is how a consumer proves it.

What is proved and what is assumed

The blueprint's proof is a minimal-counterexample argument on two measures: first the length of the index interval, then the number of edges of the enclosing cycle lying outside Γ (j-1). Both minimisations are carried out here, as strong inductions, together with

• the reduction of "x lies in a bounded face" to "some cycle encloses x" (Graph.encloses_of_isBounded_face, from Graph.face_cycles') and back (Graph.isBounded_face_of_encloses);
• 2-connectivity of every block, by iterating Graph.IsTwoConnected.union (lem:union-two-connected);
• the base case j - i ≤ 1, which is the blueprint's paragraph "If j-i ≤ 1, choose a consecutive pair H containing that union …";
• the two minimality consequences "C contains an edge of Γ j outside Γ (j-1)" and "C contains an edge of the earlier chain outside Γ (j-1)", each proved by pushing the cycle down into a shorter block with Graph.IsCycleThrough.anti;
• the splicing of a crosscut onto each of the two arcs (Graph.exists_spliced_cycles, from Graph.exists_spliced_cycle) and the edge count that makes the splice a strict improvement (Graph.edgesOutside_splice_lt, Graph.exists_cycle_edgesOutside_lt).

Graph.Descent is the middle paragraph of the blueprint's proof — from a cycle C of Γ i ∪ ⋯ ∪ Γ j enclosing x and having an edge of Γ j and an edge of Γ i ∪ ⋯ ∪ Γ (j-2) outside Γ (j-1), produce a cycle of the same block enclosing x with strictly fewer edges outside Γ (j-1). It is a statement about one step, not about the chain's outer face.

It was assumed when this module was written. Both halves are now proved:

• Schoenflies/CrosscutExists.lean — combinatorial: build the crosscut, as Graph.IsPlaneChain.crosscutExists. Nothing geometric enters beyond Graph.IsPlaneChain.disjoint_block_far, "Γ j meets the earlier chain only through Γ (j-1)".
• Schoenflies/CrosscutEncloses.lean — geometric: "the path R lies on one side of C and is a crosscut there; by thm:polygonal-crosscut, at least one of R ∪ C₁, R ∪ C₂ encloses x", as Graph.crosscutEnclosesOff. That module also carries the counterexample showing why the clause x ∈ exterior H drawing cannot be dropped — see the comment below, where the false version of it used to stand.

Schoenflies/OuterChainClosed.lean combines the two, and states lem:outer-chain with nothing assumed.

Blueprint

• Graph.chainUnion — Γ i ∪ ⋯ ∪ Γ (i+m), with chainUnion_le, le_chainUnion, chainUnion_finite, chainUnion_isTwoConnected (the last is repeated lem:union-two-connected).
• Graph.Encloses — "that face is the interior of its boundary cycle, which therefore encloses x", as a property of a graph.
• Graph.encloses_of_isBounded_face, Graph.isBounded_face_of_encloses — the two directions of that reduction; the second is the blueprint's "the face of H containing x … lies in the bounded set Int(C) and therefore is not the outer face of H".
• Graph.IsPlaneChain — the hypotheses of lem:outer-chain; Graph.OuterOnPairs — its hypothesis on consecutive pairs.
• Graph.IsCycleCrosscut — the crosscut R of the cycle C, with the two arcs it cuts.
• Graph.exists_spliced_cycles — the two cycles R ∪ C₁, R ∪ C₂.
• Graph.edgesOutside, Graph.edgesOutside_splice_lt, Graph.exists_cycle_edgesOutside_lt — "it has fewer edges outside Γ (j-1) than C, since one nonempty outside portion of C has been replaced by R ⊆ Γ (j-1)".
• Graph.Descent — the crosscut paragraph of the proof; discharged in Schoenflies/CrosscutEncloses.lean from Graph.CrosscutExists alone.
• Graph.IsPlaneChain.not_encloses — the double minimisation.
• Graph.IsPlaneChain.outer_chain — lem:outer-chain, from Graph.Descent; Graph.IsPlaneChain.outer_chain' in Schoenflies/OuterChainClosed.lean is the same statement with nothing assumed.

Blocks of a chain

def Graph.chainUnion {α : Type u_1} {β : Type u_2} (Γ : ℕ → Graph α β) (i : ℕ) : ℕ → Graph α β

chainUnion Γ i m is Γ i ∪ Γ (i+1) ∪ ⋯ ∪ Γ (i+m).

Indexed by the length m of the block rather than by its right endpoint: the blueprint minimises j - i, and with this indexing that is a strong induction on the second argument with no subtraction anywhere.

Equations

• Graph.chainUnion Γ i 0 = Γ i
• Graph.chainUnion Γ i m.succ = (Graph.chainUnion Γ i m).union (Γ (i + m + 1))

@[simp]

theorem Graph.chainUnion_zero {α : Type u_1} {β : Type u_2} (Γ : ℕ → Graph α β) (i : ℕ) : chainUnion Γ i 0 = Γ i

@[simp]

theorem Graph.chainUnion_succ {α : Type u_1} {β : Type u_2} (Γ : ℕ → Graph α β) (i m : ℕ) : chainUnion Γ i (m + 1) = (chainUnion Γ i m).union (Γ (i + m + 1))

theorem Graph.chainUnion_one {α : Type u_1} {β : Type u_2} (Γ : ℕ → Graph α β) (i : ℕ) : chainUnion Γ i 1 = (Γ i).union (Γ (i + 1))

A block of length one is a consecutive pair.

theorem Graph.mem_vertexSet_chainUnion {α : Type u_1} {β : Type u_2} {Γ : ℕ → Graph α β} {i m : ℕ} {x : α} : x ∈ (chainUnion Γ i m).vertexSet ↔ ∃ (p : ℕ), i ≤ p ∧ p ≤ i + m ∧ x ∈ (Γ p).vertexSet

theorem Graph.mem_edgeSet_chainUnion {α : Type u_1} {β : Type u_2} {Γ : ℕ → Graph α β} {i m : ℕ} {e : β} : e ∈ (chainUnion Γ i m).edgeSet ↔ ∃ (p : ℕ), i ≤ p ∧ p ≤ i + m ∧ e ∈ (Γ p).edgeSet

theorem Graph.chainUnion_le {α : Type u_1} {β : Type u_2} {Γ : ℕ → Graph α β} {G : Graph α β} {i m : ℕ} (h : ∀ (p : ℕ), i ≤ p → p ≤ i + m → Γ p ≤ G) : chainUnion Γ i m ≤ G

A block sits inside any graph containing all of its members.

theorem Graph.le_chainUnion {α : Type u_1} {β : Type u_2} {Γ : ℕ → Graph α β} {G : Graph α β} {i m p : ℕ} (hle : ∀ (q : ℕ), i ≤ q → q ≤ i + m → Γ q ≤ G) (hp : i ≤ p) (hp' : p ≤ i + m) : Γ p ≤ chainUnion Γ i m

Each member of a block is a subgraph of it. The compatibility hypothesis is what makes the right-hand summand of a Graph.union a subgraph, and it is free once every member lies in one ambient graph.

theorem Graph.chainUnion_finite {α : Type u_1} {β : Type u_2} {Γ : ℕ → Graph α β} {i m : ℕ} (h : ∀ (p : ℕ), i ≤ p → p ≤ i + m → (Γ p).Finite) : (chainUnion Γ i m).Finite

A block of finite graphs is finite.

theorem Graph.chainUnion_isTwoConnected {α : Type u_1} {β : Type u_2} {Γ : ℕ → Graph α β} {G : Graph α β} {i m : ℕ} (hle : ∀ (q : ℕ), i ≤ q → q ≤ i + m → Γ q ≤ G) (htc : ∀ (q : ℕ), i ≤ q → q ≤ i + m → (Γ q).IsTwoConnected) (hmeet : ∀ (q : ℕ), i ≤ q → q < i + m → ∃ (a : α) (b : α), a ≠ b ∧ a ∈ (Γ q).vertexSet ∧ a ∈ (Γ (q + 1)).vertexSet ∧ b ∈ (Γ q).vertexSet ∧ b ∈ (Γ (q + 1)).vertexSet) : (chainUnion Γ i m).IsTwoConnected

lem:union-two-connected, iterated. A block of 2-connected graphs in which consecutive members share two distinct vertices is 2-connected.

Reading a cycle inside a subgraph

Graph.IsCycleThrough.anti is the cycle counterpart of Graph.IsPath.anti; it is what turns "no edge of C is outside this block" into "C is a cycle of this block".

theorem Graph.IsCycleThrough.mem_edgeSet_cons {α : Type u_1} {β : Type u_2} {G : Graph α β} {e g : β} {u v : α} {D : List β} (h : G.IsCycleThrough e u v D) (hg : g ∈ e :: D) : g ∈ G.edgeSet

Every edge on a cycle is an edge of the graph.

theorem Graph.IsCycleThrough.anti {α : Type u_1} {β : Type u_2} {G K : Graph α β} {e : β} {u v : α} {D : List β} (h : G.IsCycleThrough e u v D) (hKG : K ≤ G) (hE : ∀ g ∈ e :: D, g ∈ K.edgeSet) : K.IsCycleThrough e u v D

A cycle all of whose edges belong to a subgraph is a cycle of that subgraph.

theorem Graph.IsCycleThrough.mono {α : Type u_1} {β : Type u_2} {G K : Graph α β} {e : β} {u v : α} {D : List β} (h : K.IsCycleThrough e u v D) (hKG : K ≤ G) : G.IsCycleThrough e u v D

A cycle of a subgraph is a cycle of the graph.

A crosscut of a cycle, with the two arcs it cuts

This is the combinatorial output of the blueprint's crosscut paragraph, bundled: the path R in F = Γ (j-1), its two endpoints a, b on the cycle, and the two arcs D₁, D₂ the endpoints cut the cycle into. Both arcs are required to carry an edge that F does not have — the blueprint's "each arc contains an edge outside Γ (j-1), because its endpoints belong to different maximal subpaths of the intersection" — which is what makes the splice a strict improvement on both sides, so that it does not matter which of the two spliced cycles turns out to enclose x.

structure Graph.IsCycleCrosscut {α : Type u_1} {β : Type u_2} (H F : Graph α β) (e : β) (u v : α) (D : List β) (a b : α) (R D₁ D₂ : List β) : Prop

A crosscut of a cycle. R is a path of H between two vertices a ≠ b of the cycle e :: D, lying in F, using no edge of the cycle and no vertex of it internally; D₁, D₂ are the two arcs the cycle splits into, each carrying an edge outside F.

• ne : a ≠ b

  The two cut points are distinct.

• arc₁ : H.IsPath a D₁ b

  The first arc runs from a to b.

• arc₂ : H.IsPath b D₂ a

  The second arc runs back.

• split : (D₁ ++ D₂).Perm (e :: D)

  Together the arcs use every edge of the cycle exactly once.

• isPath : H.IsPath a R b

  The crosscut is a path between the two cut points.

• mem_left : a ∈ H.walkVertices u D

  The first cut point is on the cycle.

• mem_right : b ∈ H.walkVertices u D

  So is the second.

• edges_mem (g : β) : g ∈ R → g ∈ F.edgeSet

  The crosscut lies in F.

• edges_new (g : β) : g ∈ R → g ∉ D ++ [e]

  "No edge of R is an edge of C."

• interior (y : α) : y ∈ H.walkVertices a R → y ≠ a → y ≠ b → y ∉ H.walkVertices u D

  "Its internal vertices do not lie on C."

• outside₁ : ∃ g ∈ D₁, g ∉ F.edgeSet

  "Each arc contains an edge outside Γ (j-1)."

• outside₂ : ∃ g ∈ D₂, g ∉ F.edgeSet

  The same for the other arc.

theorem Graph.exists_spliced_cycles {α : Type u_1} {β : Type u_2} {H F : Graph α β} {e : β} {u v a b : α} {D R D₁ D₂ : List β} (hcyc : H.IsCycleThrough e u v D) (hcc : H.IsCycleCrosscut F e u v D a b R D₁ D₂) : ∃ (e₁ : β) (e₂ : β) (u₁ : α) (v₁ : α) (u₂ : α) (v₂ : α) (T₁ : List β) (T₂ : List β), H.IsCycleThrough e₁ u₁ v₁ T₁ ∧ H.IsCycleThrough e₂ u₂ v₂ T₂ ∧ (e₁ :: T₁).Perm (D₁ ++ R) ∧ (e₂ :: T₂).Perm (D₂ ++ R)

The two cycles a crosscut splices, R ∪ C₁ and R ∪ C₂, as cycles of the ambient graph with their edge lists named. Both are produced by Graph.exists_spliced_cycle, applied to the cycle's own subgraph and to each arc in turn.

def Graph.edgesOutside {α : Type u_1} {β : Type u_2} (H : Graph α β) (W : List β) : Set β

The edges of a walk that the graph H does not have. The second measure of the blueprint's minimal-counterexample argument is the size of this set for H = Γ (j-1).

Equations

• H.edgesOutside W = {g : β | g ∈ W ∧ g ∉ H.edgeSet}

theorem Graph.mem_edgesOutside {α : Type u_1} {β : Type u_2} {H : Graph α β} {W : List β} {g : β} : g ∈ H.edgesOutside W ↔ g ∈ W ∧ g ∉ H.edgeSet

theorem Graph.finite_edgesOutside {α : Type u_1} {β : Type u_2} (H : Graph α β) (W : List β) : (H.edgesOutside W).Finite

theorem Graph.edgesOutside_append {α : Type u_1} {β : Type u_2} (H : Graph α β) (W₁ W₂ : List β) : H.edgesOutside (W₁ ++ W₂) = H.edgesOutside W₁ ∪ H.edgesOutside W₂

theorem Graph.edgesOutside_perm {α : Type u_1} {β : Type u_2} {H : Graph α β} {W₁ W₂ : List β} (hp : W₁.Perm W₂) : H.edgesOutside W₁ = H.edgesOutside W₂

theorem Graph.edgesOutside_eq_empty {α : Type u_1} {β : Type u_2} {H : Graph α β} {W : List β} (h : ∀ g ∈ W, g ∈ H.edgeSet) : H.edgesOutside W = ∅

theorem Graph.edgesOutside_splice_lt {α : Type u_1} {β : Type u_2} {H : Graph α β} {W W' D₁ D₂ R : List β} (hnodup : W.Nodup) (hperm : W.Perm (D₁ ++ D₂)) (hperm' : W'.Perm (D₁ ++ R)) (hR : ∀ g ∈ R, g ∈ H.edgeSet) (hD₂ : ∃ g ∈ D₂, g ∉ H.edgeSet) : (H.edgesOutside W').ncard < (H.edgesOutside W).ncard

The count the descent step decreases. Replacing one arc D₂ of a cycle by a list R of edges the graph H already has strictly lowers the number of edges outside H, provided the discarded arc had at least one such edge.

The two arcs of a cycle share no edge, which is why the discarded edge is not silently still present on the arc that was kept: that is what the Nodup hypothesis on the cycle's edge list supplies. It holds for a cycle because the detour of Graph.IsCycleThrough is a path and does not contain the named edge.

Enclosing a point

def Graph.Encloses {β : Type u_1} (H : Graph Schoenflies.Plane β) (drawing : β → ℝ → Schoenflies.Plane) (x : Schoenflies.Plane) : Prop

"That face is the interior of its boundary cycle, which therefore encloses x." A graph encloses a point when some cycle of it has that point in its interior.

Equations

• H.Encloses drawing x = ∃ (e : β) (u : Schoenflies.Plane) (v : Schoenflies.Plane) (D : List β), H.IsCycleThrough e u v D ∧ x ∈ Schoenflies.inside (Graph.edgesCover drawing (e :: D))

theorem Graph.Encloses.mono {β : Type u_1} {H K : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x : Schoenflies.Plane} (hHK : H ≤ K) (h : H.Encloses drawing x) : K.Encloses drawing x

A cycle of a subgraph encloses whatever it enclosed.

theorem Graph.isBounded_face_of_encloses {β : Type u_1} {H : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x : Schoenflies.Plane} (hx : x ∈ H.exterior drawing) (henc : H.Encloses drawing x) : Bornology.IsBounded (H.face drawing x)

"The face of H containing x is connected and disjoint from C; since it contains x ∈ Int(C) it lies in the bounded set Int(C)." An enclosed point has a bounded face.

theorem Graph.encloses_of_isBounded_face {β : Type u_1} {H : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x : Schoenflies.Plane} [H.Finite] (hd : H.IsDrawing drawing) (hpoly : ∀ g ∈ H.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing g)) (h2 : H.IsTwoConnected) (hx : x ∈ H.exterior drawing) (hb : Bornology.IsBounded (H.face drawing x)) : H.Encloses drawing x

"By lem:face-cycles, that face is the interior of its boundary cycle." A point in a bounded face of a finite 2-connected polygonal plane graph is enclosed by a cycle of it.

theorem Graph.exists_cycle_edgesOutside_lt {β : Type u_1} {drawing : β → ℝ → Schoenflies.Plane} {x : Schoenflies.Plane} {H F : Graph Schoenflies.Plane β} {e : β} {u v : Schoenflies.Plane} {D : List β} (hcyc : H.IsCycleThrough e u v D) {D₁ D₂ R : List β} (hperm : (e :: D).Perm (D₁ ++ D₂)) (hR : ∀ g ∈ R, g ∈ F.edgeSet) (h₁ : ∃ g ∈ D₁, g ∉ F.edgeSet) (h₂ : ∃ g ∈ D₂, g ∉ F.edgeSet) {e₁ e₂ : β} {u₁ v₁ u₂ v₂ : Schoenflies.Plane} {T₁ T₂ : List β} (hZ₁ : H.IsCycleThrough e₁ u₁ v₁ T₁) (hZ₂ : H.IsCycleThrough e₂ u₂ v₂ T₂) (hp₁ : (e₁ :: T₁).Perm (D₁ ++ R)) (hp₂ : (e₂ :: T₂).Perm (D₂ ++ R)) (hone : x ∈ Schoenflies.inside (edgesCover drawing (e₁ :: T₁)) ∨ x ∈ Schoenflies.inside (edgesCover drawing (e₂ :: T₂))) : ∃ (e' : β) (u' : Schoenflies.Plane) (v' : Schoenflies.Plane) (D' : List β), H.IsCycleThrough e' u' v' D' ∧ x ∈ Schoenflies.inside (edgesCover drawing (e' :: D')) ∧ (F.edgesOutside (e' :: D')).ncard < (F.edgesOutside (e :: D)).ncard

The last mile of the descent step. Suppose the cycle C = e :: D of H splits at two of its vertices into arcs carrying D₁ and D₂, each with an edge that the graph F does not have; suppose R is a list of edges of F; and suppose Z₁, Z₂ are cycles of H carrying D₁ ++ R and D₂ ++ R. If x is inside one of Z₁, Z₂, then some cycle of H encloses x with strictly fewer edges outside F than C has.

This is everything in the blueprint's crosscut paragraph after "exactly one of the two cycles R ∪ C₁, R ∪ C₂ encloses x", so a discharger of Graph.Descent has only to produce the crosscut and decide which side. The splitting of the cycle is Graph.IsCycleThrough.split_at and the two spliced cycles are Graph.exists_spliced_cycle; both hand back exactly the permutation statements assumed here.

The chain

structure Graph.IsPlaneChain {β : Type u_1} (Γ : ℕ → Graph Schoenflies.Plane β) (drawing : β → ℝ → Schoenflies.Plane) (G : Graph Schoenflies.Plane β) (n : ℕ) : Prop

The hypotheses of lem:outer-chain. Γ 0, …, Γ n are finite 2-connected polygonal plane graphs, all drawn inside one ambient plane graph G — which is what makes "after subdividing common points into vertices" true by construction — with consecutive members sharing at least two vertices and nonconsecutive members disjoint. n ≥ 2 is the blueprint's k ≥ 3.

• two_le : 2 ≤ n

  At least three graphs.

• le_ambient (p : ℕ) : p ≤ n → Γ p ≤ G

  Every member is drawn inside the ambient plane graph.

• isDrawing : G.IsDrawing drawing

  The ambient graph is a plane graph.

• polygonal (g : β) : g ∈ G.edgeSet → Schoenflies.IsPolygonal (edgeArc drawing g)

  Its edges are polygonal.

• finite (p : ℕ) : p ≤ n → (Γ p).Finite

  Every member is finite.

• twoConnected (p : ℕ) : p ≤ n → (Γ p).IsTwoConnected

  Every member is 2-connected.

• meet (p : ℕ) : p + 1 ≤ n → ∃ (a : Schoenflies.Plane) (b : Schoenflies.Plane), a ≠ b ∧ a ∈ (Γ p).vertexSet ∧ a ∈ (Γ (p + 1)).vertexSet ∧ b ∈ (Γ p).vertexSet ∧ b ∈ (Γ (p + 1)).vertexSet

  Consecutive members have at least two vertices in common.

• disjoint (p q : ℕ) : p ≤ n → q ≤ n → p + 1 < q → Disjoint ((Γ p).pointSet drawing) ((Γ q).pointSet drawing)

  Nonconsecutive members are disjoint — as point sets, which is what the blueprint means and what the crosscut step of the proof uses.

theorem Graph.IsPlaneChain.block_le {β : Type u_1} {Γ : ℕ → Graph Schoenflies.Plane β} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {n i m : ℕ} (h : IsPlaneChain Γ drawing G n) (hm : i + m ≤ n) : chainUnion Γ i m ≤ G

theorem Graph.IsPlaneChain.le_block {β : Type u_1} {Γ : ℕ → Graph Schoenflies.Plane β} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {n i m p : ℕ} (h : IsPlaneChain Γ drawing G n) (hm : i + m ≤ n) (hp : i ≤ p) (hp' : p ≤ i + m) : Γ p ≤ chainUnion Γ i m

theorem Graph.IsPlaneChain.block_finite {β : Type u_1} {Γ : ℕ → Graph Schoenflies.Plane β} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {n i m : ℕ} (h : IsPlaneChain Γ drawing G n) (hm : i + m ≤ n) : (chainUnion Γ i m).Finite

theorem Graph.IsPlaneChain.block_isDrawing {β : Type u_1} {Γ : ℕ → Graph Schoenflies.Plane β} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {n i m : ℕ} (h : IsPlaneChain Γ drawing G n) (hm : i + m ≤ n) : (chainUnion Γ i m).IsDrawing drawing

theorem Graph.IsPlaneChain.block_polygonal {β : Type u_1} {Γ : ℕ → Graph Schoenflies.Plane β} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {n i m : ℕ} (h : IsPlaneChain Γ drawing G n) (hm : i + m ≤ n) (g : β) : g ∈ (chainUnion Γ i m).edgeSet → Schoenflies.IsPolygonal (edgeArc drawing g)

theorem Graph.IsPlaneChain.block_isTwoConnected {β : Type u_1} {Γ : ℕ → Graph Schoenflies.Plane β} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {n i m : ℕ} (h : IsPlaneChain Γ drawing G n) (hm : i + m ≤ n) : (chainUnion Γ i m).IsTwoConnected

theorem Graph.IsPlaneChain.mem_pointSet_block {β : Type u_1} {Γ : ℕ → Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {i m : ℕ} {z : Schoenflies.Plane} (hz : z ∈ (chainUnion Γ i m).pointSet drawing) : ∃ (p : ℕ), i ≤ p ∧ p ≤ i + m ∧ z ∈ (Γ p).pointSet drawing

A point of a block's drawing lies on one of its members.

theorem Graph.IsPlaneChain.disjoint_block_far {β : Type u_1} {Γ : ℕ → Graph Schoenflies.Plane β} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {n i m : ℕ} (h : IsPlaneChain Γ drawing G n) (hm : i + m + 2 ≤ n) : Disjoint ((chainUnion Γ i m).pointSet drawing) ((Γ (i + m + 2)).pointSet drawing)

"Γ j meets the earlier chain only through Γ (j-1)." The block Γ i ∪ ⋯ ∪ Γ (i+m) and the member Γ (i+m+2) are disjoint, every pair of indices involved being nonconsecutive. This is the form the descent step consumes.

theorem Graph.IsPlaneChain.disjoint_vertexSet {β : Type u_1} {Γ : ℕ → Graph Schoenflies.Plane β} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {n p : ℕ} (h : IsPlaneChain Γ drawing G n) {q : ℕ} (hp : p ≤ n) (hq : q ≤ n) (hpq : p + 1 < q) : Disjoint (Γ p).vertexSet (Γ q).vertexSet

Nonconsecutive members share no vertex.

theorem Graph.IsPlaneChain.disjoint_edgeSet {β : Type u_1} {Γ : ℕ → Graph Schoenflies.Plane β} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {n p : ℕ} (h : IsPlaneChain Γ drawing G n) {q : ℕ} (hp : p ≤ n) (hq : q ≤ n) (hpq : p + 1 < q) : Disjoint (Γ p).edgeSet (Γ q).edgeSet

Nonconsecutive members share no edge: an edge of both would be drawn inside both point sets.

The assumed step

Everything in the blueprint's proof except this one paragraph is discharged below.

def Graph.Descent {β : Type u_1} (Γ : ℕ → Graph Schoenflies.Plane β) (drawing : β → ℝ → Schoenflies.Plane) (n : ℕ) (x : Schoenflies.Plane) : Prop

The crosscut step of lem:outer-chain, assumed.

Given a cycle C of the block Γ i ∪ ⋯ ∪ Γ (i+m+2) that encloses x, which has an edge of the last member Γ (i+m+2) outside Γ (i+m+1) and an edge of the earlier chain Γ i ∪ ⋯ ∪ Γ (i+m) outside Γ (i+m+1), there is a cycle of the same block that encloses x and has strictly fewer edges outside Γ (i+m+1).

This is the blueprint's paragraph beginning "Minimality of the interval implies that C contains an edge of Γ j outside Γ (j-1)": choose points a, b in the interiors of the two edges; each of the two arcs of C from a to b must meet Γ (j-1), because Γ j meets the earlier chain only through Γ (j-1); take the two maximal subpaths of C ∩ Γ (j-1) they contain and a minimum-length path R in Γ (j-1) from one to the other; R is a crosscut of the side of C it lies in, and thm:polygonal-crosscut says exactly one of R ∪ C₁, R ∪ C₂ encloses x. That cycle stays in the block, and one nonempty outside portion of C has been replaced by R ⊆ Γ (j-1).

It is a statement about a single descent step, not about outer faces, and it does not mention n except to keep the block inside the chain. A discharging module has Graph.IsCycleThrough.split_at, Graph.exists_spliced_cycle, Graph.IsDrawing.arcs_of_split and Schoenflies.crosscutSplitsRegion available.

Equations

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

Descent, split into a combinatorial and a geometric half

Graph.Descent is what the main theorem consumes, and Graph.descent_of_crosscut derives it from the two halves below, doing the splicing and the edge count in between. A module wishing to discharge Descent may therefore prove these two instead, which is the natural division of labour: CrosscutExists is a statement about walks in graphs with no geometry in it beyond the disjointness of nonconsecutive members, and CrosscutEncloses is a statement about one plane graph, one cycle and one crosscut, with no chain in it at all.

def Graph.CrosscutExists {β : Type u_1} (Γ : ℕ → Graph Schoenflies.Plane β) (drawing : β → ℝ → Schoenflies.Plane) (n : ℕ) (x : Schoenflies.Plane) : Prop

The combinatorial half of the descent step. The blueprint's "choose points a, b in the relative interiors of these two edges … each of those two arcs must meet Γ (j-1) … choose such a path R of minimum length": from a cycle of the block enclosing x with an edge of the last member and an edge of the earlier chain outside Γ (j-1), build a crosscut of that cycle inside Γ (j-1).

The hypothesis that x is enclosed is carried along because it costs nothing and a discharger may want it; the construction in the blueprint does not use it.

Equations

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

def Graph.OuterOnPairs {β : Type u_1} (Γ : ℕ → Graph Schoenflies.Plane β) (drawing : β → ℝ → Schoenflies.Plane) (n : ℕ) (x : Schoenflies.Plane) : Prop

The hypothesis of lem:outer-chain on consecutive pairs: x is in the outer face of every Γ p ∪ Γ (p+1) — off its drawing, with an unbounded face through it. A consumer proves the second clause with Graph.beyondSquare_subset_face, and Graph.unbounded_face_unique is what makes "an unbounded face" the outer face.

Equations

• Graph.OuterOnPairs Γ drawing n x = ∀ (p : ℕ), p + 1 ≤ n → x ∈ (Graph.chainUnion Γ p 1).exterior drawing ∧ ¬Bornology.IsBounded ((Graph.chainUnion Γ p 1).face drawing x)

theorem Graph.IsPlaneChain.not_encloses_pair {β : Type u_1} {Γ : ℕ → Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {n : ℕ} {x : Schoenflies.Plane} {p : ℕ} (hout : OuterOnPairs Γ drawing n x) (hp : p + 1 ≤ n) : ¬(chainUnion Γ p 1).Encloses drawing x

The base case, j = i + 1. No cycle of a consecutive pair encloses a point of that pair's outer face.

theorem Graph.IsPlaneChain.not_encloses_single {β : Type u_1} {Γ : ℕ → Graph Schoenflies.Plane β} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {n : ℕ} {x : Schoenflies.Plane} {p : ℕ} (h : IsPlaneChain Γ drawing G n) (hout : OuterOnPairs Γ drawing n x) (hp : p ≤ n) : ¬(Γ p).Encloses drawing x

The base case, j = i. A single member of the chain is contained in a consecutive pair — the one after it, or, at the far end, the one before it.

theorem Graph.IsPlaneChain.not_encloses {β : Type u_1} {Γ : ℕ → Graph Schoenflies.Plane β} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {n : ℕ} {x : Schoenflies.Plane} (h : IsPlaneChain Γ drawing G n) (hout : OuterOnPairs Γ drawing n x) (hdesc : Descent Γ drawing n x) (m i : ℕ) : i + m ≤ n → ¬(chainUnion Γ i m).Encloses drawing x

The double minimal-counterexample argument. No block of the chain encloses x.

The outer induction is on the length m of the block — the blueprint's "choose indices i ≤ j with j - i minimum". Inside it, for a block of length at least two, the induction on c is the blueprint's "choose C so that the number of its edges outside Γ (j-1) is minimum".

theorem Graph.IsPlaneChain.mem_exterior_chain {β : Type u_1} {Γ : ℕ → Graph Schoenflies.Plane β} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {n : ℕ} {x : Schoenflies.Plane} (h : IsPlaneChain Γ drawing G n) (hout : OuterOnPairs Γ drawing n x) : x ∈ (chainUnion Γ 0 n).exterior drawing

x is off the whole chain: it is off every consecutive pair, and every member belongs to one.

theorem Graph.IsPlaneChain.outer_chain {β : Type u_1} {Γ : ℕ → Graph Schoenflies.Plane β} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {n : ℕ} {x : Schoenflies.Plane} (h : IsPlaneChain Γ drawing G n) (hout : OuterOnPairs Γ drawing n x) (hdesc : Descent Γ drawing n x) : x ∈ (chainUnion Γ 0 n).exterior drawing ∧ ¬Bornology.IsBounded ((chainUnion Γ 0 n).face drawing x)

lem:outer-chain (outer face of a chain). If x is in the outer face of every consecutive pair Γ p ∪ Γ (p+1), then x is in the outer face of Γ 0 ∪ ⋯ ∪ Γ n.

"In the outer face" is x ∈ exterior … ∧ ¬ IsBounded (face … x); by Graph.unbounded_face_unique there is only one unbounded face, so this really does say x is in the outer face.