Discharging the realization hypothesis of lem:k33

Schoenflies/Graph/K33Planar.lean proves the nonplanarity of K(3,3) from one assumption, Graph.IsHexRealization: that the six-cycle, the two arcs the chord cuts it into, and the two closed curves the chord forms with them are all presented by cyclic vertex lists. Schoenflies/Realization.lean now supplies the presentations. This module wires the two together.

Blueprint

• Schoenflies.exists_poly_anchored, Schoenflies.IsPolygonal.union, Graph.IsDrawing.isPolygonal_edgesCover — §1: a polygonal set is the carrier of a vertex list running between any two of its points, so two polygonal sets that meet have a polygonal union, and a walk of a polygonal plane graph draws a polygonal set.
• Schoenflies.ClosedPolygon.reverse — a closed polygon read backwards.
• Schoenflies.ClosedPolygon.arc_vertex_eq, …arcPieces_eq — the decomposition of an arc is the arc's own: two closed polygons that share an arc, starting at the same vertex, run through the same vertices along it. This is what makes the three presentations below fit together into one crosscut.
• Schoenflies.exists_closedPolygon_arcs_oriented — the realization of a splitting with the first arc's direction fixed as well, so that two realizations of one arc can be compared.
• Graph.IsK33Config.isPolygonal_hexSet, …chord_inter_arcA, …chord_inter_arcB — the three curves the crosscut is built from, as polygonal Jordan curves.
• Graph.IsHexGeneric — the general-position hypothesis that survives: at each of the two cut points, the six-cycle and both spliced curves turn.
• Graph.IsK33Config.isHexRealization — Graph.IsHexRealization, discharged from it. This is the theorem this module exists for.
• Graph.Bendable, Graph.IsK33Config.false_of_hexGeneric, …not_isDrawing_of_bendable, Graph.IsArcK33.false_of_bendable, Graph.IsK33Subdivision.false_of_bendable, Graph.k33Graph_not_isDrawing — lem:k33 and cor:k33-subdivision with IsHexRealization replaced by IsHexGeneric.

What is still assumed, and why — READ THIS BEFORE USING THE THEOREMS BELOW

Milestone H8 is not closed here. Graph.IsHexRealization is gone, but a strictly smaller hypothesis has taken its place, and it is not discharged.

Schoenflies.ClosedPolygon forbids a vertex at which the curve runs straight through, and Schoenflies.ClosedPolygon.isCornerAt_vertex says that this is not a defect of the proofs: every vertex of every realization is a corner of the curve. A crosscut whose ends are cut points of C therefore forces those ends to be corners — of C, and of both curves the crosscut forms with the two arcs. Graph.IsHexGeneric says exactly that and nothing more, and by the two corner theorems it cannot be weakened while the crosscut is presented as a Schoenflies.IsPolygonalCrosscut.

For a drawn K(3,3) it is the statement that at each of the six vertices the three edges leave along three pairwise non-collinear germs. A polygonal drawing need not have that: two of the three edges at a vertex may leave along exactly opposite rays, which is perfectly compatible with the drawing condition. The remaining gap is therefore a bending lemma — every polygonal drawing can be redrawn so that no two edges at a vertex are collinear there — and it is genuinely about changing the drawing, not about presentations. Graph.Bendable is that statement in the shape the theorems below consume; nothing here proves it.

A polygonal set is a vertex list between any two of its points

Schoenflies.IsPolygonal is "the carrier of a vertex list", and a vertex list carries a path, so the predicate is not closed under arbitrary finite unions — two disjoint segments are not the carrier of any one list. It is closed under unions that meet, and the way to see that is to move the ends of the list: a list can be made to start and end wherever one likes on its own carrier, by running out and back.

A closed polygon read backwards

A realization of a splitting names its two arcs in a direction, and two realizations of one arc need not agree on it. Reversing the cyclic order is what reconciles them.

def Schoenflies.ClosedPolygon.reverse {m : ℕ} (P : ClosedPolygon m) : ClosedPolygon m

The same closed polygon, traversed the other way.

Equations

• P.reverse = { vertex := fun (j : ZMod (m + 3)) => P.vertex (-j), vertex_inj := ⋯, edges_meet := ⋯, corner := ⋯ }

@[simp]

theorem Schoenflies.ClosedPolygon.reverse_vertex {m : ℕ} (P : ClosedPolygon m) (j : ZMod (m + 3)) : P.reverse.vertex j = P.vertex (-j)

theorem Schoenflies.ClosedPolygon.reverse_edge {m : ℕ} (P : ClosedPolygon m) (j : ZMod (m + 3)) : P.reverse.edge j = P.edge (-j - 1)

@[simp]

theorem Schoenflies.ClosedPolygon.reverse_carrier {m : ℕ} (P : ClosedPolygon m) : P.reverse.carrier = P.carrier

theorem Schoenflies.ClosedPolygon.reverse_natCast {n k t : ℕ} (ht : t < k) : ↑(k - t - 1) + ↑t + 1 = ↑k

The t-th edge of the reversed arc is the k - 1 - t-th of the original: the same edges, listed backwards.

theorem Schoenflies.ClosedPolygon.reverse_arc {m : ℕ} (P : ClosedPolygon m) (a : ZMod (m + 3)) (k : ℕ) : P.reverse.arc (-a - ↑k) k = P.arc a k

Reversing does not move an arc, it only starts it at the other end.

theorem Schoenflies.ClosedPolygon.sameEdges_reverse_arcPieces {m : ℕ} (P : ClosedPolygon m) (a : ZMod (m + 3)) (k : ℕ) : SameEdges (P.reverse.arcPieces (-a - ↑k) k) (P.arcPieces a k)

Reversing does not change the edge list either, up to the order and the naming of each edge's two ends — which is exactly what Schoenflies.SameEdges forgives.

The decomposition of an arc is the arc's own

Graph.IsHexRealization asks for three closed polygons that agree on the arcs they share. They are found independently, and nothing so far says they agree — until this: two closed polygons carrying the same arc, and starting it at the same vertex, run through the same vertices along it. The proof walks the arc: the first edges of the two are two segments leaving one point along one ray, so one contains the other, and the shorter one's far end would be a vertex of its own polygon interior to an edge of the other — which corner forbids.

theorem Schoenflies.ClosedPolygon.natCast_ne_zero_of_lt {m t : ℕ} (ht1 : 0 < t) (ht2 : t < m + 3) : ↑t ≠ 0

A numeral strictly between 0 and the modulus is not 0 in the cyclic index.

theorem Schoenflies.ClosedPolygon.vertex_notMem_edge_natCast {m : ℕ} (P : ClosedPolygon m) (a : ZMod (m + 3)) {t : ℕ} (ht1 : 0 < t) (ht2 : t < m + 2) : P.vertex a ∉ P.edge (a + ↑t)

The first vertex of an arc lies on none of its later edges — a step index below the modulus reaches neither the edge leaving that vertex nor the one arriving at it.

theorem Schoenflies.ClosedPolygon.exists_ball_arc_subset_edge {m : ℕ} (P : ClosedPolygon m) (a : ZMod (m + 3)) (k : ℕ) {w : Plane} (hw : ∀ (t : ℕ), 0 < t → t < k → w ∉ P.edge (a + ↑t)) : ∃ r > 0, Metric.ball w r ∩ P.arc a k ⊆ P.edge a

Around a point that no later edge of the arc reaches, the arc is its first edge alone.

theorem Schoenflies.ClosedPolygon.exists_step_lt {ρ : ℝ} (hρ : 0 < ρ) (u v : Plane) : ∃ (s : ℝ), 0 < s ∧ s ≤ 1 ∧ s * ‖u‖ < ρ ∧ s * ‖v‖ < ρ

Bounds a step along two directions inside one ball.

theorem Schoenflies.ClosedPolygon.exists_pos_smul_of_ball_subset {v₀ v₁ u₁ : Plane} {r : ℝ} (hr : 0 < r) (hv : v₁ ≠ v₀) (hsub : segment ℝ v₀ v₁ ∩ Metric.ball v₀ r ⊆ segment ℝ v₀ u₁) : ∃ (c : ℝ), 0 < c ∧ v₁ - v₀ = c • (u₁ - v₀)

Two segments leaving one point and agreeing near it leave along the same ray.

theorem Schoenflies.ClosedPolygon.notMem_openSegment_first_edge {m m' : ℕ} (P : ClosedPolygon m) (Q : ClosedPolygon m') (a : ZMod (m + 3)) (b : ZMod (m' + 3)) {k l : ℕ} (hk1 : 1 ≤ k) (hk2 : k ≤ m + 2) (hl1 : 1 ≤ l) (harc : P.arc a k = Q.arc b l) (hstart : P.vertex a = Q.vertex b) : Q.vertex (b + 1) ∉ openSegment ℝ (P.vertex a) (P.vertex (a + 1))

A vertex of one polygon is never interior to the other's first edge. Either the shared arc is that single edge — and then the far end of the edge cannot be strictly inside it — or the other polygon has two edges at the vertex, both lying near it inside one straight segment, which is what its corner field forbids.

theorem Schoenflies.ClosedPolygon.natCast_pred_succ {n t : ℕ} (ht : 0 < t) : ↑(t - 1) + 1 = ↑t

Stepping the cyclic index by a positive numeral.

theorem Schoenflies.ClosedPolygon.arc_succ {m : ℕ} (P : ClosedPolygon m) (a : ZMod (m + 3)) {k : ℕ} (hk : 1 ≤ k) : P.arc a k = P.edge a ∪ P.arc (a + 1) (k - 1)

An arc is its first edge together with the arc that leaves the next vertex.

theorem Schoenflies.ClosedPolygon.edge_inter_arc_succ {m : ℕ} (P : ClosedPolygon m) (a : ZMod (m + 3)) {k : ℕ} (hk : k ≤ m + 2) : P.edge a ∩ P.arc (a + 1) (k - 1) ⊆ {P.vertex (a + 1)}

The first edge of an arc meets the rest of it only at the vertex between them.

theorem Schoenflies.ClosedPolygon.arc_one_ne {m m' : ℕ} (P : ClosedPolygon m) (Q : ClosedPolygon m') (a : ZMod (m + 3)) (b : ZMod (m' + 3)) {l : ℕ} (hl : 2 ≤ l) (harc : P.arc a 1 = Q.arc b l) (hedge : P.edge a = Q.edge b) : False

A one-edge arc has no second edge. If the same arc were also presented with two or more edges, its second edge would lie inside its first, which edges_meet forbids.

theorem Schoenflies.ClosedPolygon.arc_vertex_eq (k : ℕ) {m m' : ℕ} (P : ClosedPolygon m) (Q : ClosedPolygon m') (a : ZMod (m + 3)) (b : ZMod (m' + 3)) (l : ℕ) : 1 ≤ k → k ≤ m + 2 → 1 ≤ l → l ≤ m' + 2 → P.arc a k = Q.arc b l → P.vertex a = Q.vertex b → k = l ∧ ∀ t ≤ k, P.vertex (a + ↑t) = Q.vertex (b + ↑t)

Two closed polygons that carry the same arc, starting it at the same vertex, run through the same vertices along it — and in particular use the same number of edges. This is what makes independent realizations of the six-cycle and of the two spliced curves agree.

theorem Schoenflies.ClosedPolygon.arcPieces_eq {m m' : ℕ} (P : ClosedPolygon m) (Q : ClosedPolygon m') (a : ZMod (m + 3)) (b : ZMod (m' + 3)) {k l : ℕ} (hk1 : 1 ≤ k) (hk2 : k ≤ m + 2) (hl1 : 1 ≤ l) (hl2 : l ≤ m' + 2) (harc : P.arc a k = Q.arc b l) (hstart : P.vertex a = Q.vertex b) : P.arcPieces a k = Q.arcPieces b l

Two closed polygons that carry the same arc, starting it at the same vertex, cut it into the same edges.

theorem Schoenflies.exists_closedPolygon_arcs_oriented {C A₁ A₂ : Set Plane} (hJ : IsJordanCurve C) (hP : IsPolygonal C) {p q : Plane} (hp : IsCornerAt C p) (hq : IsCornerAt C q) (hpq : p ≠ q) (hA1 : IsArcBetween A₁ p q) (hA2 : IsArcBetween A₂ p q) (hunion : A₁ ∪ A₂ = C) (hinter : A₁ ∩ A₂ = {p, q}) : ∃ (m : ℕ) (P : ClosedPolygon m) (a : ZMod (m + 3)) (k : ℕ), P.carrier = C ∧ 1 ≤ k ∧ k ≤ m + 2 ∧ P.vertex a = p ∧ P.vertex (a + ↑k) = q ∧ P.arc a k = A₁ ∧ P.arc (a + ↑k) (m + 3 - k) = A₂

The realization of a splitting, with the first arc's direction fixed too. The two arcs of Schoenflies.exists_closedPolygon_arcs_ordered come out in the order they were given, but the polygon may traverse them either way; reading it backwards when it does is what pins the first arc to start at p. Two realizations of one arc can then be compared with Schoenflies.ClosedPolygon.arcPieces_eq.

What the realization needs from the drawing, and nothing else

def Graph.IsHexGeneric {β : Type u_1} (drawing : β → ℝ → Schoenflies.Plane) (e : Fin 3 → Fin 3 → β) (x y : Fin 3 → Schoenflies.Plane) (s : Fin 3) : Prop

General position at the two cut points of the crosscut indexed by s. At each of the two ends x s and y (s + 1) of the remaining edge, the six-cycle turns, and so does each of the two closed curves the remaining edge forms with the two halves of the six-cycle.

This is not a hypothesis chosen for convenience. Schoenflies.ClosedPolygon.isCornerAt_vertex and Schoenflies.ClosedPolygon.exists_vertex_eq_of_isCornerAt together say that the vertex set of a realization is the corner set of the curve; a crosscut cutting C at these two points forces them to be vertices of all three closed polygons, hence corners of all three curves. For a drawn K(3,3) it says that at each of the six vertices no two of the three edges leave along one line.

Equations

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

theorem Graph.IsK33Config.isPolygonal_arcA {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) (hpoly : ∀ f ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing f)) (s : Fin 3) : Schoenflies.IsPolygonal (edgesCover drawing (arcA e s))

The first half of the six-cycle is polygonal: it is drawn by a path.

theorem Graph.IsK33Config.isPolygonal_arcB {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) (hpoly : ∀ f ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing f)) (s : Fin 3) : Schoenflies.IsPolygonal (edgesCover drawing (arcB e s))

The second half of the six-cycle is polygonal.

theorem Graph.IsK33Config.isPolygonal_hexSet {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) (hpoly : ∀ f ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing f)) : Schoenflies.IsPolygonal (hexSet drawing e)

The six-cycle of a polygonally drawn K(3,3) is polygonal: it is the union of its two halves, which meet.

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

A remaining edge meets the first half of the six-cycle exactly in its own two ends.

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

A remaining edge meets the second half of the six-cycle exactly in its own two ends.

theorem Graph.IsK33Config.isHexRealization {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} {s : Fin 3} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) (hpoly : ∀ f ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing f)) (hgen : IsHexGeneric drawing e x y s) : IsHexRealization drawing e s

Graph.IsHexRealization, discharged. The six-cycle and the two curves the remaining edge forms with its halves are three polygonal Jordan curves, so Schoenflies.exists_closedPolygon_arcs_oriented presents each of them as a closed polygon whose two arcs are the two given halves, both read from x s to y (s+1).

The three presentations are found independently, and what makes them fit together is Schoenflies.ClosedPolygon.arcPieces_eq: two closed polygons carrying one arc from one vertex cut it into the same edges. So the six-cycle's presentation and the first spliced curve's agree on the first half, the six-cycle's and the second spliced curve's agree on the second half, and the two spliced curves agree on the remaining edge — the last only after reversing one of them, since a crosscut is traversed one way in each of the two curves it bounds.

lem:k33 and cor:k33-subdivision, with the realization gone

What is left as a hypothesis is a bending step, and only that: every polygonal drawing can be redrawn so that no two edges at a vertex leave it along one line.

theorem Graph.IsK33Config.false_of_hexGeneric {β : Type u_1} {G : Graph Schoenflies.Plane β} {drawing : β → ℝ → Schoenflies.Plane} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} (h : G.IsK33Config x y e) (hd : G.IsDrawing drawing) (hpoly : ∀ f ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc drawing f)) (hgen : ∀ (s : Fin 3), IsHexGeneric drawing e x y s) : False

lem:k33 for a polygonal drawing in general position.

theorem Graph.IsK33Config.not_isDrawing_of_bendable {β : Type u_1} {G : Graph Schoenflies.Plane β} {x y : Fin 3 → Schoenflies.Plane} {e : Fin 3 → Fin 3 → β} [G.Finite] (h : G.IsK33Config x y e) (hbend : ∀ (dr : β → ℝ → Schoenflies.Plane), G.IsDrawing dr → (∀ f ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc dr f)) → ∃ (dr' : β → ℝ → Schoenflies.Plane), G.IsDrawing dr' ∧ (∀ f ∈ G.edgeSet, Schoenflies.IsPolygonal (edgeArc dr' f)) ∧ ∀ (s : Fin 3), IsHexGeneric dr' e x y s) : ¬∃ (dr : β → ℝ → Schoenflies.Plane), G.IsDrawing dr

Lemma 3.10 (nonplanarity of K(3,3)), with only the bending step assumed. A graph carrying a copy of K(3,3) has no plane drawing, provided a polygonal drawing can be bent into general position at the six vertices.

@[reducible, inline]

abbrev Graph.Bendable (x y : Fin 3 → Schoenflies.Plane) : Prop

The bending step, for the abstract K(3,3) on six named points of the plane: every polygonal drawing of it can be redrawn, polygonally, so that at each of the six vertices no two of the three edges leave along one line. This is the one thing left unproved; see "What is still assumed" in the module docstring.

Equations

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

theorem Graph.IsArcK33.false_of_bendable {x y : Fin 3 → Schoenflies.Plane} {P : Fin 3 → Fin 3 → Set Schoenflies.Plane} (h : IsArcK33 x y P) (hbend : Bendable x y) : False

lem:k33 for nine arcs: no nine arcs in the plane meet only where a K(3,3) forces them to, assuming Graph.Bendable.

theorem Graph.IsK33Subdivision.false_of_bendable {β : Type u_1} {drawing : β → ℝ → Schoenflies.Plane} {x y : Fin 3 → Schoenflies.Plane} {H : Graph Schoenflies.Plane β} {W : Fin 3 → Fin 3 → List β} (hd : H.IsDrawing drawing) (h : H.IsK33Subdivision x y W) (hbend : Bendable x y) : False

Corollary 3.11 (subdivisions of K(3,3)). No subdivision of K(3,3) has a plane drawing, assuming Graph.Bendable, and only for the contracted graph k33Graph x y, whose nine edges are the branch paths.

theorem Graph.k33Graph_not_isDrawing (x y : Fin 3 → Schoenflies.Plane) (hx : Function.Injective x) (hy : Function.Injective y) (hxy : ∀ (i j : Fin 3), x i ≠ y j) (hbend : Bendable x y) : ¬∃ (dr : Fin 3 × Fin 3 → ℝ → Schoenflies.Plane), (k33Graph x y).IsDrawing dr

The headline: K(3,3) has no plane drawing. Stated for the concrete graph Graph.k33Graph x y, whose nine edges are the index pairs. Assuming Graph.Bendable, the one hypothesis this module leaves standing.