The utility graph K(3,3) inside a plane graph

The blueprint's proof of lem:k33 is four sentences: regard K(3,3) as the six-cycle x₀y₀x₁y₁x₂y₂x₀ together with the three remaining edges x₀y₁, x₁y₂, x₂y₀; the six-cycle is a Jordan curve; each remaining edge lies wholly on one side of it; two of the three lie on the same side, and their endpoints alternate on the six-cycle, contrary to cor:alternating-crosscuts.

Everything in that proof except the last two citations is established here. What is left is the polygonal Jordan curve theorem — which supplies "the two sides" — and the alternating crosscut corollary itself; neither exists yet, so lem:k33 is not stated. See the note at the end of this docstring for exactly how the last step will read.

K(3,3) is a configuration, not a graph

There is no K33 : Graph α β. A copy of K(3,3) inside G is Graph.IsK33Config G x y e: six vertices x 0, x 1, x 2, y 0, y 1, y 2, all distinct, and nine edge names e i j with e i j linking x i to y j. Nothing says G has no other vertex or edge.

This is the shape the theorem is used in — one always finds a K(3,3) inside a graph one already has, never constructs the abstract one — and it is also what makes the drawing hypothesis land correctly: Graph.IsDrawing G drawing is a hypothesis about all of G, so taking G larger only strengthens it.

Two economies follow from stating the configuration this way. The nine edge names are automatically distinct (Graph.IsK33Config.eq_of_e_eq): an edge has only two ends, so two names coinciding would force the index pairs to agree. And no looplessness clause is needed: x i ≠ y j is one of the four fields.

The indexing is arithmetic in Fin 3, so that decide can do the bookkeeping

The six-cycle uses the edges e i i and e (i+1) i; the three remaining edges are e s (s+1) for s : Fin 3. Every combinatorial side condition below — that a remaining edge is not a cycle edge, that the two arcs of the cut cycle cover it and meet only at the cut points — is a statement about index pairs quantified over Fin 3, and is discharged by decide. The edges themselves never have to be compared.

The two arcs into which the ends of the remaining edge e s (s+1) cut the six-cycle are named by their index pairs as well (Graph.arcAPairs, Graph.arcBPairs); Graph.arcA and Graph.arcB are the corresponding edge lists, rfl-equal to the mapped pair lists so that both presentations are available with no conversion lemma.

Blueprint

• Graph.IsK33Config — a copy of the utility graph.
• Graph.IsK33Config.hexagon_isCycleThrough — §"Plane graphs and the utility graph": "regard K(3,3) as the six-cycle x₁y₁x₂y₂x₃y₃x₁ together with the three remaining edges".
• Graph.IsK33Config.hexagon_isJordanCurve — lem:k33, "the six-cycle is a polygonal Jordan curve". Polygonality plays no part; it is needed only where the polygonal Jordan curve theorem is applied to the result.
• Graph.IsK33Config.chord_inter_hexSet, Graph.IsK33Config.chord_openArc_eq, Graph.IsK33Config.chord_openArc_subset_connectedComponentIn — lem:k33, "each remaining edge lies wholly on one side": a remaining edge meets the six-cycle in exactly its own two ends, so its interior is a connected subset of the complement, hence lies in one component. This is also the crosscut hypothesis of thm:polygonal-crosscut and cor:alternating-crosscuts.
• Graph.IsK33Config.exists_two_chords_same_side — lem:k33, "two of the three lie on the same side". The two sides arrive as an arbitrary pair of disjoint open sets covering the complement, which is the form thm:polygonal-jordan will supply them in.
• Graph.IsK33Config.chords_alternate — lem:k33, "their endpoints alternate on the six-cycle", in the form cor:alternating-crosscuts consumes: the ends of one remaining edge cut the cycle into two arcs meeting only at those ends, and the two ends of another remaining edge lie one interior to each. Every pair of remaining edges is of the form (s, s+1), so the single index s covers all three pairs.
• Graph.IsK33Config.chords_disjoint — the disjointness that cor:alternating-crosscuts contradicts: two remaining edges have four distinct ends, and distinct edges of a plane graph meet only at a shared end.

How lem:k33 will close. Given a plane drawing of a graph with a K(3,3) configuration, make it polygonal (Graph.polygonal_redrawing, lem:polygonal-redrawing); the six-cycle is then a polygonal Jordan curve, and thm:polygonal-jordan gives the two disjoint open sides that exists_two_chords_same_side wants. It returns two remaining edges on the same side; chords_alternate says their ends alternate, so cor:alternating-crosscuts makes them meet, and chords_disjoint says they do not.

structure Graph.IsK33Config {α : Type u_1} {β : Type u_2} (G : Graph α β) (x y : Fin 3 → α) (e : Fin 3 → Fin 3 → β) : Prop

A copy of the utility graph K(3,3) inside G.

• isLink (i j : Fin 3) : G.IsLink (e i j) (x i) (y j)

  e i j joins the i-th vertex of one side to the j-th vertex of the other.

• x_injective : Function.Injective x

  The three vertices of the first side are distinct.

• y_injective : Function.Injective y

  The three vertices of the second side are distinct.

• ne (i j : Fin 3) : x i ≠ y j

  The two sides are disjoint.

theorem Graph.IsK33Config.x_ne_x {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : Fin 3 → α} {e : Fin 3 → Fin 3 → β} {i k : Fin 3} (h : G.IsK33Config x y e) (hik : i ≠ k) : x i ≠ x k

theorem Graph.IsK33Config.y_ne_y {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : Fin 3 → α} {e : Fin 3 → Fin 3 → β} {j l : Fin 3} (h : G.IsK33Config x y e) (hjl : j ≠ l) : y j ≠ y l

theorem Graph.IsK33Config.x_ne_y {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : Fin 3 → α} {e : Fin 3 → Fin 3 → β} (h : G.IsK33Config x y e) (i j : Fin 3) : x i ≠ y j

theorem Graph.IsK33Config.y_ne_x {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : Fin 3 → α} {e : Fin 3 → Fin 3 → β} (h : G.IsK33Config x y e) (j i : Fin 3) : y j ≠ x i

theorem Graph.IsK33Config.eq_of_e_eq {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : Fin 3 → α} {e : Fin 3 → Fin 3 → β} {i j k l : Fin 3} (h : G.IsK33Config x y e) (heq : e i j = e k l) : i = k ∧ j = l

The nine edges carry nine different names. This is not an axiom of the configuration: an edge has only two ends, so two of the nine names being equal would force the two index pairs to agree.

theorem Graph.IsK33Config.e_ne {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : Fin 3 → α} {e : Fin 3 → Fin 3 → β} {i j k l : Fin 3} (h : G.IsK33Config x y e) (hne : ¬(i = k ∧ j = l)) : e i j ≠ e k l

theorem Graph.IsK33Config.inc_elim {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : Fin 3 → α} {e : Fin 3 → Fin 3 → β} {i j : Fin 3} {z : α} (h : G.IsK33Config x y e) (hz : G.Inc (e i j) z) : z = x i ∨ z = y j

A vertex on one of the nine edges is one of that edge's two ends.

theorem Graph.IsK33Config.notMem_walkVertices {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : Fin 3 → α} {e : Fin 3 → Fin 3 → β} {z : α} (h : G.IsK33Config x y e) {W : List β} {w : α} (hzw : z ≠ w) (hW : ∀ f ∈ W, ∃ (i : Fin 3) (j : Fin 3), f = e i j ∧ z ≠ x i ∧ z ≠ y j) : z ∉ G.walkVertices w W

Freshness, in the form the path constructor asks for. A vertex which is neither the source of the rest of the walk nor an end of any of its edges is not among the vertices that rest visits.

The six-cycle

The blueprint reads K(3,3) as the six-cycle x₀y₀x₁y₁x₂y₂x₀ together with the three remaining edges. The cycle is presented as Schoenflies/Graph/Cycle.lean presents one: through the edge e 0 0, with a detour path running the other way round.

def Graph.hexPairs : List (Fin 3 × Fin 3)

The index pairs of the six edges of the six-cycle, in the order the cycle is traversed starting from e 0 0. Kept as index pairs, not as edges, because every question about which edges the cycle uses is then decidable.

Equations

• Graph.hexPairs = [(0, 0), (0, 2), (2, 2), (2, 1), (1, 1), (1, 0)]

def Graph.hexDetour {β : Type u_2} (e : Fin 3 → Fin 3 → β) : List β

The five edges of the detour of the six-cycle: the path x₀ → y₂ → x₂ → y₁ → x₁ → y₀ that returns to the other end of e 0 0.

Equations

• Graph.hexDetour e = [e 0 2, e 2 2, e 2 1, e 1 1, e 1 0]

def Graph.hexList {β : Type u_2} (e : Fin 3 → Fin 3 → β) : List β

The six edges of the six-cycle.

Equations

• Graph.hexList e = e 0 0 :: Graph.hexDetour e

theorem Graph.hexList_eq_map {β : Type u_2} (e : Fin 3 → Fin 3 → β) : hexList e = List.map (fun (p : Fin 3 × Fin 3) => e p.1 p.2) hexPairs

theorem Graph.mem_hexList_iff {β : Type u_2} {e : Fin 3 → Fin 3 → β} {f : β} : f ∈ hexList e ↔ ∃ p ∈ hexPairs, f = e p.1 p.2

theorem Graph.IsK33Config.hexDetour_isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : Fin 3 → α} {e : Fin 3 → Fin 3 → β} (h : G.IsK33Config x y e) : G.IsPath (x 0) (hexDetour e) (y 0)

The detour of the six-cycle is a path. Each freshness clause says that the vertex a step departs from is none of the six vertices the rest of the detour meets.

theorem Graph.IsK33Config.hexagon_isCycleThrough {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : Fin 3 → α} {e : Fin 3 → Fin 3 → β} (h : G.IsK33Config x y e) : G.IsCycleThrough (e 0 0) (x 0) (y 0) (hexDetour e)

The six-cycle is a cycle, presented through the edge e 0 0.

The three remaining edges

e s (s+1), for s : Fin 3, are the three edges of K(3,3) that the six-cycle leaves out.

theorem Graph.IsK33Config.chord_notMem_hexList {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : Fin 3 → α} {e : Fin 3 → Fin 3 → β} (h : G.IsK33Config x y e) (s : Fin 3) : e s (s + 1) ∉ hexList e

The three remaining edges are not edges of the six-cycle.

theorem Graph.IsK33Config.chord_ne {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : Fin 3 → α} {e : Fin 3 → Fin 3 → β} {s t : Fin 3} (h : G.IsK33Config x y e) (hst : s ≠ t) : e s (s + 1) ≠ e t (t + 1)

Two distinct remaining edges carry distinct names, and share no end.

theorem Graph.IsK33Config.hexList_edge_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : Fin 3 → α} {e : Fin 3 → Fin 3 → β} (h : G.IsK33Config x y e) {f : β} (hf : f ∈ hexList e) : f ∈ G.edgeSet

The edges of the six-cycle are edges of the graph.

theorem Graph.mem_hexList {β : Type u_2} (e : Fin 3 → Fin 3 → β) {p : Fin 3 × Fin 3} (hp : p ∈ hexPairs) : e p.1 p.2 ∈ hexList e

The six-cycle cut at the ends of one remaining edge

The two ends of the remaining edge e s (s+1) are x s and y (s+1), and they cut the six-cycle into two paths: x s → y s → x (s+1) → y (s+1) and x s → y (s+2) → x (s+2) → y (s+1). The other two remaining edges each have one end interior to the first and one end interior to the second — this is the blueprint's "their endpoints alternate on the six-cycle".

def Graph.arcAPairs (s : Fin 3) : List (Fin 3 × Fin 3)

Index pairs of the first of the two paths the ends of e s (s+1) cut the six-cycle into.

Equations

• Graph.arcAPairs s = [(s, s), (s + 1, s), (s + 1, s + 1)]

def Graph.arcBPairs (s : Fin 3) : List (Fin 3 × Fin 3)

Index pairs of the second of the two paths.

Equations

• Graph.arcBPairs s = [(s, s + 2), (s + 2, s + 2), (s + 2, s + 1)]

def Graph.arcA {β : Type u_2} (e : Fin 3 → Fin 3 → β) (s : Fin 3) : List β

The edges of the first path.

Equations

• Graph.arcA e s = [e s s, e (s + 1) s, e (s + 1) (s + 1)]

def Graph.arcB {β : Type u_2} (e : Fin 3 → Fin 3 → β) (s : Fin 3) : List β

The edges of the second path.

Equations

• Graph.arcB e s = [e s (s + 2), e (s + 2) (s + 2), e (s + 2) (s + 1)]

theorem Graph.arcA_eq_map {β : Type u_2} (e : Fin 3 → Fin 3 → β) (s : Fin 3) : arcA e s = List.map (fun (p : Fin 3 × Fin 3) => e p.1 p.2) (arcAPairs s)

theorem Graph.arcB_eq_map {β : Type u_2} (e : Fin 3 → Fin 3 → β) (s : Fin 3) : arcB e s = List.map (fun (p : Fin 3 × Fin 3) => e p.1 p.2) (arcBPairs s)

theorem Graph.IsK33Config.arcA_isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : Fin 3 → α} {e : Fin 3 → Fin 3 → β} (h : G.IsK33Config x y e) (s : Fin 3) : G.IsPath (x s) (arcA e s) (y (s + 1))

The first of the two paths is a path.

theorem Graph.IsK33Config.arcB_isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {x y : Fin 3 → α} {e : Fin 3 → Fin 3 → β} (h : G.IsK33Config x y e) (s : Fin 3) : G.IsPath (x s) (arcB e s) (y (s + 1))

The second of the two paths is a path.

The six-cycle drawn in the plane

Everything from here on is about a drawing of the configuration. Nothing in this section uses more geometry than the three clauses of Graph.IsDrawing.

def Graph.hexSet {β : Type u_1} (drawing : β → ℝ → Schoenflies.Plane) (e : Fin 3 → Fin 3 → β) : Set Schoenflies.Plane

The point set of the six-cycle of a drawn K(3,3).

Equations

• Graph.hexSet drawing e = Graph.edgesCover drawing (Graph.hexList e)

theorem Graph.mem_edgesCover_map_iff {β : Type u_1} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} {L : List (Fin 3 × Fin 3)} {p : Schoenflies.Plane} : p ∈ edgesCover drawing (List.map (fun (q : Fin 3 × Fin 3) => e q.1 q.2) L) ↔ ∃ q ∈ L, p ∈ edgeArc drawing (e q.1 q.2)

theorem Graph.mem_hexSet_iff {β : Type u_1} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} {p : Schoenflies.Plane} : p ∈ hexSet drawing e ↔ ∃ q ∈ hexPairs, p ∈ edgeArc drawing (e q.1 q.2)

theorem Graph.mem_arcA_iff {β : Type u_1} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} {s : Fin 3} {p : Schoenflies.Plane} : p ∈ edgesCover drawing (arcA e s) ↔ ∃ q ∈ arcAPairs s, p ∈ edgeArc drawing (e q.1 q.2)

theorem Graph.mem_arcB_iff {β : Type u_1} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} {s : Fin 3} {p : Schoenflies.Plane} : p ∈ edgesCover drawing (arcB e s) ↔ ∃ q ∈ arcBPairs s, p ∈ edgeArc drawing (e q.1 q.2)

theorem Graph.IsK33Config.hexagon_isJordanCurve {β : Type u_1} {G : Graph Schoenflies.Plane β} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) : Schoenflies.IsJordanCurve (hexSet drawing e)

The six-cycle of a drawn K(3,3) is a Jordan curve. This is the blueprint's "the six-cycle is a polygonal Jordan curve"; polygonality plays no part in it, and is needed only where the polygonal Jordan curve theorem is applied to the result.

theorem Graph.IsK33Config.x_mem_hexSet {β : Type u_1} {G : Graph Schoenflies.Plane β} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) (i : Fin 3) : x i ∈ hexSet drawing e

The i-th vertex of the first side lies on the six-cycle.

theorem Graph.IsK33Config.y_mem_hexSet {β : Type u_1} {G : Graph Schoenflies.Plane β} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) (j : Fin 3) : y j ∈ hexSet drawing e

The j-th vertex of the second side lies on the six-cycle.

theorem Graph.IsK33Config.chord_inter_hexSet {β : Type u_1} {G : Graph Schoenflies.Plane β} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) (s : Fin 3) : edgeArc drawing (e s (s + 1)) ∩ hexSet drawing e = {x s, y (s + 1)}

Each of the three remaining edges is a crosscut of the six-cycle: its arc meets the cycle in exactly its own two ends.

theorem Graph.IsK33Config.chord_openArc_eq {β : Type u_1} {G : Graph Schoenflies.Plane β} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) (s : Fin 3) : Schoenflies.openArc (drawing (e s (s + 1))) = edgeArc drawing (e s (s + 1)) \ {x s, y (s + 1)}

The interior of a remaining edge, as the blueprint reads it: its arc without its two ends.

theorem Graph.IsK33Config.chord_openArc_subset_compl {β : Type u_1} {G : Graph Schoenflies.Plane β} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) (s : Fin 3) : Schoenflies.openArc (drawing (e s (s + 1))) ⊆ (hexSet drawing e)ᶜ

A remaining edge lies wholly off the six-cycle except at its ends.

theorem Graph.IsK33Config.chord_openArc_isPreconnected {β : Type u_1} {G : Graph Schoenflies.Plane β} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) (s : Fin 3) : IsPreconnected (Schoenflies.openArc (drawing (e s (s + 1))))

theorem Graph.IsK33Config.chord_openArc_nonempty {β : Type u_1} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} (s : Fin 3) : (Schoenflies.openArc (drawing (e s (s + 1)))).Nonempty

theorem Graph.IsK33Config.chord_openArc_subset_connectedComponentIn {β : Type u_1} {G : Graph Schoenflies.Plane β} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) (s : Fin 3) {p : Schoenflies.Plane} (hp : p ∈ Schoenflies.openArc (drawing (e s (s + 1)))) : Schoenflies.openArc (drawing (e s (s + 1))) ⊆ connectedComponentIn (hexSet drawing e)ᶜ p

Each of the three remaining edges lies wholly on one side of the six-cycle: its interior, being connected and disjoint from the cycle, lies in a single connected component of the complement.

theorem Graph.IsK33Config.chords_disjoint {β : Type u_1} {G : Graph Schoenflies.Plane β} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} {s t : Fin 3} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) (hst : s ≠ t) : edgeArc drawing (e s (s + 1)) ∩ edgeArc drawing (e t (t + 1)) = ∅

Two distinct remaining edges are disjoint. Their four ends are distinct, and two distinct edges of a plane graph meet only at a shared end.

The two arcs the ends of a remaining edge cut the six-cycle into

theorem Graph.IsK33Config.arcA_isArcBetween {β : Type u_1} {G : Graph Schoenflies.Plane β} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) (s : Fin 3) : Schoenflies.IsArcBetween (edgesCover drawing (arcA e s)) (x s) (y (s + 1))

theorem Graph.IsK33Config.arcB_isArcBetween {β : Type u_1} {G : Graph Schoenflies.Plane β} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) (s : Fin 3) : Schoenflies.IsArcBetween (edgesCover drawing (arcB e s)) (x s) (y (s + 1))

theorem Graph.IsK33Config.arcs_union {β : Type u_1} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} (s : Fin 3) : edgesCover drawing (arcA e s) ∪ edgesCover drawing (arcB e s) = hexSet drawing e

The two arcs make up the six-cycle.

theorem Graph.IsK33Config.arcs_inter {β : Type u_1} {G : Graph Schoenflies.Plane β} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) (s : Fin 3) : edgesCover drawing (arcA e s) ∩ edgesCover drawing (arcB e s) = {x s, y (s + 1)}

The two arcs meet exactly in the two ends of the remaining edge that cuts the cycle.

theorem Graph.IsK33Config.chords_alternate {β : Type u_1} {G : Graph Schoenflies.Plane β} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) (s : Fin 3) : ∃ (A : Set Schoenflies.Plane) (B : Set Schoenflies.Plane), Schoenflies.IsArcBetween A (x s) (y (s + 1)) ∧ Schoenflies.IsArcBetween B (x s) (y (s + 1)) ∧ A ∪ B = hexSet drawing e ∧ A ∩ B = {x s, y (s + 1)} ∧ x (s + 1) ∈ A \ {x s, y (s + 1)} ∧ y (s + 1 + 1) ∈ B \ {x s, y (s + 1)}

The endpoints of two of the three remaining edges alternate on the six-cycle.

The remaining edge indexed by s has ends x s and y (s+1); they cut the six-cycle into two arcs A and B meeting only in those two points. The remaining edge indexed by s+1 has ends x (s+1) and y (s+1+1), and this says one of them is interior to A and the other interior to B. Since the three remaining edges are indexed by Fin 3, every pair of them is of this form, which is what the blueprint's "their endpoints alternate on the six-cycle" asserts.

Two of the three remaining edges lie on the same side

theorem Graph.IsK33Config.chord_subset_or {β : Type u_1} {G : Graph Schoenflies.Plane β} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) {U V : Set Schoenflies.Plane} (hUo : IsOpen U) (hVo : IsOpen V) (hUV : Disjoint U V) (hcover : (hexSet drawing e)ᶜ ⊆ U ∪ V) (s : Fin 3) : Schoenflies.openArc (drawing (e s (s + 1))) ⊆ U ∨ Schoenflies.openArc (drawing (e s (s + 1))) ⊆ V

A remaining edge lies wholly in one of two disjoint open sets covering the complement of the six-cycle: its interior is connected and misses the cycle.

theorem Graph.IsK33Config.exists_two_chords_same_side {β : Type u_1} {G : Graph Schoenflies.Plane β} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} {drawing : β → ℝ → Schoenflies.Plane} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) {U V : Set Schoenflies.Plane} (hUo : IsOpen U) (hVo : IsOpen V) (hUV : Disjoint U V) (hcover : (hexSet drawing e)ᶜ ⊆ U ∪ V) : ∃ (s : Fin 3) (t : Fin 3), s ≠ t ∧ (Schoenflies.openArc (drawing (e s (s + 1))) ⊆ U ∧ Schoenflies.openArc (drawing (e t (t + 1))) ⊆ U ∨ Schoenflies.openArc (drawing (e s (s + 1))) ⊆ V ∧ Schoenflies.openArc (drawing (e t (t + 1))) ⊆ V)

Two of the three remaining edges lie on the same side of the six-cycle. The blueprint's "two of the three lie on the same side": three edges, two sides. The two sides arrive here as an arbitrary pair of disjoint open sets covering the complement of the cycle, which is the form the polygonal Jordan curve theorem supplies them in.