Lemma 3.10: the utility graph is not planar, and Corollary 3.11 for its subdivisions #
Schoenflies/Graph/K33.lean built the whole configuration: the six-cycle of a drawn K(3,3)
is a Jordan curve, each of the three remaining edges is a crosscut of it, two of the three lie
on the same side, their endpoints alternate, and any two of them are disjoint. This module
wires those five facts to Schoenflies.alternating_crosscuts and derives the contradiction; it
then does the blueprint's reduction of cor:k33-subdivision to lem:k33.
One hypothesis is assumed and not proved: Graph.IsHexRealization. See "The gap" below.
The remaining results use only the hypotheses in their statements.
Blueprint #
Graph.IsHexCrosscut— the six-cycle, together with one of the three remaining edges, in the vocabularySchoenflies.IsPolygonalCrosscutspeaks: aSchoenflies.ClosedPolygon, its two arcs, the crosscut, and a reference point.Graph.IsK33Config.endpoints_subset_arcA,…_arcB,…exists_reference_point,…isHexCrosscut— the four topological clauses ofSchoenflies.IsPolygonalCrosscut, discharged from the drawing, so that only the combinatorial realization has to be assumed.Graph.IsHexRealization— that combinatorial realization, and the one thing assumed here.Graph.IsK33Config.exists_two_chords_same_region—lem:k33, "two of the three lie on the same side", with the side named as a region of the complement rather than as one of a pair of open sets, which is the form the crosscut corollary consumes.Graph.IsK33Config.false_of_isHexCrosscut— the contradiction at a fixed pair of remaining edges:cor:alternating-crosscutsmakes them meet,chords_disjointsays they do not.Graph.IsK33Config.false_of_hexCrosscuts,…false_of_hexRealizations—lem:k33for a drawing that is already polygonal.Graph.IsK33Config.not_isDrawing—lem:k33: a graph carrying a copy ofK(3,3)has no plane drawing at all.lem:polygonal-redrawingreduces the general drawing to a polygonal one, which is the only place polygonality is used.Graph.IsArcK33,Graph.k33Graph,Graph.IsArcK33.arcDrawing,…isDrawing,…isK33Config,…false_of_realization—cor:k33-subdivision, first half: nine arcs in the plane meeting only where aK(3,3)forces them to already are a plane drawing ofK(3,3), on an abstract graph built here for the purpose.Graph.IsK33Subdivision,…isArcK33,…false_of_realization—cor:k33-subdivision: in a plane drawing of a subdivision, the branch paths draw nine such arcs.
The gap: realizing the six-cycle as a ClosedPolygon #
Every statement of Schoenflies/PolygonalJordan.lean, Schoenflies/PolygonalCrosscut.lean and
Schoenflies/AlternatingCrosscuts.lean is about a Schoenflies.ClosedPolygon m — a cyclic
vertex list with vertex_inj, edges_meet and corner. The six-cycle of a polygonally
drawn K(3,3) is a polygonal Jordan curve as a point set, and nothing in the development
turns a point set into a ClosedPolygon: there is no declaration anywhere whose conclusion is
∃ m (C : ClosedPolygon m), C.carrier = _. The only closed polygons that exist are the
hand-built Schoenflies.triangle and Schoenflies.unitTriangle.
IsHexRealization is exactly that missing step, stated for the one curve this argument needs
it for and pared down to its combinatorial core: four closed polygons and four equations
identifying their carriers and edge lists with the drawing. No topological side condition
survives in it — the reference point of Theorem 2.8 and the three "meets" clauses are proved
here from the drawing. It is not proved here, and every theorem below that mentions it is
therefore requires that realization as a hypothesis.
Why the realization is allowed to change the drawing. IsHexRealization asks for
C.arc a k = arcA e s, which pins the two ends of that arc — the vertices x s and
y (s+1) — to be vertices of C. A Schoenflies.ClosedPolygon has no straight vertices
(its corner field), so this is possible only if the six-cycle actually turns at x s and at
y (s+1). A polygonal drawing need not do that: two of the three polygonal edges at a vertex
may leave it in exactly opposite directions, and then no closed polygon with that carrier has
that point as a vertex. A realization must therefore be free to bend the drawing at the six
vertices first, and Graph.IsK33Config.not_isDrawing gives it that freedom: it hands the
realization a polygonal drawing and accepts any drawing back. This restriction comes from
Schoenflies.IsPolygonalCrosscut, not from anything here; the alternative is a crosscut
interface that lets the two cut points be interior to edges of C.
The missing realization, isolated #
The six-cycle of a polygonally drawn K(3,3), cut by the remaining edge e s (s+1), presented
in the vocabulary of Schoenflies.IsPolygonalCrosscut: a ClosedPolygon whose carrier is the
six-cycle, whose two arcs from the cut are the two halves arcA e s and arcB e s, and whose
crosscut occupies exactly the remaining edge's arc.
The six-cycle and one remaining edge, realized as a polygonal crosscut. C is the
six-cycle as a Schoenflies.ClosedPolygon, cut at the vertices a and a + k — which are the
two ends x s and y (s+1) of the remaining edge indexed by s — into the two arcs
arcA e s and arcB e s; K is the remaining edge, and J₁, J₂ the two closed polygons it
forms with the two arcs.
This is the only thing the argument below assumes, and it is exactly what a bridge from
polygonal Jordan curves to Schoenflies.ClosedPolygon would supply.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The six-cycle separates the plane: it is the carrier of a closed polygon, and
thm:polygonal-jordan applies to that.
The alternation, with the two arcs named #
Graph.IsK33Config.chords_alternate returns the two arcs existentially. The crosscut corollary
has to be handed those particular sets, since the realization has to reproduce them, so the
two membership clauses are restated here with the arcs written out.
The near end of the next remaining edge is interior to the first arc.
The far end of the next remaining edge is interior to the second arc.
Two of the three remaining edges lie in one region #
A remaining edge's interior lies inside the edge's arc.
Two of the three remaining edges lie in one and the same region of the complement of the
six-cycle. This is Graph.IsK33Config.exists_two_chords_same_side with the two sides read as
the two regions Int and Ext of the polygonal Jordan curve theorem, which is the form the
crosscut corollary consumes.
The topological side conditions of the crosscut, discharged #
Schoenflies.IsPolygonalCrosscut asks for four things beyond the edge lists: that the crosscut
meets the polygon only in points of each arc, and a reference point off the polygon in the
region the crosscut does not enter. All four are properties of the drawing, and are proved
here, so that what has to be assumed from outside is only the combinatorial realization
(Graph.IsHexRealization).
The two ends of the remaining edge lie on the first arc of the cut.
The two ends of the remaining edge lie on the second arc of the cut.
The reference point of Theorem 2.8, for a remaining edge. The interior of the remaining edge lies in one region of the complement of the six-cycle; any point of the other region is a legitimate reference point, and the other region is nonempty because it is a region.
What must still be assumed: the combinatorial realization #
Everything above is proved. What is not is that the six-cycle, its two arcs, and the two closed
curves the remaining edge forms with them are closed polygons at all — that a polygonal Jordan
curve given as a point set carries a cyclic vertex list. IsHexRealization says exactly that,
and nothing more: no reference point, no meeting condition, only the four ClosedPolygons and
the four equations identifying their carriers and edge lists with the drawing.
The six-cycle and one remaining edge, realized combinatorially. The six-cycle is a
Schoenflies.ClosedPolygon C whose two arcs from the cut at a, a + k are the two halves
arcA e s, arcB e s of the six-cycle; the remaining edge occupies the segments K; and the
two closed curves it forms with the two arcs are closed polygons J₁, J₂ carrying exactly
those segments.
This is the one thing this module assumes and does not prove. See "The gap" in the module docstring.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The realization is enough. The four topological clauses of
Schoenflies.IsPolygonalCrosscut come from the drawing: the remaining edge meets the six-cycle
exactly in its own two ends (chord_inter_hexSet), which lie on both arcs, and the reference
point is exists_reference_point.
The contradiction #
The two remaining edges indexed by s and s + 1 cannot lie in one region. Their four
ends alternate around the six-cycle (chords_alternate), so cor:alternating-crosscuts makes
them meet; but distinct edges of a plane graph meet only at shared vertices, and these two share
none (chords_disjoint).
lem:k33 for a drawing that is already polygonal. Three remaining edges, two sides:
two of them lie in one region (exists_two_chords_same_region); every pair of remaining edges
is indexed by s and s + 1 for some s, so false_of_isHexCrosscut applies.
lem:k33 for a polygonal drawing, from the combinatorial realization alone.
Lemma 3.10 (nonplanarity of K(3,3)). A finite graph carrying a copy of K(3,3) has no
plane drawing.
lem:polygonal-redrawing replaces an arbitrary drawing by a polygonal one on the same graph and
the same vertices, which is the only use polygonality is put to; the contradiction itself is
false_of_hexRealizations. The realization hypothesis is therefore consulted only about
drawings that are already polygonal — and it is allowed to change the drawing again, which it
must be: see "The gap" in the module docstring.
Corollary 3.11: no subdivision of K(3,3) has a plane drawing #
The blueprint's proof replaces each branch path of a subdivision by the simple arc it draws and
then treats that arc as a single edge. Both halves are done here, in that order: first the
abstract statement that nine arcs meeting only where they must already carry a drawn
K(3,3) (Graph.IsArcK33), then the reduction of a drawn subdivision to nine such arcs.
Nine arcs in the plane, meeting only where they must. This is what a plane drawing of a
subdivision of K(3,3) leaves once each branch path has been replaced by the arc it draws: six
distinct points, and for each pair (i, j) an arc from x i to y j, with two distinct arcs
meeting only in a point that is an endpoint of both.
Nothing here mentions a graph. The abstract K(3,3) that carries these arcs is built below.
- arc (i j : Fin 3) : Schoenflies.IsArcBetween (P i j) (x i) (y j)
- x_injective : Function.Injective x
The three points of the first side are distinct.
- y_injective : Function.Injective y
The three points of the second side are distinct.
The two sides are disjoint.
Two distinct arcs meet only in a common endpoint.
Instances For
An endpoint of an edge of the abstract K(3,3) is incident with it.
The nine arcs, parametrized: a drawing of k33Graph. The parametrizations are the ones the
arcs come with, so the point set of an edge is the arc it was built from
(IsArcK33.edgeArc_eq).
Equations
- h.arcDrawing p = Exists.choose ⋯
Instances For
An arc carries none of the six points except its own two ends: a third point x k lies on
the arc P k l for every l, and two distinct arcs meet only in a common end.
The nine arcs draw the abstract K(3,3) in the plane.
The nine arcs carry a copy of K(3,3), on the graph they draw.
lem:k33 for nine arcs: no nine arcs in the plane meet only where a K(3,3) forces
them to. This assumes the realization, exactly as Graph.IsK33Config.not_isDrawing does.
From a drawn subdivision to nine arcs #
A subdivision of K(3,3) inside a graph. Six distinct branch vertices and nine branch
paths, the (i, j)-th running from x i to y j; distinct branch paths share no edge and meet
only in vertices that are branch vertices of both.
Both clauses are combinatorial: no drawing appears. That distinct branch paths meet only in common branch vertices is the blueprint's own phrasing of what a subdivision is.
- x_injective : Function.Injective x
The three branch vertices of the first side are distinct.
- y_injective : Function.Injective y
The three branch vertices of the second side are distinct.
The two sides are disjoint.
Distinct branch paths share no edge.
- vertex_meet (i j k l : Fin 3) : (i, j) ≠ (k, l) → ∀ v ∈ H.walkVertices (x i) (W i j), v ∈ H.walkVertices (x k) (W k l) → v ∈ {x i, y j} ∩ {x k, y l}
Distinct branch paths meet only in vertices that are branch vertices of both.
Instances For
A branch path has at least one edge: an empty one would identify its two ends.
The branch paths of a drawn subdivision are nine arcs meeting only where they must. A point on two branch paths lies on an edge of each; the two edges are distinct, so a plane drawing puts the point at a vertex incident with both, and a vertex on two branch paths is a branch vertex of both.
Corollary 3.11 (subdivisions of K(3,3)). No subdivision of K(3,3) has a plane
drawing. This assumes the realization, exactly as Graph.IsK33Config.not_isDrawing does, and
the realization is needed only for the contracted graph k33Graph x y, whose nine edges are
the branch paths.