Building the crosscut of the outer-chain descent

Graph.CrosscutExists, the combinatorial half of the descent step of lem:outer-chain, discharged. Nothing here is geometric: the only fact about the plane that enters is Graph.IsPlaneChain.disjoint_block_far, "Γ j meets the earlier chain only through Γ (j-1)", and it is used exactly twice, to say that a vertex cannot lie on both Γ i ∪ ⋯ ∪ Γ (j-2) and Γ j.

The blueprint's argument, and how it is formalised here

The blueprint chooses points a, b in the relative interiors of an edge of Γ j and an edge of the earlier chain, cuts the cycle C there, observes that each of the two arcs must meet Γ (j-1), and takes a minimum-length path of Γ (j-1) between two maximal subpaths of C ∩ Γ (j-1) lying on different arcs.

Cutting a cycle at interior points of two of its edges is, combinatorially, the statement that two distinct edges g₁ ≠ g₂ of the cycle split the remaining edges into two arcs (Graph.IsCycleThrough.split_at_edges): the closed walk reads

… ─g₁→ p ─W₁→ q ─g₂→ q' ─W₂→ p' ─g₁→ …

and the two arcs are W₁ and W₂, whose visited sets S₁, S₂ are disjoint and cover the vertices of the cycle. That pair of facts replaces the notion of a maximal subpath entirely:

• "a and b lie on different maximal subpaths of C ∩ Γ (j-1)" becomes a ∈ S₁, b ∈ S₂;
• the property of maximal subpaths that the argument actually consumes — that no subpath of C ∩ Γ (j-1) joins two of them — becomes Graph.exists_isCycleCrosscut's hypothesis hpres: every edge of the cycle that Γ (j-1) also has keeps both of its ends on the same side. That is immediate here, because the only cycle edges joining the two sides are g₁ and g₂, and neither is an edge of Γ (j-1).

With that, walking along cycle edges of Γ (j-1) cannot cross from S₁ to S₂, and all four minimality clauses of Graph.IsCycleCrosscut fall out of one minimisation: among all walks of Γ (j-1) from S₁ to S₂, take one of least length.

• it is a path, because any walk between its own two ends is a competitor (Graph.IsWalk.isPath_of_minLength);
• its internal vertices miss C, because a vertex of C on it lies in S₁ or in S₂, and either way one of the two halves is a strictly shorter competitor;
• no edge of it is an edge of C: such an edge has both ends on C, hence both ends among {a, b} by the previous clause, hence joins S₁ to S₂ while lying in Γ (j-1), which hpres forbids;
• each arc of C between a and b carries an edge outside Γ (j-1), since otherwise the arc itself would be a walk of cycle edges of Γ (j-1) from S₁ to S₂.

Two general lemmas

Graph.IsPath.split_at_edge (cut a path at one of its edges, with the two freshness clauses Graph.IsCycleThrough.split_aux asks for) and Graph.IsCycleThrough.rotate (present a cycle through any one of its edges) are general facts about walks with nothing to do with this development; they are the missing companions of Graph.IsPath.split_meet and Graph.IsCycleThrough.split_at and belong in Schoenflies/Graph/Walk.lean and Schoenflies/FaceCyclesProof.lean respectively.

Blueprint

• Graph.IsPath.split_at_edge, Graph.IsCycleThrough.rotate, Graph.IsCycleThrough.split_at_edges — "choose points a, b in the relative interiors of these two edges. The two arcs of the cycle C from a to b are internally disjoint", read combinatorially (lem:outer-chain).
• Graph.exists_isCycleCrosscut — "since Γ_{j-1} is connected, there is a path in Γ_{j-1} from P to C ∖ V(P). Choose such a path R of minimum length …", the whole minimality paragraph of lem:outer-chain, with the chain abstracted away into the two sides S₁, S₂.
• Graph.IsPlaneChain.crosscutExists — Graph.CrosscutExists, the combinatorial half of the descent step of lem:outer-chain.

Cutting a path at an edge, and rotating a cycle

theorem Graph.IsPath.split_at_edge {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} {g : β} (h : G.IsPath u W v) (hg : g ∈ W) : ∃ (W₁ : List β) (W₂ : List β) (c : α) (d : α), W = W₁ ++ g :: W₂ ∧ G.IsPath u W₁ c ∧ G.IsLink g c d ∧ G.IsPath d W₂ v ∧ c ∉ G.walkVertices d W₂ ∧ ∀ z ∈ G.walkVertices u W₁, z ∈ G.walkVertices c (g :: W₂) → z = c

A path cut at one of its edges. The two extra clauses are exactly what Graph.IsCycleThrough.split_aux asks for: the near half never returns to the far end of the cut edge, and a vertex reached by both halves is the near end of it.

This is the edge-indexed companion of Graph.IsPath.split_meet, which cuts at a vertex.

theorem Graph.IsCycleThrough.rotate {α : Type u_1} {β : Type u_2} {G : Graph α β} {e g : β} {u v : α} {D : List β} (hc : G.IsCycleThrough e u v D) (hg : g ∈ e :: D) : ∃ (c : α) (d : α) (W : List β), G.IsCycleThrough g c d W ∧ (g :: W).Perm (e :: D)

A cycle presented through any one of its edges. Graph.IsCycleThrough names one edge and one path; this re-presents the same cycle with a different edge named, which is what an argument that has to start walking at a given edge needs.

theorem Graph.IsCycleThrough.mem_walkVertices_of_inc {α : Type u_1} {β : Type u_2} {G : Graph α β} {e f : β} {u v z : α} {D : List β} (hc : G.IsCycleThrough e u v D) (hf : f ∈ e :: D) (hz : G.Inc f z) : z ∈ G.walkVertices u D

Both ends of an edge of a cycle are vertices of the cycle.

theorem Graph.IsCycleThrough.split_at_edges {α : Type u_1} {β : Type u_2} {G : Graph α β} {e g₁ g₂ : β} {u v : α} {D : List β} (hc : G.IsCycleThrough e u v D) (hg₁ : g₁ ∈ e :: D) (hg₂ : g₂ ∈ e :: D) (hne : g₁ ≠ g₂) : ∃ (p : α) (p' : α) (q : α) (q' : α) (W₁ : List β) (W₂ : List β), G.IsLink g₁ p' p ∧ G.IsPath p W₁ q ∧ G.IsLink g₂ q q' ∧ G.IsPath q' W₂ p' ∧ (g₁ :: (W₁ ++ g₂ :: W₂)).Perm (e :: D) ∧ Disjoint (G.walkVertices p W₁) (G.walkVertices q' W₂) ∧ G.walkVertices u D = G.walkVertices p W₁ ∪ G.walkVertices q' W₂

A cycle cut at two of its edges is two arcs. This is the blueprint's "choose points a, b in the relative interiors of these two edges; the two arcs of the cycle C from a to b are internally disjoint", with the two interior points replaced by the two edges themselves: the closed walk reads … ─g₁→ p ─W₁→ q ─g₂→ q' ─W₂→ p' ─g₁→ …, and the two arcs W₁, W₂ visit disjoint sets of vertices which together are all the vertices of the cycle.

The crosscut, from a two-sided cycle and a connected subgraph

theorem Graph.exists_isCycleCrosscut {α : Type u_1} {β : Type u_2} {H F : Graph α β} {e : β} {u v : α} {D : List β} (hcyc : H.IsCycleThrough e u v D) (hFH : F ≤ H) {S₁ S₂ : Set α} (hdisj : Disjoint S₁ S₂) (hcover : H.walkVertices u D = S₁ ∪ S₂) (hpres : ∀ f ∈ e :: D, f ∈ F.edgeSet → ∀ (z w : α), H.IsLink f z w → (z ∈ S₁ ↔ w ∈ S₁)) (hconn : F.Connected) (ha : ∃ a ∈ S₁, a ∈ F.vertexSet) (hb : ∃ b ∈ S₂, b ∈ F.vertexSet) : ∃ (a : α) (b : α) (R : List β) (D₁ : List β) (D₂ : List β), H.IsCycleCrosscut F e u v D a b R D₁ D₂

The minimality paragraph of lem:outer-chain, with the chain abstracted away.

The cycle e :: D of H has its vertices split into two disjoint sides S₁, S₂ — in the application, the two arcs cut off by an edge of Γ j and an edge of the earlier chain — in such a way that no edge of the cycle lying in F joins the two sides (hpres). If F is connected and has a vertex on each side, then a minimum-length path of F from one side to the other is a crosscut of the cycle in the sense of Graph.IsCycleCrosscut.

hpres is what the blueprint's maximal subpaths of C ∩ Γ (j-1) are for: it is the only property of them the argument uses, and here it is a one-line consequence of the two cut edges being outside F.

The descent step's crosscut

theorem Graph.IsPlaneChain.crosscutExists {β : Type u_1} {Γ : ℕ → Graph Schoenflies.Plane β} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {n : ℕ} (h : IsPlaneChain Γ drawing G n) {x : Schoenflies.Plane} : CrosscutExists Γ drawing n x

Graph.CrosscutExists, discharged. From a cycle of the block Γ i ∪ ⋯ ∪ Γ (i+m+2) carrying an edge of Γ (i+m+2) and an edge of the earlier chain, both outside Γ (i+m+1), build a crosscut of that cycle inside Γ (i+m+1).

The two named edges cut the cycle into two arcs (Graph.IsCycleThrough.split_at_edges). Each arc has a vertex in Γ (i+m+1): walking along it from the edge of Γ (i+m+2) to the edge of the earlier chain leaves V(Γ (i+m+2)) at some edge, and that edge belongs neither to Γ (i+m+2) (both its ends would stay inside) nor to the earlier chain (its end inside V(Γ (i+m+2)) would then lie on both, which Graph.IsPlaneChain.disjoint_block_far forbids), so it belongs to Γ (i+m+1). The rest is Graph.exists_isCycleCrosscut.