The polygon bridge

Two independent representations of a closed polygon had grown up side by side and never met. Schoenflies/Strip.lean carries ClosedPolygon m, a cyclic vertex list indexed by ZMod (m + 3), and everything the collar of Lemma 1.8 says is said about it. Schoenflies/Parity.lean carries List Piece together with IsClosedChain, and everything the crossing count of Lemma 2.1 and Lemma 2.2 says is said about that. Neither knew about the other, and — worse — nothing anywhere produced a ClosedPolygon, so every theorem about one was formally a theorem about a structure that might have been empty.

This module closes the three gaps.

Non-vacuity

Schoenflies.triangle builds a ClosedPolygon 0 out of any three points with nonzero orientation determinant, and Schoenflies.unitTriangle is the concrete instance with vertices (0,0), (1,0), (0,1). The only real work is edges_meet: two edges of a triangle share exactly one endpoint, and Schoenflies.segment_inter_shared says two segments meeting at an endpoint whose far ends are off the shared line meet nowhere else. That lemma is proved by taking the orientation form against the first segment's direction, which kills the first segment's own parameter and forces the second's to vanish.

The representation bridge

ClosedPolygon.pieces lists the m + 3 edges as pairs of endpoints, in cyclic order. It is a closed chain (ClosedPolygon.isClosedChain_pieces), every piece is nondegenerate (ClosedPolygon.pieces_nondeg), and — the point of the exercise — ClosedPolygon.cover_pieces says it occupies exactly the polygon's carrier. Closedness is a telescoping sum: Schoenflies.sum_range_boundary evaluates the mod-2 boundary of the chain 0 → 1 → ⋯ → n as the sum of its two ends, and the two ends of 0 → ⋯ → m + 3 are the same vertex because m + 3 is 0 in ZMod (m + 3).

The curve bridge

ClosedPolygon.isJordanCurve_carrier and ClosedPolygon.isPolygonal_carrier say the carrier is a simple closed polygonal curve in the blueprint's sense, which is what the polygonal Jordan curve theorem (Theorem 2.3) takes as its hypothesis. The loop is built by concatenating edge parametrizations around the cycle: ClosedPolygon.chain k is the union of the edges leaving vertices 0, …, k, and ClosedPolygon.isArcBetween_chain grows it one edge at a time by IsArcBetween.concatenate. The hypothesis that concatenation needs — the new edge meets what came before only at the vertex they share — is exactly edges_meet twice over: once to place the meeting point among the new edge's own two endpoints, and once more to rule out the far one, which would otherwise let the polygon close early. The last edge closes the loop through IsJordanCurve.of_two_arcs, and there the far endpoint is not ruled out: it is the second shared point that makes the two arcs a curve rather than an arc.

Both halves at once

The last section is what the bridge is for: the two statements of Lemma 2.2 — parity is constant on a component of the complement, and it flips across an edge — restated for the carrier of a ClosedPolygon rather than for the cover of an anonymous list. The flip needs the edge list split around the edge being crossed, which is List.append_of_mem together with ClosedPolygon.pieces_nodup; that the two remaining fragments miss the crossing point is edges_meet a third time.

Blueprint

• Schoenflies.triangle, Schoenflies.unitTriangle — witnesses that §1's "simple closed polygonal curve" is not vacuous.
• ClosedPolygon.pieces, ClosedPolygon.cover_pieces, ClosedPolygon.isClosedChain_pieces — the edge list the crossing count of §2 is defined on, and that it carries the polygon.
• ClosedPolygon.isJordanCurve_carrier, ClosedPolygon.isPolygonal_carrier — §1, "a simple closed polygonal curve"; jointly the hypothesis of Theorem 2.3.
• ClosedPolygon.parity_eq_of_mem_connectedComponentIn_carrier, ClosedPolygon.parity_flip_carrier — the two halves of Lemma 2.2, read off a ClosedPolygon. These are the statements Theorem 2.3 consumes.

One general lemma is stated here that does not belong here: Schoenflies.exists_of_mem_cover, the destructor matching Schoenflies.mem_cover, whose home is Schoenflies/Parity.lean.

Two segments that share an endpoint

The one piece of plane geometry this module needs. Schoenflies/SegmentMeet.lean describes the intersection of two arbitrary segments; here the two are known to share an endpoint, and the conclusion is sharper and the proof shorter.

theorem Schoenflies.segment_inter_shared {a b c : Plane} (h : (b - a).det (c - b) ≠ 0) : segment ℝ a b ∩ segment ℝ b c ⊆ {b}

Two segments sharing the endpoint b, whose far ends are off the line through the other, meet only at b. Taking the orientation form against b - a annihilates the first segment's own parameter, so the second segment's parameter must vanish.

Non-vacuity: a triangle is a closed polygon

Nothing in the strip development ever built a ClosedPolygon, so polygonal_collar and every theorem beside it was formally a theorem about a structure with no known inhabitant. A triangle is the smallest witness, and no coordinates are needed: any three points with nonzero orientation determinant will do.

def Schoenflies.triangle {a b c : Plane} (h : (b - a).det (c - a) ≠ 0) : ClosedPolygon 0

A triangle is a simple closed polygon. Any three points that are not collinear, taken in that cyclic order. edges_meet holds because two of the three edges always share exactly one endpoint, and corner because the orientation form is what nonzero says.

Equations

• Schoenflies.triangle h = { vertex := ![a, b, c], vertex_inj := ⋯, edges_meet := ⋯, corner := ⋯ }

@[simp]

theorem Schoenflies.triangle_vertex_zero {a b c : Plane} (h : (b - a).det (c - a) ≠ 0) : (triangle h).vertex 0 = a

@[simp]

theorem Schoenflies.triangle_vertex_one {a b c : Plane} (h : (b - a).det (c - a) ≠ 0) : (triangle h).vertex 1 = b

@[simp]

theorem Schoenflies.triangle_vertex_two {a b c : Plane} (h : (b - a).det (c - a) ≠ 0) : (triangle h).vertex 2 = c

def Schoenflies.unitTriangle : ClosedPolygon 0

A concrete simple closed polygon: the triangle with vertices (0,0), (1,0) and (0,1).

Equations

• Schoenflies.unitTriangle = Schoenflies.triangle Schoenflies.unitTriangle._proof_1

A telescoping sum mod two

theorem Schoenflies.sum_range_boundary (g : ℕ → ZMod 2) (n : ℕ) : (List.map (fun (j : ℕ) => g j + g (j + 1)) (List.range n)).sum = g 0 + g n

The mod-2 boundary of the chain 0 → 1 → ⋯ → n is the sum of its two ends: every interior vertex is counted twice. This is the whole content of "a cycle is a closed chain".

Natural-number indices

Both bridges run over the vertices with a natural number and cast into ZMod (m + 3). Below the modulus the cast is injective, which is what turns "these two indices are different naturals" into "these are different edges" and back.

theorem Schoenflies.ClosedPolygon.natCast_inj {m j k : ℕ} (hj : j < m + 3) (hk : k < m + 3) (h : ↑j = ↑k) : j = k

Below the modulus, casting a natural number into ZMod (m + 3) is injective.

theorem Schoenflies.ClosedPolygon.natCast_succ {m : ℕ} (j : ℕ) : ↑(j + 1) = ↑j + 1

The successor, pushed through the cast.

theorem Schoenflies.ClosedPolygon.vertex_natCast_ne {m : ℕ} {P : ClosedPolygon m} {j k : ℕ} (hj : j < m + 3) (hk : k < m + 3) (hjk : j ≠ k) : P.vertex ↑j ≠ P.vertex ↑k

Distinct indices below the modulus name distinct vertices.

theorem Schoenflies.ClosedPolygon.edge_meet_earlier {m : ℕ} {P : ClosedPolygon m} {j k : ℕ} (hjk : j < k) (hk : k + 1 < m + 3) {z : Plane} (hzj : z ∈ P.edge ↑j) (hzk : z ∈ P.edge ↑k) : z = P.vertex ↑k

An edge meets an earlier edge only at its own initial vertex. edges_meet puts the meeting point at one of the two ends of the later edge; the far end is ruled out by applying edges_meet the other way round, which would put the later edge's terminal vertex on the earlier edge and hence make it one of two vertices it cannot be. This is what stops the polygon from closing before it has run through all its vertices.

theorem Schoenflies.ClosedPolygon.edge_meet_last {m : ℕ} {P : ClosedPolygon m} {j : ℕ} (hj : j < m + 2) {z : Plane} (hzj : z ∈ P.edge ↑j) (hz : z ∈ P.edge ↑(m + 2)) : z = P.vertex 0 ∨ z = P.vertex ↑(m + 2)

The last edge meets every earlier edge only at a vertex it shares with the cycle's ends. Here the far end is not excluded: the last edge runs back to vertex 0, so both of its ends are legitimate meeting points, and that is precisely what makes the carrier a closed curve rather than an arc.

The representation bridge

Schoenflies/Parity.lean counts crossings of a List Piece; ClosedPolygon.pieces is the list it should be handed. The four obligations below are exactly what every parity statement asks for: a list, closedness, nondegeneracy, and — the one that carries the geometry — that the list occupies the polygon.

def Schoenflies.ClosedPolygon.pieces {m : ℕ} (P : ClosedPolygon 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))

theorem Schoenflies.ClosedPolygon.mem_pieces {m : ℕ} (P : ClosedPolygon 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.ClosedPolygon.exists_of_mem_pieces {m : ℕ} {P : ClosedPolygon 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.ClosedPolygon.pieces_nondeg {m : ℕ} (P : ClosedPolygon m) (Q : Piece) : Q ∈ P.pieces → Q.Nondeg

No edge of a simple closed polygon is degenerate: consecutive vertices are distinct.

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

The edge list is a closed chain. Each vertex is the terminal end of one edge and the initial end of the next, so it is counted twice; the cycle closes because m + 3 is 0 in ZMod (m + 3), which makes the two ends of the telescoping sum the same vertex.

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

The edge list carries the polygon. Without this equation no parity statement says anything about a ClosedPolygon: the crossing count is defined against cover, and the collar against carrier.

The curve bridge

chain k is the union of the edges leaving vertices 0, …, k. Each is an arc from vertex 0 to vertex k + 1, obtained from its predecessor by IsArcBetween.concatenate; the whole carrier is the last of them plus the edge that runs back to vertex 0.

def Schoenflies.ClosedPolygon.chain {m : ℕ} (P : ClosedPolygon m) : ℕ → Set Plane

The union of the edges leaving vertices 0, 1, …, k.

Equations

• P.chain 0 = P.edge 0
• P.chain k.succ = P.chain k ∪ P.edge ↑(k + 1)

theorem Schoenflies.ClosedPolygon.mem_chain_iff {m : ℕ} {P : ClosedPolygon m} {z : Plane} {k : ℕ} : z ∈ P.chain k ↔ ∃ j ≤ k, z ∈ P.edge ↑j

theorem Schoenflies.ClosedPolygon.chain_eq_carrier {m : ℕ} (P : ClosedPolygon m) : P.chain (m + 2) = P.carrier

Running through all m + 3 edges exhausts the carrier.

theorem Schoenflies.ClosedPolygon.isArcBetween_chain {m : ℕ} (P : ClosedPolygon m) (k : ℕ) : k + 1 < m + 3 → IsArcBetween (P.chain k) (P.vertex 0) (P.vertex ↑(k + 1))

The partial chains are arcs. One edge at a time, glued at the vertex they share: edge_meet_earlier is exactly the hypothesis IsArcBetween.concatenate asks for. The bound k + 1 < m + 3 is what keeps the growing arc from meeting its own start.

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

The carrier of a simple closed polygon is a Jordan curve. The arc through all but the last edge, and the last edge running back to where it started, meet exactly at their two shared endpoints.

The carrier is polygonal

IsPolygonal asks for a vertex list whose poly carrier is the set. Cycling once round the polygon and coming back to the first vertex is that list.

def Schoenflies.ClosedPolygon.vlist {m : ℕ} (P : ClosedPolygon m) : ℕ → List Plane

The vertex list v₀, v₁, …, v_{k+1}, which walks the first k + 1 edges.

Equations

• P.vlist 0 = [P.vertex 0, P.vertex ↑1]
• P.vlist k.succ = P.vlist k ++ [P.vertex ↑(k + 1 + 1)]

theorem Schoenflies.ClosedPolygon.vlist_ne_nil {m : ℕ} (P : ClosedPolygon m) (k : ℕ) : P.vlist k ≠ []

theorem Schoenflies.ClosedPolygon.getLast_vlist {m : ℕ} (P : ClosedPolygon m) (k : ℕ) : (P.vlist k).getLast ⋯ = P.vertex ↑(k + 1)

theorem Schoenflies.ClosedPolygon.poly_vlist {m : ℕ} (P : ClosedPolygon m) (k : ℕ) : poly (P.vlist k) = P.chain k

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

The carrier of a simple closed polygon is polygonal: it is the carrier of the vertex list that runs once round the cycle and back to its first vertex.

The bridge in use

With both halves in place a parity statement can be read off a ClosedPolygon directly.

theorem Schoenflies.ClosedPolygon.exists_direction_pieces {m : ℕ} (P : ClosedPolygon 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.ClosedPolygon.parity_eq_of_mem_connectedComponentIn_carrier {m : ℕ} (P : ClosedPolygon 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 for a closed polygon (Lemma 2.2): π_C is constant on the component of the complement of the carrier containing a given point.

The flip across an edge

The second half of Lemma 2.2 is stated for the edge list split around the edge being crossed, L₁ ++ (a, b) :: L₂. Splitting is List.append_of_mem; what has to be checked is that the two remaining fragments miss the point being crossed, and that is edges_meet again — another edge can reach an interior point of this one only at one of this one's two ends, which an interior point is not.

theorem Schoenflies.ClosedPolygon.exists_of_mem_cover {L : List Piece} {z : Plane} (hz : z ∈ cover L) : ∃ R ∈ L, z ∈ R.seg

What a list of pieces occupies, taken apart. The counterpart of Schoenflies.mem_cover, which only builds; this belongs next to it in Schoenflies/Parity.lean.

theorem Schoenflies.ClosedPolygon.notMem_edge_of_mem_openSegment {m : ℕ} {P : ClosedPolygon 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.ClosedPolygon.pieces_nodup {m : ℕ} (P : ClosedPolygon m) : P.pieces.Nodup

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

theorem Schoenflies.ClosedPolygon.parity_flip_carrier {m : ℕ} (P : ClosedPolygon 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, for a closed polygon (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.