Separation and crossing parity before normalization

Schoenflies.ClosedPolygon carries a corner field — no three consecutive vertices collinear — and Schoenflies.ClosedPolygon.isCornerAt_vertex shows that field is not slack: a point at which the curve runs straight is a vertex of no ClosedPolygon presentation of it. So a consumer that must present a curve with vertices at prescribed points cannot use ClosedPolygon at all, and the plane-graph arguments are exactly such consumers: the branch points of a drawing land wherever the drawing puts them.

Schoenflies.PrePolygon is the presentation without that field, and vertices may be put anywhere. This module gives it everything the crosscut chain asks of a simple closed polygon: an edge list for the crossing count, the curve statements, the polygonal Jordan curve theorem, and the two parity values.

Everything transports across normalization, except the parity

Schoenflies.PrePolygon.exists_closedPolygon_of_prePolygon deletes redundant vertices and returns a genuine ClosedPolygon with the same carrier. Any property of the carrier as a set is therefore free: isJordanCurve_carrier, isPolygonal_carrier and isSeparating_carrier below are each three lines, and none of them needs a word about vertices.

The crossing parity is not a property of the carrier. It is computed from a list of edges, and normalization changes that list: it merges collinear edges, so P.pieces is a subdivision of the normalized polygon's. Lemma 2.1 (Schoenflies.parity_subdivide) says subdivision does not change the parity, which is why one expects the parity to transport — but the normalization theorem is an existence statement and keeps no record of which points were deleted, so there is no subdivision in hand to feed it. See the note at the end of this docstring.

The parity is therefore re-derived here, and the derivation turns out not to need the collar at all. Once the curve is known to separate, the two values are forced:

• far along the ray direction the count is zero, and the half-plane where it is zero is convex and unbounded, hence lies in the unbounded region — so π_C = 0 on the outside;
• across an interior point of any one edge the count jumps by one (Lemma 2.2), and the two test points lie off the curve, so they lie in different regions — so the other region carries 1.

Both steps are stated for an arbitrary closed chain whose cover separates the plane (Schoenflies.parity_eq_zero_of_mem_outside_cover, …parity_eq_one_of_mem_inside_cover); the PrePolygon statements are instances. The ClosedPolygon versions in Schoenflies/PolygonalJordan.lean are instances too — ClosedPolygon.parity_eq_one_of_mem_inside currently goes through StripData, and does not have to.

Blueprint

• Schoenflies.PrePolygon.pieces, …cover_pieces, …isClosedChain_pieces, …pieces_nondeg — the edge list the crossing count of §2 is defined on, for a vertex list that has not been normalized. Same list as ClosedPolygon.pieces; PrePolygon.pieces_toPre is rfl.
• Schoenflies.PrePolygon.isJordanCurve_carrier, …isPolygonal_carrier — §1, "a simple closed polygonal curve"; jointly the hypothesis of Theorem 2.3.
• Schoenflies.PrePolygon.isSeparating_carrier — Theorem 2.3 in the form Definition 2.4 asks for, for a polygon presented with redundant vertices.
• Schoenflies.PrePolygon.parity_flip_carrier — Lemma 2.2, second half.
• Schoenflies.parity_eq_zero_of_mem_outside_cover, Schoenflies.parity_eq_one_of_mem_inside_cover — the last sentence of Theorem 2.3, for an arbitrary closed chain whose cover separates.
• Schoenflies.PrePolygon.parity_eq_zero_of_mem_outside, …parity_eq_one_of_mem_inside, …parity_eq_zero_iff, …parity_eq_one_iff — the same, read off a PrePolygon.

Two notes for the integrator

PrePolygon.pieces duplicates ClosedPolygon.pieces. The two definitions are literally the same expression and PrePolygon.pieces_toPre proves them equal by rfl. The right arrangement is to define ClosedPolygon.pieces P := P.toPre.pieces and to keep only the PrePolygon proofs — the proofs of cover_pieces, isClosedChain_pieces, pieces_nondeg, pieces_nodup, notMem_edge_of_mem_openSegment and parity_flip_carrier in Schoenflies/PolygonBridge.lean use vertex_inj and edges_meet and nothing else, so they are the proofs below with ClosedPolygon written for PrePolygon. That refactor cannot happen inside this module: PrePolygon is declared in Schoenflies/Realization.lean, which is downstream of PolygonBridge. It needs PrePolygon moved up beside ClosedPolygon in Schoenflies/Strip.lean.

Merging collinear edges is a subdivision, but not one this development can point at. Deleting a redundant vertex v replaces the two edges at v by their union, which is exactly undoing Schoenflies.splitAt v on the merged edge; iterating, P.pieces is subdivide P'.pieces vs for the list vs of deleted vertices — up to the order of the list, which rotate disturbs. So two things are missing before parity_subdivide could be used here: Schoenflies.parity invariance under List.Perm (immediate, parity is a sum over the list), and a strengthening of exists_closedPolygon_of_prePolygon to ∃ m' (P' : ClosedPolygon m') (vs : List Plane), P'.carrier = P.carrier ∧ P.pieces ~ subdivide P'.pieces vs, carried through the induction. The direct argument below is shorter than either.

Small arithmetic helpers

Copies of two private facts of Schoenflies/PolygonalJordan.lean; they are private there and so are these.

The two parity values from separation alone

The blueprint reads the two values off a point far along the ray direction and off a point either side of an edge. Neither step knows anything about vertices, so both are stated here for an arbitrary closed chain whose cover separates the plane.

theorem Schoenflies.parity_eq_zero_of_mem_outside_cover {L : List Piece} {u : Plane} (hu : u.IsDirection) (hL : ∀ Q ∈ L, hgt u Q.1 ≠ hgt u Q.2) (hC : IsClosedChain L) (hsep : IsSeparating (cover L)) {x : Plane} (hx : x ∈ outside (cover L)) : parity u L x = 0

π_C = 0 on the unbounded region (Theorem 2.3, last sentence), for any closed chain whose cover separates the plane.

The blueprint's argument: a point far enough along the ray direction is crossed by no edge, and the whole half-plane of such points is convex — hence connected — and unbounded, so it lies in the unbounded region. Parity is constant there (Lemma 2.2), and the value is the one read off the far point.

theorem Schoenflies.parity_eq_one_of_mem_inside_cover {L : List Piece} {u : Plane} (hu : u.IsDirection) (hL : ∀ Q ∈ L, hgt u Q.1 ≠ hgt u Q.2) (hC : IsClosedChain L) (hsep : IsSeparating (cover L)) {a b : Plane} (ha : a ∉ cover L) (hb : b ∉ cover L) (hab : parity u L a ≠ parity u L b) {x : Plane} (hx : x ∈ inside (cover L)) : parity u L x = 1

π_C = 1 on the bounded region (Theorem 2.3, last sentence), for any closed chain whose cover separates the plane and which has some two points of the complement with different parities.

Those two points cannot be in the same region, since parity is constant on a region; so one of them is inside and the other outside. The outside carries 0, hence the inside does not.

For a polygon the two points are supplied by Lemma 2.2: just before and just after an interior point of any single edge.

The edge list

Verbatim Schoenflies.ClosedPolygon.pieces with the structure changed; pieces_toPre records that the two are the same list.

def Schoenflies.PrePolygon.pieces {m : ℕ} (P : PrePolygon m) : List Piece

The m + 3 edges of the polygon, as a list of pieces in cyclic order. This is the form the crossing count of §2 is defined on.

Equations

• P.pieces = List.map (fun (j : ℕ) => (P.vertex ↑j, P.vertex (↑j + 1))) (List.range (m + 3))

@[simp]

theorem Schoenflies.PrePolygon.pieces_toPre {m : ℕ} (P : ClosedPolygon m) : P.toPre.pieces = P.pieces

Forgetting the corner field does not change the edge list.

theorem Schoenflies.PrePolygon.mem_pieces {m : ℕ} (P : PrePolygon m) (i : ZMod (m + 3)) : (P.vertex i, P.vertex (i + 1)) ∈ P.pieces

Every edge of the polygon is on the list.

theorem Schoenflies.PrePolygon.exists_of_mem_pieces {m : ℕ} {P : PrePolygon m} {Q : Piece} (hQ : Q ∈ P.pieces) : ∃ (i : ZMod (m + 3)), Q = (P.vertex i, P.vertex (i + 1))

Every piece on the list is an edge of the polygon.

theorem Schoenflies.PrePolygon.pieces_nondeg {m : ℕ} (P : PrePolygon m) (Q : Piece) : Q ∈ P.pieces → Q.Nondeg

No edge is degenerate: consecutive vertices are distinct. Redundant vertices are allowed, but repeated ones are not.

theorem Schoenflies.PrePolygon.isClosedChain_pieces {m : ℕ} (P : PrePolygon m) : IsClosedChain P.pieces

The edge list is a closed chain. Each vertex ends one edge and starts the next, so it is counted twice; the cycle closes because m + 3 is 0 in ZMod (m + 3).

theorem Schoenflies.PrePolygon.cover_pieces {m : ℕ} (P : PrePolygon m) : cover P.pieces = P.carrier

The edge list carries the polygon. This is the equation that turns every parity statement, which is about cover, into a statement about the carrier.

theorem Schoenflies.PrePolygon.pieces_nodup {m : ℕ} (P : PrePolygon m) : P.pieces.Nodup

The edge list has no repeated entry: distinct indices name distinct initial vertices.

The curve statements, and separation

All three are properties of the carrier as a set, and normalization keeps the carrier, so all three come across from the ClosedPolygon versions with nothing to check.

theorem Schoenflies.PrePolygon.isCompact_carrier {m : ℕ} (P : PrePolygon m) : IsCompact P.carrier

The carrier is compact: it is what a finite list of segments occupies.

theorem Schoenflies.PrePolygon.isClosed_carrier {m : ℕ} (P : PrePolygon m) : IsClosed P.carrier

theorem Schoenflies.PrePolygon.isJordanCurve_carrier {m : ℕ} (P : PrePolygon m) : IsJordanCurve P.carrier

The carrier is a Jordan curve, redundant vertices and all. Deleting them does not move the curve, and the normalized polygon's carrier is a Jordan curve.

theorem Schoenflies.PrePolygon.isPolygonal_carrier {m : ℕ} (P : PrePolygon m) : IsPolygonal P.carrier

The carrier is polygonal.

theorem Schoenflies.PrePolygon.isSeparating_carrier {m : ℕ} (P : PrePolygon m) : IsSeparating P.carrier

The polygonal Jordan curve theorem (Theorem 2.3) for a polygon presented with redundant vertices, in the form Definition 2.4 asks for.

This is the statement the crosscut machinery of Schoenflies/CrosscutCells.lean onwards consumes, and IsSeparating speaks only of the carrier, so normalizing and quoting ClosedPolygon.isSeparating_carrier is the whole proof.

theorem Schoenflies.PrePolygon.connectedComponentIn_eq_inside_or_outside {m : ℕ} (P : PrePolygon m) {x : Plane} (hx : x ∉ P.carrier) : connectedComponentIn P.carrierᶜ x = inside P.carrier ∨ connectedComponentIn P.carrierᶜ x = outside P.carrier

Exactly two regions: the component of any point off the polygon is one of the two named ones.

The crossing parity

The list-level statements of Schoenflies/Parity.lean, read off a PrePolygon.

theorem Schoenflies.PrePolygon.exists_direction_pieces {m : ℕ} (P : PrePolygon m) : ∃ (u : Plane), u.IsDirection ∧ ∀ Q ∈ P.pieces, hgt u Q.1 ≠ hgt u Q.2

A ray direction level for no edge of the polygon; the blueprint's "rotate the coordinate system so that no edge is horizontal", with nothing rotated.

theorem Schoenflies.PrePolygon.parity_eq_of_mem_connectedComponentIn_carrier {m : ℕ} (P : PrePolygon m) {u : Plane} (hu : u.IsDirection) (hL : ∀ Q ∈ P.pieces, hgt u Q.1 ≠ hgt u Q.2) {x y : Plane} (hx : x ∉ P.carrier) (hy : y ∈ connectedComponentIn P.carrierᶜ x) : parity u P.pieces y = parity u P.pieces x

Crossing parity (Lemma 2.2): π_C is constant on the component of the complement of the carrier containing a given point.

theorem Schoenflies.PrePolygon.notMem_edge_of_mem_openSegment {m : ℕ} {P : PrePolygon m} {i j : ZMod (m + 3)} (hij : j ≠ i) {p : Plane} (hp : p ∈ openSegment ℝ (P.vertex i) (P.vertex (i + 1))) : p ∉ P.edge j

An interior point of one edge lies on no other edge: edges_meet puts any other edge's meeting point at an end of this one, and an interior point is neither end.

theorem Schoenflies.PrePolygon.parity_flip_carrier {m : ℕ} (P : PrePolygon m) {u : Plane} (hu : u.IsDirection) (hL : ∀ Q ∈ P.pieces, hgt u Q.1 ≠ hgt u Q.2) (i : ZMod (m + 3)) {p : Plane} (hp : p ∈ openSegment ℝ (P.vertex i) (P.vertex (i + 1))) : ∃ δ > 0, ∀ (t : ℝ), 0 < t → t < δ → p - t • u ∉ P.carrier ∧ p + t • u ∉ P.carrier ∧ parity u P.pieces (p - t • u) = parity u P.pieces (p + t • u) + 1

Opposite sides of an edge (Lemma 2.2, second half). Just before and just after an interior point of an edge, in the ray direction, the base point is off the carrier and the crossing parity differs by one.

The edge being crossed is split out of the list by List.append_of_mem; that the two remaining fragments miss the crossing point is edges_meet, through PrePolygon.notMem_edge_of_mem_openSegment.

theorem Schoenflies.PrePolygon.exists_parity_ne {m : ℕ} (P : PrePolygon m) {u : Plane} (hu : u.IsDirection) (hL : ∀ Q ∈ P.pieces, hgt u Q.1 ≠ hgt u Q.2) : ∃ (a : Plane) (b : Plane), a ∉ P.carrier ∧ b ∉ P.carrier ∧ parity u P.pieces a ≠ parity u P.pieces b

Two points off the curve at which the parity differs: just before and just after the midpoint of the first edge. This is what turns the separation theorem into the two parity values.

theorem Schoenflies.PrePolygon.parity_eq_zero_of_mem_outside {m : ℕ} (P : PrePolygon m) {u : Plane} (hu : u.IsDirection) (hL : ∀ Q ∈ P.pieces, hgt u Q.1 ≠ hgt u Q.2) {x : Plane} (hx : x ∈ outside P.carrier) : parity u P.pieces x = 0

π_C = 0 on the unbounded region (Theorem 2.3), for a polygon presented with redundant vertices.

theorem Schoenflies.PrePolygon.parity_eq_one_of_mem_inside {m : ℕ} (P : PrePolygon m) {u : Plane} (hu : u.IsDirection) (hL : ∀ Q ∈ P.pieces, hgt u Q.1 ≠ hgt u Q.2) {x : Plane} (hx : x ∈ inside P.carrier) : parity u P.pieces x = 1

π_C = 1 on the bounded region (Theorem 2.3), for a polygon presented with redundant vertices.

theorem Schoenflies.PrePolygon.parity_eq_one_iff {m : ℕ} (P : PrePolygon m) {u : Plane} (hu : u.IsDirection) (hL : ∀ Q ∈ P.pieces, hgt u Q.1 ≠ hgt u Q.2) {x : Plane} (hx : x ∉ P.carrier) : parity u P.pieces x = 1 ↔ x ∈ inside P.carrier

The crossing parity decides the region (Theorem 2.3): off the curve, π_C = 1 says "inside".

theorem Schoenflies.PrePolygon.parity_eq_zero_iff {m : ℕ} (P : PrePolygon m) {u : Plane} (hu : u.IsDirection) (hL : ∀ Q ∈ P.pieces, hgt u Q.1 ≠ hgt u Q.2) {x : Plane} (hx : x ∉ P.carrier) : parity u P.pieces x = 0 ↔ x ∈ outside P.carrier

The crossing parity decides the region, the other way round.

The ClosedPolygon parity values are instances

A machine check of the claim made in this module's docstring. Schoenflies/PolygonalJordan.lean proves ClosedPolygon.parity_eq_one_of_mem_inside from a StripData — the collar of Lemma 1.8, which is where corner is used. The collar is needed for Theorem 2.3 itself, but not a second time for the parity value: given separation, the two values follow from the general lemmas above. The two examples below are the same statements, re-proved that way.