`lem:face-cycles`, with nothing assumed #

Schoenflies/FaceCyclesProof.lean proves lem:face-cycles modulo one hypothesis, Schoenflies.CrosscutSplitsRegion: the exhaustion clause of thm:polygonal-crosscut for a crosscut whose two endpoints are arbitrary points of the curve. This module proves that hypothesis and restates the lemma without it (Graph.face_cycles', Graph.IsDrawing.hasFaceCycles_union').

Why the crosscut theorem had to be redone, and how far #

main's Theorem 2.8 (Schoenflies.IsPolygonalCrosscut) cuts a ClosedPolygon at two of its vertices, and Schoenflies.ClosedPolygon.isCornerAt_vertex says a point at which the curve runs straight is a vertex of no ClosedPolygon presentation of it. In the ear induction the two cut points are graph vertices, at which the two cycle edges may leave along opposite rays. So the presentation has to be Schoenflies.PrePolygon, which has no corner field, and the two main hypotheses edges₁/edges₂ — multiset equalities SameEdges Jᵢ.pieces (Aᵢ ++ K) — have to go as well, for the reason Schoenflies/FaceCyclesProof.lean records: the merged curve Aᵢ ∪ P may run straight through a cut point, and then no presentation of it has an edge ending there.

Both go away at once by never realizing J₁ and J₂ at all. The two curves of the split are given by literal edge lists Aᵢ ++ K, so Lemma 2.7 (Schoenflies.parity_split) applies with nothing to check, and only the easy half of Theorem 2.3 is asked of them: "points in the same region have the same crossing count", which is Lemma 2.2 (Schoenflies.parity_eq_of_mem_connectedComponentIn) and needs no realization. The hard half — the two values 0 and 1 — is needed for J alone, where Schoenflies.PrePolygon.parity_eq_one_iff of Schoenflies/PrePolygonSep.lean supplies it. That is the whole of the reduction; Lemma 2.6 (Schoenflies.crosscut_cells) is already stated at the set level and is quoted unchanged.

What the presentation still has to do is put the two cut points on its vertex list, and that is Schoenflies.PrePolygon.insertLast of Schoenflies/PrePolygonArc.lean, the inverse of Schoenflies.PrePolygon.deleteLast. A point interior to an edge is brought to the last edge by Schoenflies.PrePolygon.rotate and the edge is split in two; simplicity survives because the far end of the split edge lies on neither half.

For the integrator #

The Schoenflies.PrePolygon arc apparatus this module runs on — Schoenflies.PrePolygon.arcPieces, …arc, …arcList, …insertLast and Schoenflies.exists_prePolygon_split — lives in Schoenflies/PrePolygonArc.lean, shared with Schoenflies/Graph/K33Land.lean. It is Schoenflies.ClosedPolygon.arcPieces and its API of Schoenflies/ParitySplitting.lean and Schoenflies/Realization.lean transcribed with the structure changed — the proofs use vertex_inj and edges_meet and nothing else. The right arrangement, as Schoenflies/PrePolygonSep.lean already says of pieces, is to prove them once for PrePolygon and define the ClosedPolygon versions as P.toPre.arcPieces; that needs PrePolygon moved up beside ClosedPolygon in Schoenflies/Strip.lean.

Three declarations here are general and belong elsewhere: Schoenflies.isSeparating_of_isJordanCurve in Schoenflies/Realization.lean, Schoenflies.IsArcBetween.ne in Schoenflies/Curve.lean, and Schoenflies.isChainFrom_segsOf in Schoenflies/ParitySplitting.lean beside Schoenflies.isChainFrom_pathPieces. Schoenflies.two_arcs_unique_of_isClosed subsumes Schoenflies.two_arcs_unique and should replace it in Schoenflies/Realization.lean.

Once this module is moved above Schoenflies/FaceCyclesProof.lean, the hypothesis Schoenflies.CrosscutSplitsRegion can be deleted from Graph.face_cycles and Graph.IsDrawing.hasFaceCycles_union, and the two primed statements at the end here dropped.

Blueprint #

Schoenflies.two_arcs_unique_of_isClosed — the two arcs a pair of points cuts a curve into are determined, with the competing splitting known only to be closed and nondegenerate.
Schoenflies.crosscutSplitsRegion — the exhaustion clause of thm:polygonal-crosscut at arbitrary cut points: Schoenflies.CrosscutSplitsRegion, proved.
Graph.IsDrawing.hasFaceCycles_union' — one ear of lem:face-cycles.
Graph.face_cycles' — lem:face-cycles.
Graph.IsFaceCycle.eq_inside_of_isBounded' — "in particular, every bounded face is the interior of its boundary cycle".

Small pieces the assembly needs #

source

theorem Schoenflies.isSeparating_of_isJordanCurve {S : Set Plane} (hJ : IsJordanCurve S) (hP : IsPolygonal S) :

IsSeparating S

A polygonal Jordan curve separates the plane (Theorem 2.3, at the set level): realize it and quote Schoenflies.ClosedPolygon.isSeparating_carrier.

source

theorem Schoenflies.isChainFrom_segsOf (vs : List Plane) (h : vs ≠ []) :

IsChainFrom (segsOf vs) (vs.head h) (vs.getLast h)

A polyline is a chain from its first point to its last, with its degenerate steps dropped. Schoenflies.isChainFrom_pathPieces says this for Schoenflies.pathPieces, which keeps them; Schoenflies.segsOf is the list a consumer needing nondegenerate edges must use.

source

theorem Schoenflies.two_arcs_unique_of_isClosed {C A₁ A₂ D₁ D₂ : Set Plane} {p q : Plane} (hA : A₁ ∪ A₂ = C) (hAi : A₁ ∩ A₂ = {p, q}) (hD : D₁ ∪ D₂ = C) (hDi : D₁ ∩ D₂ = {p, q}) (hA1 : IsArcBetween A₁ p q) (hA2 : IsArcBetween A₂ p q) (hc1 : IsClosed D₁) (hc2 : IsClosed D₂) (hn1 : ¬D₁ ⊆ {p, q}) (hn2 : ¬D₂ ⊆ {p, q}) :

A₁ = D₁ ∧ A₂ = D₂ ∨ A₁ = D₂ ∧ A₂ = D₁

The two-arc decomposition is determined, and the competitor need not be known to be two arcs. This is Schoenflies.two_arcs_unique with the hypotheses on the second splitting weakened to what its proof uses: the two sets are closed and neither is just the two cut points. The edge lists of a polygon supply exactly that, and nothing tells us they are arcs until this lemma has said so.

Theorem 2.8 at arbitrary cut points #

The blueprint's Theorem 2.8 is proved on main for a crosscut cutting a ClosedPolygon at two of its vertices; Schoenflies.ClosedPolygon.isCornerAt_vertex makes that a real restriction, since a point where the curve runs straight is a vertex of no ClosedPolygon presentation. The exhaustion clause is what a consumer splitting a face at two graph vertices needs, and here it is proved with no condition on the two points beyond lying on the curve.

The route is the blueprint's, with PrePolygon in place of ClosedPolygon and with the two Schoenflies.SameEdges hypotheses of Schoenflies.IsPolygonalCrosscut replaced by literal edge lists: the two curves of the split are presented as Aᵢ ++ K, so Lemma 2.7 (Schoenflies.parity_split) applies with nothing to check. Only one direction of Theorem 2.3 is needed for those two lists — "the same region forces the same count", which is Lemma 2.2 and asks for no realization at all. The other direction is needed only for the curve C itself, and there Schoenflies.PrePolygon.parity_eq_one_iff supplies it.

source

theorem Schoenflies.crosscutSplitsRegion :

CrosscutSplitsRegion

The exhaustion clause of the polygonal crosscut theorem, at arbitrary cut points. This is Schoenflies.CrosscutSplitsRegion, the hypothesis Schoenflies/FaceCyclesProof.lean was left with.