lem:k33 and cor:k33-subdivision, with nothing assumed #
Schoenflies/Graph/K33Planar.lean proves the nonplanarity of K(3,3) from
Graph.IsHexRealization; Schoenflies/Graph/K33Closed.lean reduces that to Graph.Bendable —
"every polygonal drawing can be redrawn so that no two edges leave a vertex along one line". This
module removes the hypothesis altogether. Nothing is bent.
Where the hypothesis came from, and why it is not needed #
Schoenflies.ClosedPolygon carries a corner field, and
Schoenflies.ClosedPolygon.isCornerAt_vertex shows the field is not slack: every vertex of
every ClosedPolygon presentation is a point at which the curve turns. So a crosscut interface
phrased with ClosedPolygons — Schoenflies.IsPolygonalCrosscut, and hence
Schoenflies.alternating_crosscuts — can only cut the curve at corners, and a drawn K(3,3) puts
its branch points wherever it likes.
The blueprint's cor:alternating-crosscuts has no such condition: it is stated for a set-level
simple closed polygonal curve and simple polygonal arcs with endpoints anywhere on it. The fix is
to state the crosscut for Schoenflies.PrePolygon — ClosedPolygon without corner — whose
vertices may sit anywhere on the curve. Schoenflies/PrePolygonSep.lean already supplies the two
things Theorem 2.8 asks of such a curve: that its carrier separates the plane, and the two values
of the crossing parity. Everything else in the chain is about edge lists, and edge lists do not
know about corners.
The one construction this needed #
Three closed polygons enter Theorem 2.8 — the curve C and the two curves Jᵢ the crosscut
forms with the two arcs — and their edge lists must agree: SameEdges Jᵢ.pieces (Aᵢ ++ K).
Schoenflies/Graph/K33Closed.lean found three realizations independently and matched them with
Schoenflies.ClosedPolygon.arcPieces_eq, whose proof is exactly where corner was consumed. For
PrePolygon no such matching theorem can exist: two presentations of one arc need not agree.
So the two spliced curves are not found — they are built. Schoenflies.PrePolygon.exists_splice
lays two chains with common ends end to end and returns a PrePolygon whose edge list is their
concatenation, so the three lists agree by construction and nothing has to be matched. The chains
themselves come from Schoenflies.exists_prePolygon_arcs_oriented, which needs
Schoenflies.PrePolygon.insertLast of Schoenflies/PrePolygonArc.lean: a point of the curve that
is not yet a vertex is interior to an edge, and an edge may be cut. That is the inverse of
Schoenflies.PrePolygon.deleteLast, and it is what makes "a PrePolygon may be presented with
vertices at any prescribed finite set of points of its carrier" a theorem
(Schoenflies.PrePolygon.exists_prePolygon_vertices).
What this module rests on #
The Schoenflies.PrePolygon arc apparatus — chain, arcPieces, arc, arc_inter,
isArcBetween_arc, parity_splitting, parity_ne_iff_mem_farRegion, insertLast,
exists_prePolygon_vertices, Schoenflies.exists_prePolygon_split and the segment-cutting
lemmas — is in Schoenflies/PrePolygonArc.lean, shared with Schoenflies/FaceCyclesLand.lean.
Only what is peculiar to the crosscut wiring is left here.
Blueprint #
Schoenflies.PrePolygon.exists_splice— two arcs with common ends, laid end to end.Schoenflies.PrePolygon.reverse,…reverse_arc,…sameEdges_reverse_arcPieces— the polygon traversed the other way, which is what pins the direction of a prescribed arc.Schoenflies.exists_prePolygon_arcs,…exists_prePolygon_arcs_oriented— §1, the realization theorem with the cut points anywhere on the curve, tracking a prescribed splitting. CompareSchoenflies.exists_closedPolygon_arcs, which requires the cut points to be corners.Schoenflies.IsPrePolygonalCrosscutand its API up to…alternating_inter_nonempty_of_same_side—thm:polygonal-crosscutandcor:alternating-crosscutsin the blueprint's own generality: the split points need not be corners.Graph.IsPreHexCrosscut,Graph.IsK33Config.isPreHexCrosscut— the six-cycle of a polygonally drawnK(3,3), cut at the two ends of one remaining edge, as such a crosscut. This is whatGraph.IsHexRealizationwas assuming, and it is proved here.Graph.IsK33Config.false_of_isPreHexCrosscut,…false_of_polygonal,Graph.IsK33Config.not_exists_isDrawing—lem:k33.Graph.IsArcK33.elim,Graph.IsK33Subdivision.elim—cor:k33-subdivision.Graph.k33Graph_not_exists_isDrawing—lem:k33for the concrete graph.
A note on names, for the integrator #
The direct statements use eliminator-style names because the realization-parametric lemmas are still in the import closure:
With this module in place Graph.IsHexRealization, Graph.IsHexCrosscut, Graph.IsHexGeneric
and Graph.Bendable have no consumers left.
Splicing two chains into a closed polygon #
The crosscut of Theorem 2.8 asks for three closed polygons whose edge lists fit together, and
independent realizations of three curves do not. The way out is to realize only the curve C,
and to build the two spliced curves out of one arc of C and one presentation of the crosscut —
so that the three edge lists agree by construction. This is that construction: two chains with
the same pair of ends, meeting only there, laid end to end.
Two arcs with common ends splice into a closed polygon whose edge list is their
concatenation. P.arcPieces a k runs from p to q and P'.arcPieces b l runs from q back
to p; the two meet only at p and q.
The polygon read backwards #
Needed only to pin the direction in which a realization traverses a prescribed arc; the
Schoenflies.ClosedPolygon version is in Schoenflies/Graph/K33Closed.lean, and this is the
same construction with the corner field dropped.
The same closed polygon, traversed the other way.
Equations
Instances For
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 realization theorem, tracking a prescribed splitting #
Schoenflies.exists_prePolygon_split of Schoenflies/PrePolygonArc.lean presents the curve with
the two cut points among its vertices, with no corner condition on them. What remains is to say
which arc of that presentation is which of two prescribed arcs, and in which direction the
first is traversed.
The realization theorem, tracking a splitting into two named arcs.
The realization of a splitting, with both the arcs and the direction fixed. The two arcs
come out in the order they were given and the first is traversed from p to q; reading the
polygon backwards when it is not is what pins the direction.
This is the shape the crosscut wiring consumes, and — unlike
Schoenflies.exists_closedPolygon_arcs_oriented — it asks nothing of p and q beyond lying on
the curve.
Theorem 2.8 and Corollary 2.9 for a polygon presented with redundant vertices #
Schoenflies.IsPolygonalCrosscut is stated for ClosedPolygons, and by
Schoenflies.ClosedPolygon.isCornerAt_vertex that pins the two cut points to be corners of the
curve. Nothing in the proof of Theorem 2.8 needs the corner field: what it uses of C, J₁,
J₂ is that their carriers separate the plane and that their crossing counts are the ones the
edge lists compute. Schoenflies/PrePolygonSep.lean supplies both for a PrePolygon, so the
whole chain goes through with the cut points anywhere on the curve.
The setting of Theorem 2.8, with the cut points unrestricted. Word for word
Schoenflies.IsPolygonalCrosscut, with PrePolygon for ClosedPolygon.
The first arc runs forward through at most a full turn.
J₁carries the edges of the first arc together with those of the crosscut.J₂carries the edges of the second arc together with those of the crosscut.The crosscut meets the polygon only in points of the first arc …
… and only in points of the second arc.
- notMem : y ∉ C.carrier
The reference point lies off the polygon …
- avoids : Disjoint (cover K) (connectedComponentIn C.carrierᶜ y)
… and the crosscut does not enter its region.
Instances For
The front door. A crosscut is normally presented by saying that it meets C exactly in
its two endpoints, and that those endpoints are the two cut vertices.
The two arcs may be swapped.
The elementary consequences #
The edges of the crosscut are nondegenerate, because they are edges of J₁.
A ray direction transverse to every edge of C and of the crosscut at once.
The two cells #
The untouched region of ℝ² ∖ C lies in one region of ℝ² ∖ J₁, namely the one of y.
Lemma 2.6(a), first half: the cell lies in Ω ∖ P.
Lemma 2.6(a): the cell is a connected component of Ω ∖ P.
Lemma 2.6(c): the closure of the cell meets the polygon exactly in its arc.
Exhaustion: the crossing counts add up #
A point off C ∪ P is separated from y by C exactly when it is separated from y by
exactly one of J₁, J₂.
Theorem 2.8, the two cells.
Corollary 2.9 #
The region the crosscut enters is the component of any of its points off C.
Corollary 2.9, core form.
Corollary 2.9 for a second crosscut presented as a simple arc.
Corollary 2.9 in the shape a plane-graph argument produces it.
Corollary 2.9 with "the same side" read as "the same connected component".
The six-cycle and one remaining edge, as a crosscut #
Graph.IsHexCrosscut of Schoenflies/Graph/K33Planar.lean is the same statement with
Schoenflies.ClosedPolygon for Schoenflies.PrePolygon; the change is what removes the corner
condition on the two cut points, which is the whole of the remaining gap.
The six-cycle and one remaining edge, realized as a polygonal crosscut, with the two cut points wherever the drawing put them.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The crosscut exists for any polygonal drawing. The six-cycle is
realized as a Schoenflies.PrePolygon cut at the two ends of the remaining edge — possible
because a PrePolygon may have a vertex wherever one likes — and the two closed curves the
remaining edge forms with the two halves are then built from that realization and from one
presentation of the remaining edge, rather than found independently. That is what makes the three
edge lists agree, and it is why no matching lemma, and hence no general position, is needed.
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, so cor:alternating-crosscuts makes them meet; but distinct
edges of a plane graph meet only at shared vertices, and these two share none.
lem:k33 for a drawing that is already polygonal, with nothing assumed.
Lemma 3.10 (nonplanarity of K(3,3)), with no hypothesis left. 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; the contradiction is then false_of_polygonal. This is
Graph.IsK33Config.not_isDrawing of Schoenflies/Graph/K33Planar.lean with its realization
hypothesis discharged, and Graph.IsK33Config.not_isDrawing_of_bendable of
Schoenflies/Graph/K33Closed.lean with Graph.Bendable discharged: no drawing has to be bent,
because the crosscut no longer needs the six vertices to be corners.
lem:k33 for nine arcs: no nine arcs in the plane meet only where a
K(3,3) forces them to.
Corollary 3.11 (subdivisions of K(3,3)). No subdivision of K(3,3)
has a plane drawing.
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, with nothing assumed beyond the six
points being six distinct points of the plane.