The Jordan curve theorem for polygons

Statements of the separation properties of polygonal simple closed curves in the plane, following Moise, Geometric Topology in Dimensions 2 and 3, Ch. 2 ("Separation properties of polygons in R²"). Only the polygonal case is stated: this is what the triangulation theorem consumes (via the combinatorial Schoenflies theorem, Moise Thm. 5.3). The full Jordan curve theorem (Moise Ch. 4) is not on the triangulation route's critical path.

PolygonalCircle is the honest object: cyclically indexed vertices joined by genuine segments, with adjacent segments meeting exactly at their shared vertex and non-adjacent segments disjoint. A junk witness cannot satisfy these fields: they force the carrier to be a topological circle.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle : Type

A polygonal simple closed curve in the plane: at least three vertices, cyclically indexed, with consecutive vertices distinct, adjacent edges meeting exactly in their shared vertex, and non-adjacent edges disjoint.

• n : ℕ

  The number of vertices (and edges).

• three_le : 3 ≤ self.n

  A polygon has at least three vertices.

• vertex : ZMod self.n → Plane

  The cyclically indexed vertices.

• adjacent_ne (i : ZMod self.n) : self.vertex i ≠ self.vertex (i + 1)

  Consecutive vertices are distinct, so every edge is a genuine segment.

• consecutive_inter (i : ZMod self.n) : segment ℝ (self.vertex i) (self.vertex (i + 1)) ∩ segment ℝ (self.vertex (i + 1)) (self.vertex (i + 2)) = {self.vertex (i + 1)}

  Adjacent edges meet exactly in their shared vertex.

• nonadjacent_disjoint (i j : ZMod self.n) : i ≠ j → i ≠ j + 1 → j ≠ i + 1 → segment ℝ (self.vertex i) (self.vertex (i + 1)) ∩ segment ℝ (self.vertex j) (self.vertex (j + 1)) = ∅

  Non-adjacent edges are disjoint.

instance LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.instNeZeroNatN (J : PolygonalCircle) : NeZero J.n

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeSegment (J : PolygonalCircle) (i : ZMod J.n) : Set Plane

The edge from vertex i to vertex i + 1.

Equations

• J.edgeSegment i = segment ℝ (J.vertex i) (J.vertex (i + 1))

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.NonAdjacentEdges (J : PolygonalCircle) (i j : ZMod J.n) : Prop

Two edge indices are nonadjacent when the corresponding edges share no endpoint.

Equations

• J.NonAdjacentEdges i j = (i ≠ j ∧ i ≠ j + 1 ∧ j ≠ i + 1)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.carrier (J : PolygonalCircle) : Set Plane

The carrier of the polygon: the union of its edges.

Equations

• J.carrier = ⋃ (i : ZMod J.n), J.edgeSegment i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.vertex_mem_carrier (J : PolygonalCircle) (i : ZMod J.n) : J.vertex i ∈ J.carrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.carrier_nonempty (J : PolygonalCircle) : J.carrier.Nonempty

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isCompact_edgeSegment (J : PolygonalCircle) (i : ZMod J.n) : IsCompact (J.edgeSegment i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isCompact_carrier (J : PolygonalCircle) : IsCompact J.carrier

The carrier of a polygon is compact.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isClosed_carrier (J : PolygonalCircle) : IsClosed J.carrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isClosed_edgeSegment (J : PolygonalCircle) (i : ZMod J.n) : IsClosed (J.edgeSegment i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.mapEmbedding (J : PolygonalCircle) (f : Plane → Plane) (hinj : Set.InjOn f J.carrier) (hedge : ∀ (i : ZMod J.n), f '' J.edgeSegment i = segment ℝ (f (J.vertex i)) (f (J.vertex (i + 1)))) : PolygonalCircle

Transport a polygon through a function which is injective on its carrier and straight on each edge. No extension to an ambient homeomorphism is needed.

Equations

• J.mapEmbedding f hinj hedge = { n := J.n, three_le := ⋯, vertex := fun (i : ZMod J.n) => f (J.vertex i), adjacent_ne := ⋯, consecutive_inter := ⋯, nonadjacent_disjoint := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.mapEmbedding_n (J : PolygonalCircle) (f : Plane → Plane) (hinj : Set.InjOn f J.carrier) (hedge : ∀ (i : ZMod J.n), f '' J.edgeSegment i = segment ℝ (f (J.vertex i)) (f (J.vertex (i + 1)))) : (J.mapEmbedding f hinj hedge).n = J.n

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.mapEmbedding_vertex (J : PolygonalCircle) (f : Plane → Plane) (hinj : Set.InjOn f J.carrier) (hedge : ∀ (i : ZMod J.n), f '' J.edgeSegment i = segment ℝ (f (J.vertex i)) (f (J.vertex (i + 1)))) (i : ZMod J.n) : (J.mapEmbedding f hinj hedge).vertex i = f (J.vertex i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.mapEmbedding_edgeSegment (J : PolygonalCircle) (f : Plane → Plane) (hinj : Set.InjOn f J.carrier) (hedge : ∀ (i : ZMod J.n), f '' J.edgeSegment i = segment ℝ (f (J.vertex i)) (f (J.vertex (i + 1)))) (i : ZMod J.n) : (J.mapEmbedding f hinj hedge).edgeSegment i = f '' J.edgeSegment i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.mapEmbedding_carrier (J : PolygonalCircle) (f : Plane → Plane) (hinj : Set.InjOn f J.carrier) (hedge : ∀ (i : ZMod J.n), f '' J.edgeSegment i = segment ℝ (f (J.vertex i)) (f (J.vertex (i + 1)))) : (J.mapEmbedding f hinj hedge).carrier = f '' J.carrier

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.mapHomeomorph (J : PolygonalCircle) (h : Plane ≃ₜ Plane) (hedge : ∀ (i : ZMod J.n), ⇑h '' J.edgeSegment i = segment ℝ (h (J.vertex i)) (h (J.vertex (i + 1)))) : PolygonalCircle

Transport a polygon through a homeomorphism which is straight on each polygon edge.

Equations

• J.mapHomeomorph h hedge = { n := J.n, three_le := ⋯, vertex := fun (i : ZMod J.n) => h (J.vertex i), adjacent_ne := ⋯, consecutive_inter := ⋯, nonadjacent_disjoint := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.mapHomeomorph_n (J : PolygonalCircle) (h : Plane ≃ₜ Plane) (hedge : ∀ (i : ZMod J.n), ⇑h '' J.edgeSegment i = segment ℝ (h (J.vertex i)) (h (J.vertex (i + 1)))) : (J.mapHomeomorph h hedge).n = J.n

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.mapHomeomorph_vertex (J : PolygonalCircle) (h : Plane ≃ₜ Plane) (hedge : ∀ (i : ZMod J.n), ⇑h '' J.edgeSegment i = segment ℝ (h (J.vertex i)) (h (J.vertex (i + 1)))) (i : ZMod J.n) : (J.mapHomeomorph h hedge).vertex i = h (J.vertex i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.mapHomeomorph_edgeSegment (J : PolygonalCircle) (h : Plane ≃ₜ Plane) (hedge : ∀ (i : ZMod J.n), ⇑h '' J.edgeSegment i = segment ℝ (h (J.vertex i)) (h (J.vertex (i + 1)))) (i : ZMod J.n) : (J.mapHomeomorph h hedge).edgeSegment i = ⇑h '' J.edgeSegment i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.mapHomeomorph_carrier (J : PolygonalCircle) (h : Plane ≃ₜ Plane) (hedge : ∀ (i : ZMod J.n), ⇑h '' J.edgeSegment i = segment ℝ (h (J.vertex i)) (h (J.vertex (i + 1)))) : (J.mapHomeomorph h hedge).carrier = ⇑h '' J.carrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.disjoint_edgeSegment_of_nonAdjacent (J : PolygonalCircle) {i j : ZMod J.n} (hij : J.NonAdjacentEdges i j) : Disjoint (J.edgeSegment i) (J.edgeSegment j)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exists_uniform_nonAdjacent_separation (J : PolygonalCircle) : ∃ (ε : ℝ), 0 < ε ∧ ∀ (i j : ZMod J.n), J.NonAdjacentEdges i j → ∀ x ∈ J.edgeSegment i, ∀ y ∈ J.edgeSegment j, 3 * ε < dist x y

There is a uniform positive lower bound on distances between nonadjacent polygon edges.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exists_uniform_nonAdjacent_thickenings_disjoint (J : PolygonalCircle) : ∃ (ε : ℝ), 0 < ε ∧ ∀ (i j : ZMod J.n), J.NonAdjacentEdges i j → Disjoint (Metric.thickening ε (J.edgeSegment i)) (Metric.thickening ε (J.edgeSegment j))

Nonadjacent edges have disjoint tubes of one uniform positive radius.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.vertex_mem_edgeSegment_iff (J : PolygonalCircle) (i j : ZMod J.n) : J.vertex i ∈ J.edgeSegment j ↔ i = j ∨ i = j + 1

A vertex lies on exactly its outgoing and incoming polygon edges.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.vertex_injective (J : PolygonalCircle) : Function.Injective J.vertex

The vertices of a simple polygon are pairwise distinct.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exists_uniform_nonincident_vertex_edge_separation (J : PolygonalCircle) : ∃ (ε : ℝ), 0 < ε ∧ ∀ (i j : ZMod J.n), i ≠ j → i ≠ j + 1 → ∀ y ∈ J.edgeSegment j, 3 * ε < dist (J.vertex i) y

There is a uniform positive lower bound between every vertex and every edge not incident to that vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exists_uniform_edge_length (J : PolygonalCircle) : ∃ (ε : ℝ), 0 < ε ∧ ∀ (i : ZMod J.n), 3 * ε < dist (J.vertex i) (J.vertex (i + 1))

Polygon edges have a uniform positive lower bound on their lengths.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exists_featureRadius (J : PolygonalCircle) : ∃ (ε : ℝ), 0 < ε ∧ (∀ (i : ZMod J.n), 12 * ε < dist (J.vertex i) (J.vertex (i + 1))) ∧ (∀ (i j : ZMod J.n), J.NonAdjacentEdges i j → ∀ x ∈ J.edgeSegment i, ∀ y ∈ J.edgeSegment j, 12 * ε < dist x y) ∧ ∀ (i j : ZMod J.n), i ≠ j → i ≠ j + 1 → ∀ y ∈ J.edgeSegment j, 12 * ε < dist (J.vertex i) y

A single feature radius simultaneously controls edge lengths, nonadjacent-edge separation, and vertex-to-nonincident-edge separation.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.mem_incident_edge_of_mem_carrier_of_dist_lt (J : PolygonalCircle) {r : ℝ} (hsep : ∀ (i j : ZMod J.n), i ≠ j → i ≠ j + 1 → ∀ y ∈ J.edgeSegment j, r < dist (J.vertex i) y) {i : ZMod J.n} {x : Plane} (hx : x ∈ J.carrier) (hdist : dist (J.vertex i) x < r) : x ∈ J.edgeSegment i ∪ J.edgeSegment (i - 1)

Inside the vertex-to-nonincident-edge separation radius, every point of the carrier lies on one of the two edges incident to the vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ball_inter_carrier_eq_incident_edges (J : PolygonalCircle) {r : ℝ} (hsep : ∀ (i j : ZMod J.n), i ≠ j → i ≠ j + 1 → ∀ y ∈ J.edgeSegment j, r < dist (J.vertex i) y) (i : ZMod J.n) : Metric.ball (J.vertex i) r ∩ J.carrier = Metric.ball (J.vertex i) r ∩ (J.edgeSegment i ∪ J.edgeSegment (i - 1))

A ball inside the feature radius sees exactly the two polygon edges incident to its center vertex. This is the local isolation input for the vertex sectors of Moise's strip.

The local angular model at a polygon vertex

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.openAngularSector (a b : Circle) (r : ℝ) : Set ℂ

The open radial sector of radius r swept counterclockwise from direction a to direction b. It is parametrized by an open rectangle, avoiding the center and both boundary rays.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.openAngularSector a b r = (fun (p : ℝ × ℝ) => ↑p.1 * ↑(Circle.exp ((↑a).arg + p.2 * a.angleDiff b))) '' Set.Ioo 0 r ×ˢ Set.Ioo 0 1

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isPathConnected_openAngularSector (a b : Circle) {r : ℝ} (hr : 0 < r) : IsPathConnected (openAngularSector a b r)

An open angular sector of positive radius and nonzero angle is path connected.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.norm_openAngularSector_param (a b : Circle) {r : ℝ} {p : ℝ × ℝ} (hp : p ∈ Set.Ioo 0 r ×ˢ Set.Ioo 0 1) : ‖↑p.1 * ↑(Circle.exp ((↑a).arg + p.2 * a.angleDiff b))‖ = p.1

The radial norm in the sector is exactly its radial parameter.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.openAngularSector_subset_puncturedBall (a b : Circle) {r : ℝ} : openAngularSector a b r ⊆ Metric.ball 0 r \ {0}

Every point in an open angular sector lies in the punctured open disk of the stated radius.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.angularSector_param_mem_closure (a b : Circle) {r : ℝ} (hr : 0 < r) {p : ℝ × ℝ} (hp : p ∈ Set.Icc 0 r ×ˢ Set.Icc 0 1) : ↑p.1 * ↑(Circle.exp ((↑a).arg + p.2 * a.angleDiff b)) ∈ closure (openAngularSector a b r)

The closed parameter rectangle maps into the closure of the open angular sector.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.sourceRadialRay_mem_closure_openAngularSector (a b : Circle) {r radius : ℝ} (hr : 0 < r) (hradius : radius ∈ Set.Icc 0 r) : ↑radius * ↑a ∈ closure (openAngularSector a b r)

The initial radial boundary ray belongs to the closure of an angular sector.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.targetRadialRay_mem_closure_openAngularSector (a b : Circle) {r radius : ℝ} (hr : 0 < r) (hradius : radius ∈ Set.Icc 0 r) : ↑radius * ↑b ∈ closure (openAngularSector a b r)

The terminal radial boundary ray belongs to the closure of an angular sector.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.complexDirection (z : ℂ) (hz : z ≠ 0) : Circle

The unit direction of a nonzero complex vector.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.complexDirection z hz = ⟨z / ↑‖z‖, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.coe_complexDirection (z : ℂ) (hz : z ≠ 0) : ↑(complexDirection z hz) = z / ↑‖z‖

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.norm_mul_complexDirection (z : ℂ) (hz : z ≠ 0) : ↑‖z‖ * ↑(complexDirection z hz) = z

Polar reconstruction from norm and unit direction.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.openRadialRay (a : Circle) (r : ℝ) : Set ℂ

The open radial ray in direction a, truncated at radius r.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.openRadialRay a r = (fun (ρ : ℝ) => ↑ρ * ↑a) '' Set.Ioo 0 r

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.mem_openAngularSector_of_direction_eq_path {a b : Circle} {r : ℝ} {z : ℂ} (hz : z ≠ 0) (hzr : ‖z‖ < r) {t : ↑unitInterval} (ht0 : 0 < t) (ht1 : t < 1) (hdir : complexDirection z hz = (a.path b) t) : z ∈ openAngularSector a b r

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.mem_openRadialRay_of_direction_eq {a : Circle} {r : ℝ} {z : ℂ} (hz : z ≠ 0) (hzr : ‖z‖ < r) (hdir : complexDirection z hz = a) : z ∈ openRadialRay a r

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.puncturedBall_subset_twoSectors_union_rays {a b : Circle} (hab : a ≠ b) {r : ℝ} : Metric.ball 0 r \ {0} ⊆ openAngularSector a b r ∪ openAngularSector b a r ∪ openRadialRay a r ∪ openRadialRay b r

The two angular sectors and their two boundary rays partition the punctured disk.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.planeComplexEquiv : Plane ≃ₗᵢ[ℝ] ℂ

The standard linear isometry from the project's Euclidean plane to the complex plane.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.planeComplexEquiv = Complex.orthonormalBasisOneI.repr.symm

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.norm_planeComplexEquiv (x : Plane) : ‖planeComplexEquiv x‖ = ‖x‖

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.normalized_eq_of_complexDirection_eq {u v : Plane} (hu : u ≠ 0) (hv : v ≠ 0) (hdir : complexDirection (planeComplexEquiv u) ⋯ = complexDirection (planeComplexEquiv v) ⋯) : ‖u‖⁻¹ • u = ‖v‖⁻¹ • v

Equality of complex unit directions reflects equality of normalized plane vectors.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exists_nonzero_mem_segments_of_normalized_eq {u v : Plane} (hu : u ≠ 0) (hv : v ≠ 0) (hdir : ‖u‖⁻¹ • u = ‖v‖⁻¹ • v) : ∃ (q : Plane), q ≠ 0 ∧ q ∈ segment ℝ 0 u ∧ q ∈ segment ℝ 0 v

Two nonzero vectors with the same normalized direction have a common nonzero initial point on their segments from the origin.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.add_mem_segment_of_mem_segment_zero {p u q : Plane} (hq : q ∈ segment ℝ 0 u) : p + q ∈ segment ℝ p (p + u)

Translating a segment based at the origin gives the corresponding segment based at p.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.outgoingVector (J : PolygonalCircle) (i : ZMod J.n) : Plane

The ray from vertex i toward the next vertex.

Equations

• J.outgoingVector i = J.vertex (i + 1) - J.vertex i

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.incomingRayVector (J : PolygonalCircle) (i : ZMod J.n) : Plane

The ray from vertex i toward the preceding vertex.

Equations

• J.incomingRayVector i = J.vertex (i - 1) - J.vertex i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.outgoingVector_ne_zero (J : PolygonalCircle) (i : ZMod J.n) : J.outgoingVector i ≠ 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.incomingRayVector_ne_zero (J : PolygonalCircle) (i : ZMod J.n) : J.incomingRayVector i ≠ 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.incident_complexDirections_ne (J : PolygonalCircle) (i : ZMod J.n) : complexDirection (planeComplexEquiv (J.outgoingVector i)) ⋯ ≠ complexDirection (planeComplexEquiv (J.incomingRayVector i)) ⋯

The two unit directions cut out by the incident edges at a polygon vertex are distinct.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.complexDirection_pos_mul_circle (ρ : ℝ) (hρ : 0 < ρ) (a : Circle) : complexDirection (↑ρ * ↑a) ⋯ = a

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.direction_ne_boundary_of_mem_openAngularSector {a b : Circle} (hab : a ≠ b) {r : ℝ} {z : ℂ} (hz : z ∈ openAngularSector a b r) : complexDirection z ⋯ ≠ a ∧ complexDirection z ⋯ ≠ b

An interior point of an angular sector does not have either boundary direction.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.pos_rotation_mem_openAngularSector {a b : Circle} {radius bound θ : ℝ} (hθ : 0 < θ) (hδ : θ < a.angleDiff b) (hradius : 0 < radius) (hrbound : radius < bound) : ↑radius * ↑(Circle.exp θ) * ↑a ∈ openAngularSector a b bound

A small positive rotation from the initial boundary direction lies in the angular sector.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.neg_rotation_mem_openAngularSector {a b : Circle} {radius bound θ : ℝ} (hθ : 0 < θ) (hδ : θ < a.angleDiff b) (hradius : 0 < radius) (hrbound : radius < bound) : ↑radius * ↑(Circle.exp (-θ)) * ↑b ∈ openAngularSector a b bound

A small negative rotation from the terminal boundary direction lies in the angular sector.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ofReal_mul_circle_exp_re (radius θ : ℝ) : (↑radius * ↑(Circle.exp θ)).re = radius * Real.cos θ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ofReal_mul_circle_exp_im (radius θ : ℝ) : (↑radius * ↑(Circle.exp θ)).im = radius * Real.sin θ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.complexDirection_sub_eq_of_mem_segment {p q x : Plane} (hpq : p ≠ q) (hx : x ∈ segment ℝ p q) (hxp : x ≠ p) : complexDirection (planeComplexEquiv (x - p)) ⋯ = complexDirection (planeComplexEquiv (q - p)) ⋯

A noninitial point of a segment has the direction of the segment.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.outgoingDirection (J : PolygonalCircle) (i : ZMod J.n) : Circle

The outgoing complex direction at a polygon vertex.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.incomingRayDirection (J : PolygonalCircle) (i : ZMod J.n) : Circle

The complex direction from a polygon vertex toward its predecessor.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.outgoingDirection_ne_incomingRayDirection (J : PolygonalCircle) (i : ZMod J.n) : J.outgoingDirection i ≠ J.incomingRayDirection i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.coe_incomingRayDirection_add_one (J : PolygonalCircle) (i : ZMod J.n) : ↑(J.incomingRayDirection (i + 1)) = -↑(J.outgoingDirection i)

At the terminal endpoint of an edge, its incoming ray points opposite to its oriented outgoing direction.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.vertexForwardSector (J : PolygonalCircle) (i : ZMod J.n) (r : ℝ) : Set Plane

One of the two open sectors in the vertex ball, transported back from the complex plane.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.vertexBackwardSector (J : PolygonalCircle) (i : ZMod J.n) (r : ℝ) : Set Plane

The other open sector in the vertex ball.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isPathConnected_vertexForwardSector (J : PolygonalCircle) (i : ZMod J.n) {r : ℝ} (hr : 0 < r) : IsPathConnected (J.vertexForwardSector i r)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isPathConnected_vertexBackwardSector (J : PolygonalCircle) (i : ZMod J.n) {r : ℝ} (hr : 0 < r) : IsPathConnected (J.vertexBackwardSector i r)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.outgoingRay_mem_closure_vertexSectors (J : PolygonalCircle) (i : ZMod J.n) {r radius : ℝ} (hr : 0 < r) (hradius : radius ∈ Set.Icc 0 r) : J.vertex i + planeComplexEquiv.symm (↑radius * ↑(J.outgoingDirection i)) ∈ closure (J.vertexForwardSector i r) ∩ closure (J.vertexBackwardSector i r)

The outgoing edge ray is in the closure of each local side sector.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.incomingRay_mem_closure_vertexSectors (J : PolygonalCircle) (i : ZMod J.n) {r radius : ℝ} (hr : 0 < r) (hradius : radius ∈ Set.Icc 0 r) : J.vertex i + planeComplexEquiv.symm (↑radius * ↑(J.incomingRayDirection i)) ∈ closure (J.vertexForwardSector i r) ∩ closure (J.vertexBackwardSector i r)

The incoming edge ray is in the closure of each local side sector.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.vertexForwardSector_subset_ball_diff_carrier (J : PolygonalCircle) {r : ℝ} (hsep : ∀ (i j : ZMod J.n), i ≠ j → i ≠ j + 1 → ∀ y ∈ J.edgeSegment j, r < dist (J.vertex i) y) (i : ZMod J.n) : J.vertexForwardSector i r ⊆ Metric.ball (J.vertex i) r \ J.carrier

Either transported angular sector lies in its vertex ball and avoids the polygon, provided the ball sees only the two incident edges.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.vertexBackwardSector_subset_ball_diff_carrier (J : PolygonalCircle) {r : ℝ} (hsep : ∀ (i j : ZMod J.n), i ≠ j → i ≠ j + 1 → ∀ y ∈ J.edgeSegment j, r < dist (J.vertex i) y) (i : ZMod J.n) : J.vertexBackwardSector i r ⊆ Metric.ball (J.vertex i) r \ J.carrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.vertex_add_symm_mem_segment_of_mem_openRadialRay {p u : Plane} (hu : u ≠ 0) {r : ℝ} (hr : r ≤ ‖u‖) {z : ℂ} (hz : z ∈ openRadialRay (complexDirection (planeComplexEquiv u) ⋯) r) : p + planeComplexEquiv.symm z ∈ segment ℝ p (p + u)

A short radial ray in the direction of u transports into the segment from p to p + u.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ball_diff_carrier_eq_vertexSectors (J : PolygonalCircle) {r : ℝ} (hsep : ∀ (i j : ZMod J.n), i ≠ j → i ≠ j + 1 → ∀ y ∈ J.edgeSegment j, r < dist (J.vertex i) y) (hlen : ∀ (i : ZMod J.n), r < dist (J.vertex i) (J.vertex (i + 1))) (i : ZMod J.n) : Metric.ball (J.vertex i) r \ J.carrier = J.vertexForwardSector i r ∪ J.vertexBackwardSector i r

The punctured vertex ball is exactly the union of its two angular sectors.

Rectangular coordinates along an edge

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeLength (J : PolygonalCircle) (i : ZMod J.n) : ℝ

Length of edge i.

Equations

• J.edgeLength i = ‖J.outgoingVector i‖

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeLength_pos (J : PolygonalCircle) (i : ZMod J.n) : 0 < J.edgeLength i

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeCoordinate (J : PolygonalCircle) (i : ZMod J.n) (x : Plane) : ℂ

Complex coordinates centered at the initial vertex and divided by the oriented unit edge direction. The edge itself is the real interval from 0 to edgeLength.

Equations

• J.edgeCoordinate i x = LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.planeComplexEquiv (x - J.vertex i) / ↑(J.outgoingDirection i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeCoordinateInv (J : PolygonalCircle) (i : ZMod J.n) (z : ℂ) : Plane

Inverse edge coordinates.

Equations

• J.edgeCoordinateInv i z = J.vertex i + LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.planeComplexEquiv.symm (z * ↑(J.outgoingDirection i))

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeCoordinate_edgeCoordinateInv (J : PolygonalCircle) (i : ZMod J.n) (z : ℂ) : J.edgeCoordinate i (J.edgeCoordinateInv i z) = z

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeCoordinateInv_edgeCoordinate (J : PolygonalCircle) (i : ZMod J.n) (x : Plane) : J.edgeCoordinateInv i (J.edgeCoordinate i x) = x

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeCoordinate_initial (J : PolygonalCircle) (i : ZMod J.n) : J.edgeCoordinate i (J.vertex i) = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeCoordinate_terminal (J : PolygonalCircle) (i : ZMod J.n) : J.edgeCoordinate i (J.vertex (i + 1)) = ↑(J.edgeLength i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeTube (J : PolygonalCircle) (i : ZMod J.n) (trim width : ℝ) : Set Plane

An open rectangular tube around the central part of edge i.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgePositiveSide (J : PolygonalCircle) (i : ZMod J.n) (trim width : ℝ) : Set Plane

The positive-imaginary half of the edge tube.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeNegativeSide (J : PolygonalCircle) (i : ZMod J.n) (trim width : ℝ) : Set Plane

The negative-imaginary half of the edge tube.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.continuous_edgeCoordinate (J : PolygonalCircle) (i : ZMod J.n) : Continuous (J.edgeCoordinate i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isOpen_edgeTube (J : PolygonalCircle) (i : ZMod J.n) (trim width : ℝ) : IsOpen (J.edgeTube i trim width)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgePositiveSide_subset_edgeTube (J : PolygonalCircle) (i : ZMod J.n) {trim width : ℝ} (hwidth : 0 < width) : J.edgePositiveSide i trim width ⊆ J.edgeTube i trim width

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeNegativeSide_subset_edgeTube (J : PolygonalCircle) (i : ZMod J.n) {trim width : ℝ} (hwidth : 0 < width) : J.edgeNegativeSide i trim width ⊆ J.edgeTube i trim width

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isPathConnected_edgePositiveSide (J : PolygonalCircle) (i : ZMod J.n) {trim width : ℝ} (hwidth : 0 < width) (hlen : 4 * trim < J.edgeLength i) : IsPathConnected (J.edgePositiveSide i trim width)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isPathConnected_edgeNegativeSide (J : PolygonalCircle) (i : ZMod J.n) {trim width : ℝ} (hwidth : 0 < width) (hlen : 4 * trim < J.edgeLength i) : IsPathConnected (J.edgeNegativeSide i trim width)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeAxis_mem_closure_positiveSide (J : PolygonalCircle) (i : ZMod J.n) {trim width s : ℝ} (hwidth : 0 < width) (hlen : 4 * trim < J.edgeLength i) (hs : s ∈ Set.Icc (2 * trim) (J.edgeLength i - 2 * trim)) : J.edgeCoordinateInv i ↑s ∈ closure (J.edgePositiveSide i trim width)

The central edge axis is approached from the positive side rectangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeAxis_mem_closure_negativeSide (J : PolygonalCircle) (i : ZMod J.n) {trim width s : ℝ} (hwidth : 0 < width) (hlen : 4 * trim < J.edgeLength i) (hs : s ∈ Set.Icc (2 * trim) (J.edgeLength i - 2 * trim)) : J.edgeCoordinateInv i ↑s ∈ closure (J.edgeNegativeSide i trim width)

The central edge axis is approached from the negative side rectangle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeCoordinate_im_eq_zero_of_mem_edgeSegment (J : PolygonalCircle) (i : ZMod J.n) {x : Plane} (hx : x ∈ J.edgeSegment i) : (J.edgeCoordinate i x).im = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeTube_diff_carrier_eq_sides (J : PolygonalCircle) (i : ZMod J.n) {trim width : ℝ} (htrim : 0 < trim) (hwidth : 0 < width) (honly : J.edgeTube i trim width ∩ J.carrier ⊆ J.edgeSegment i) : J.edgeTube i trim width \ J.carrier = J.edgePositiveSide i trim width ∪ J.edgeNegativeSide i trim width

Removing the polygon from a central edge tube leaves exactly its positive and negative rectangular halves.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeSegment_inter_subset_endpoints (J : PolygonalCircle) {i j : ZMod J.n} (hij : i ≠ j) : J.edgeSegment i ∩ J.edgeSegment j ⊆ {J.vertex i, J.vertex (i + 1)}

Distinct polygon edges can meet only at an endpoint of the first edge.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.otherEdges (J : PolygonalCircle) (i : ZMod J.n) : Set Plane

The union of all polygon edges other than edge i.

Equations

• J.otherEdges i = ⋃ (j : ZMod J.n), ⋃ (_ : j ≠ i), J.edgeSegment j

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isCompact_otherEdges (J : PolygonalCircle) (i : ZMod J.n) : IsCompact (J.otherEdges i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isClosed_otherEdges (J : PolygonalCircle) (i : ZMod J.n) : IsClosed (J.otherEdges i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exists_ball_inter_carrier_subset_edgeSegment (J : PolygonalCircle) {i : ZMod J.n} {x : Plane} (hx : x ∈ openSegment ℝ (J.vertex i) (J.vertex (i + 1))) : ∃ (r : ℝ), 0 < r ∧ Metric.ball x r ∩ J.carrier ⊆ J.edgeSegment i

Near a relative-interior point of a polygon edge, the carrier consists only of that edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exists_basePoints_on_incident_edges (J : PolygonalCircle) {P Q : Plane} (hPQ : P ≠ Q) (hbase : segment ℝ P Q ⊆ J.carrier) {i : ZMod J.n} (hi : J.vertex i ∈ openSegment ℝ P Q) : (∃ (y : Plane), y ≠ J.vertex i ∧ y ∈ segment ℝ P Q ∧ y ∈ J.edgeSegment i) ∧ ∃ (y : Plane), y ≠ J.vertex i ∧ y ∈ segment ℝ P Q ∧ y ∈ J.edgeSegment (i - 1)

If a straight subsegment of the polygon carrier passes through a polygon vertex, its two local sides occupy the two incident polygon edges.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exists_second_basePoint_of_edge_inter_openSegment (J : PolygonalCircle) {P Q x : Plane} (hPQ : P ≠ Q) (hbase : segment ℝ P Q ⊆ J.carrier) {i : ZMod J.n} (hxEdge : x ∈ J.edgeSegment i) (hxBase : x ∈ openSegment ℝ P Q) : ∃ (y : Plane), y ≠ x ∧ y ∈ J.edgeSegment i ∧ y ∈ segment ℝ P Q

An edge meeting the relative interior of a straight subsegment of the carrier overlaps that subsegment in at least two points.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edge_endpoints_on_axis_of_inter_openBase (J : PolygonalCircle) {P Q : Plane} (hPQ : P ≠ Q) (hP0 : P.ofLp 1 = 0) (hQ0 : Q.ofLp 1 = 0) (hbase : segment ℝ P Q ⊆ J.carrier) {i : ZMod J.n} {x : Plane} (hxEdge : x ∈ J.edgeSegment i) (hxBase : x ∈ openSegment ℝ P Q) : (J.vertex i).ofLp 1 = 0 ∧ (J.vertex (i + 1)).ofLp 1 = 0

In normalized ear coordinates, every polygon edge meeting the open base lies on the horizontal base line.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.mem_edgeSegment_or_otherEdges (J : PolygonalCircle) {x : Plane} (hx : x ∈ J.carrier) (i : ZMod J.n) : x ∈ J.edgeSegment i ∨ x ∈ J.otherEdges i

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeCore (J : PolygonalCircle) (i : ZMod J.n) (trim : ℝ) : Set Plane

The closed central subsegment obtained by trimming 2 * trim from both endpoint coordinates.

Equations

• J.edgeCore i trim = (fun (s : ℝ) => J.edgeCoordinateInv i ↑s) '' Set.Icc (2 * trim) (J.edgeLength i - 2 * trim)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isCompact_edgeCore (J : PolygonalCircle) (i : ZMod J.n) (trim : ℝ) : IsCompact (J.edgeCore i trim)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeCore_subset_edgeSegment (J : PolygonalCircle) (i : ZMod J.n) {trim : ℝ} (htrim : 0 < trim) : 4 * trim < J.edgeLength i → J.edgeCore i trim ⊆ J.edgeSegment i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.disjoint_edgeCore_otherEdges (J : PolygonalCircle) (i : ZMod J.n) {trim : ℝ} (htrim : 0 < trim) (hlen : 4 * trim < J.edgeLength i) : Disjoint (J.edgeCore i trim) (J.otherEdges i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.dist_edgeCoordinateInv (J : PolygonalCircle) (i : ZMod J.n) (z w : ℂ) : dist (J.edgeCoordinateInv i z) (J.edgeCoordinateInv i w) = dist z w

Inverse edge coordinates preserve distances.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exists_edgeTube_width (J : PolygonalCircle) {trim : ℝ} (htrim : 0 < trim) (hlen : ∀ (i : ZMod J.n), 4 * trim < J.edgeLength i) : ∃ (width : ℝ), 0 < width ∧ width < trim ∧ ∀ (i : ZMod J.n), J.edgeTube i trim width ∩ J.carrier ⊆ J.edgeSegment i

After fixing a longitudinal trim, one can choose a uniform thinner transverse width so that every central edge tube meets the polygon only in its own edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeCoordinate_mem_real_Icc (J : PolygonalCircle) (i : ZMod J.n) {x : Plane} (hx : x ∈ J.edgeSegment i) : ∃ s ∈ Set.Icc 0 (J.edgeLength i), J.edgeCoordinate i x = ↑s

Points on an edge have a real edge coordinate between zero and the edge length.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.polygonStrip (J : PolygonalCircle) (trim width : ℝ) : Set Plane

The explicit open strip made from vertex balls and the isolated central edge tubes.

Equations

• J.polygonStrip trim width = (⋃ (i : ZMod J.n), Metric.ball (J.vertex i) (3 * trim)) ∪ ⋃ (i : ZMod J.n), J.edgeTube i trim width

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isOpen_polygonStrip (J : PolygonalCircle) (trim width : ℝ) : IsOpen (J.polygonStrip trim width)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.carrier_subset_polygonStrip (J : PolygonalCircle) {trim width : ℝ} (htrim : 0 < trim) (hwidth : 0 < width) : J.carrier ⊆ J.polygonStrip trim width

Vertex balls cover the endpoint portions of every edge and the central tube covers the remainder.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.StripScales (J : PolygonalCircle) : Type

Quantitative scales for the explicit polygon strip.

• trim : ℝ

  The trim declaration.

• width : ℝ

  The width declaration.

• trim_pos : 0 < self.trim
• width_pos : 0 < self.width
• width_lt_trim : self.width < self.trim
• edge_long (i : ZMod J.n) : 12 * self.trim < J.edgeLength i
• vertex_isolation (i j : ZMod J.n) : i ≠ j → i ≠ j + 1 → ∀ y ∈ J.edgeSegment j, 3 * self.trim < dist (J.vertex i) y
• tube_isolation (i : ZMod J.n) : J.edgeTube i self.trim self.width ∩ J.carrier ⊆ J.edgeSegment i

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exists_stripScales (J : PolygonalCircle) : Nonempty J.StripScales

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.stripForwardPieces (J : PolygonalCircle) (S : J.StripScales) : Set Plane

The forward vertex sectors and positive edge rectangles.

Equations

• J.stripForwardPieces S = (⋃ (i : ZMod J.n), J.vertexForwardSector i (3 * S.trim)) ∪ ⋃ (i : ZMod J.n), J.edgePositiveSide i S.trim S.width

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.stripBackwardPieces (J : PolygonalCircle) (S : J.StripScales) : Set Plane

The backward vertex sectors and negative edge rectangles.

Equations

• J.stripBackwardPieces S = (⋃ (i : ZMod J.n), J.vertexBackwardSector i (3 * S.trim)) ∪ ⋃ (i : ZMod J.n), J.edgeNegativeSide i S.trim S.width

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.polygonStrip_diff_carrier_eq_pieces (J : PolygonalCircle) (S : J.StripScales) : J.polygonStrip S.trim S.width \ J.carrier = J.stripForwardPieces S ∪ J.stripBackwardPieces S

The punctured explicit strip is exactly the union of all its local forward and backward pieces.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.StripScales.exists_edgeOverlapAngle (J : PolygonalCircle) (S : J.StripScales) (i : ZMod J.n) : ∃ (θ : ℝ), 0 < θ ∧ θ < Real.pi ∧ θ < (J.outgoingDirection i).angleDiff (J.incomingRayDirection i) ∧ θ < (J.incomingRayDirection i).angleDiff (J.outgoingDirection i) ∧ θ < (J.outgoingDirection (i + 1)).angleDiff (J.incomingRayDirection (i + 1)) ∧ θ < (J.incomingRayDirection (i + 1)).angleDiff (J.outgoingDirection (i + 1)) ∧ 2 * S.trim < (↑(5 * S.trim / 2) * ↑(Circle.exp θ)).re ∧ (↑(5 * S.trim / 2) * ↑(Circle.exp θ)).re < J.edgeLength i - 2 * S.trim ∧ |(↑(5 * S.trim / 2) * ↑(Circle.exp θ)).im| < S.width

A single sufficiently small positive angle gives overlap points for both sides of an edge at both endpoint vertex sectors.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.StripScales.initial_edge_side_intersections (J : PolygonalCircle) (S : J.StripScales) (i : ZMod J.n) : (J.vertexForwardSector i (3 * S.trim) ∩ J.edgePositiveSide i S.trim S.width).Nonempty ∧ (J.vertexBackwardSector i (3 * S.trim) ∩ J.edgeNegativeSide i S.trim S.width).Nonempty

The two side rectangles at the initial endpoint of an edge overlap the corresponding vertex sectors.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeCoordinate_terminal_ray (J : PolygonalCircle) (i : ZMod J.n) (z : ℂ) : J.edgeCoordinate i (J.vertex (i + 1) + planeComplexEquiv.symm (z * ↑(J.incomingRayDirection (i + 1)))) = ↑(J.edgeLength i) - z

Coordinates measured from an edge's terminal endpoint run in the opposite direction.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.StripScales.terminal_edge_side_intersections (J : PolygonalCircle) (S : J.StripScales) (i : ZMod J.n) : (J.vertexForwardSector (i + 1) (3 * S.trim) ∩ J.edgePositiveSide i S.trim S.width).Nonempty ∧ (J.vertexBackwardSector (i + 1) (3 * S.trim) ∩ J.edgeNegativeSide i S.trim S.width).Nonempty

The two side rectangles at the terminal endpoint of an edge overlap the corresponding vertex sectors.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isPathConnected_iUnion_of_reflTransGen {X : Type u_1} {ι : Type u_2} [TopologicalSpace X] [Nonempty ι] {s : ι → Set X} (hs : ∀ (i : ι), IsPathConnected (s i)) (hgraph : ∀ (i j : ι), Relation.ReflTransGen (fun (a b : ι) => (s a ∩ s b).Nonempty) i j) : IsPathConnected (⋃ (i : ι), s i)

A graph-connected union of path-connected sets is path-connected. This is the path analogue of IsConnected.iUnion_of_reflTransGen.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.StripScales.isPathConnected_stripForwardPieces (J : PolygonalCircle) (S : J.StripScales) : IsPathConnected (J.stripForwardPieces S)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.StripScales.isPathConnected_stripBackwardPieces (J : PolygonalCircle) (S : J.StripScales) : IsPathConnected (J.stripBackwardPieces S)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.StripScales.carrier_subset_closure_stripPieces (J : PolygonalCircle) (S : J.StripScales) : J.carrier ⊆ closure (J.stripForwardPieces S) ∩ closure (J.stripBackwardPieces S)

Every point of the polygon is approached from both of the explicit strip bands.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.StripScales.carrier_subset_closure_stripForwardPieces (J : PolygonalCircle) (S : J.StripScales) : J.carrier ⊆ closure (J.stripForwardPieces S)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.StripScales.carrier_subset_closure_stripBackwardPieces (J : PolygonalCircle) (S : J.StripScales) : J.carrier ⊆ closure (J.stripBackwardPieces S)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.interior_edgeSegment (J : PolygonalCircle) (i : ZMod J.n) : interior (J.edgeSegment i) = ∅

A genuine segment in the plane has empty planar interior.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.interior_carrier (J : PolygonalCircle) : interior J.carrier = ∅

A finite polygonal carrier has empty interior in the plane.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isConnected_carrier (J : PolygonalCircle) : IsConnected J.carrier

The carrier of a polygon is connected: it is a cyclic union of connected segments, with each segment meeting the next one at their common vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exists_segment_to_open_neighborhood (J : PolygonalCircle) {N : Set Plane} (hN : IsOpen N) (hcarrierN : J.carrier ⊆ N) {P : Plane} (hP : P ∉ J.carrier) : ∃ Q ∈ N \ J.carrier, segment ℝ P Q ⊆ J.carrierᶜ

Every point off the polygon can be joined by a single polygon-avoiding segment to any open neighborhood of the polygon. This is the "reach the strip" part of Moise Ch. 2, Thm. 1, Lemma 1.

The crossing index (Moise Ch. 2, proof of Thm. 1, Lemma 2)

The parity of the number of polygon edges crossed by the leftward horizontal ray from a point. We use the half-open edge convention (an edge is crossed when the point's height lies in the half-open interval between the endpoint heights): this replaces Moise's "slightly perturbed line" device, needs no general-position choice of axes, and makes the index everywhere defined. Horizontal edges are never crossed.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.crossingX (v w : Plane) (y : ℝ) : ℝ

The x-coordinate at height y of the line through v and w (meaningful when the heights of v and w differ, which the crossing condition guarantees at use sites).

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.crossingX v w y = v.ofLp 0 + (y - v.ofLp 1) / (w.ofLp 1 - v.ofLp 1) * (w.ofLp 0 - v.ofLp 0)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.EdgeCrossed (J : PolygonalCircle) (i : ZMod J.n) (P : Plane) : Prop

The leftward horizontal ray from P crosses edge i, with the half-open height convention.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.index (J : PolygonalCircle) (P : Plane) : ℕ

The Moise index of a point: the parity of the number of edges crossed by its leftward horizontal ray.

Equations

• J.index P = {i : ZMod J.n | J.EdgeCrossed i P}.card % 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.index_lt_two (J : PolygonalCircle) (P : Plane) : J.index P < 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.height_le_max_of_mem_segment {v w q : Plane} (hq : q ∈ segment ℝ v w) : q.ofLp 1 ≤ max (v.ofLp 1) (w.ofLp 1)

Points of a segment have heights between the endpoint heights.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.min_le_height_of_mem_segment {v w q : Plane} (hq : q ∈ segment ℝ v w) : min (v.ofLp 1) (w.ofLp 1) ≤ q.ofLp 1

Points of a segment have heights at least the smaller endpoint height.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.height_le_of_mem_carrier (J : PolygonalCircle) {q : Plane} (hq : q ∈ J.carrier) : ∃ (i : ZMod J.n), q.ofLp 1 ≤ (J.vertex i).ofLp 1

Points of the polygon have heights at most the maximal vertex height.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.index_eq_zero_of_high (J : PolygonalCircle) {P : Plane} (hP : ∀ (i : ZMod J.n), (J.vertex i).ofLp 1 < P.ofLp 1) : J.index P = 0

A point strictly above every vertex has index zero: its leftward ray crosses nothing.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.notMem_carrier_of_high (J : PolygonalCircle) {P : Plane} (hP : ∀ (i : ZMod J.n), (J.vertex i).ofLp 1 < P.ofLp 1) : P ∉ J.carrier

A point strictly above every vertex is off the polygon.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exists_index_eq_zero (J : PolygonalCircle) : ∃ P ∉ J.carrier, J.index P = 0

There are points off the polygon with index zero.

The handshake lemma for the local-constancy casework

Near a point P off the polygon, the only edges whose crossing status is not locally constant are those with exactly one endpoint at the height of P, that endpoint lying strictly to the left of P: rising edges switch on and falling edges switch off as the query point's height crosses P's. The index is therefore locally constant provided the number of such edges is even, which is a double-counting argument: every vertex has two incident edges, a horizontal partner of a left vertex is itself a left vertex (otherwise the horizontal edge would contain P), and so the non-horizontal incident edges of the left vertices pair up.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.mem_segment_of_horizontal {a b P : Plane} (ha : a.ofLp 1 = P.ofLp 1) (hb : b.ofLp 1 = P.ofLp 1) (hax : a.ofLp 0 ≤ P.ofLp 0) (hxb : P.ofLp 0 ≤ b.ofLp 0) : P ∈ segment ℝ a b

A point at the height of a horizontal segment, with abscissa between the endpoints, lies on the segment.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.leftVertices (J : PolygonalCircle) (P : Plane) : Finset (ZMod J.n)

The vertices at the height of P, strictly to its left.

Equations

• J.leftVertices P = {k : ZMod J.n | (J.vertex k).ofLp 1 = P.ofLp 1 ∧ (J.vertex k).ofLp 0 < P.ofLp 0}

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.upLeftEdges (J : PolygonalCircle) (P : Plane) : Finset (ZMod J.n)

Edges with one endpoint at the height of P and left of P, the other endpoint strictly above.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.downLeftEdges (J : PolygonalCircle) (P : Plane) : Finset (ZMod J.n)

Edges with one endpoint at the height of P and left of P, the other endpoint strictly below.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.left_of_horizontal_partner (J : PolygonalCircle) {P : Plane} (hP : P ∉ J.carrier) {k : ZMod J.n} (hk1 : (J.vertex k).ofLp 1 = P.ofLp 1) (hk0 : (J.vertex k).ofLp 0 < P.ofLp 0) {l : ZMod J.n} (hl1 : (J.vertex l).ofLp 1 = P.ofLp 1) (hedge : segment ℝ (J.vertex k) (J.vertex l) ⊆ J.carrier ∨ segment ℝ (J.vertex l) (J.vertex k) ⊆ J.carrier) : (J.vertex l).ofLp 0 < P.ofLp 0

The horizontal partner of a left vertex is a left vertex: otherwise the horizontal edge between them would contain P.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeSegment_subset_carrier (J : PolygonalCircle) (i : ZMod J.n) : segment ℝ (J.vertex i) (J.vertex (i + 1)) ⊆ J.carrier

Edge i (from vertex i to vertex i + 1) lies on the carrier.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.upLeft_card_add_downLeft_card_even (J : PolygonalCircle) {P : Plane} (hP : P ∉ J.carrier) : Even ((J.upLeftEdges P).card + (J.downLeftEdges P).card)

The handshake lemma: the flipping edges (up-left plus down-left) are even in number.

Per-edge behavior of the crossing status near a point off the polygon

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.continuous_coord (j : Fin 2) : Continuous fun (v : Plane) => v.ofLp j

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.continuous_crossingX (v w : Plane) : Continuous fun (Q : Plane) => crossingX v w (Q.ofLp 1)

The crossing abscissa depends continuously on the query point.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.crossingX_left (v w : Plane) : crossingX v w (v.ofLp 1) = v.ofLp 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.crossingX_right (v w : Plane) (hne : v.ofLp 1 ≠ w.ofLp 1) : crossingX v w (w.ofLp 1) = w.ofLp 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.mem_edgeSegment_of_crossing (J : PolygonalCircle) {P : Plane} (i : ZMod J.n) (hy : (J.vertex i).ofLp 1 ≤ P.ofLp 1 ∧ P.ofLp 1 < (J.vertex (i + 1)).ofLp 1 ∨ (J.vertex (i + 1)).ofLp 1 ≤ P.ofLp 1 ∧ P.ofLp 1 < (J.vertex i).ofLp 1) (hx : crossingX (J.vertex i) (J.vertex (i + 1)) (P.ofLp 1) = P.ofLp 0) : P ∈ J.edgeSegment i

A point whose height lies in an edge's band and whose abscissa is the crossing abscissa lies on that edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.mem_carrier_of_crossing (J : PolygonalCircle) {P : Plane} (i : ZMod J.n) (hy : (J.vertex i).ofLp 1 ≤ P.ofLp 1 ∧ P.ofLp 1 < (J.vertex (i + 1)).ofLp 1 ∨ (J.vertex (i + 1)).ofLp 1 ≤ P.ofLp 1 ∧ P.ofLp 1 < (J.vertex i).ofLp 1) (hx : crossingX (J.vertex i) (J.vertex (i + 1)) (P.ofLp 1) = P.ofLp 0) : P ∈ J.carrier

Carrier-level form of mem_edgeSegment_of_crossing.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.crossingX_eq_of_mem_edgeSegment (J : PolygonalCircle) {P : Plane} {i : ZMod J.n} (horiz : (J.vertex i).ofLp 1 ≠ (J.vertex (i + 1)).ofLp 1) (hP : P ∈ J.edgeSegment i) : crossingX (J.vertex i) (J.vertex (i + 1)) (P.ofLp 1) = P.ofLp 0

On a nonhorizontal edge, the crossing formula recovers the abscissa of every point of the edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.strict_height_band_of_mem_edgeSegment (J : PolygonalCircle) {P : Plane} {i : ZMod J.n} (hP : P ∈ J.edgeSegment i) (hheight : ∀ (k : ZMod J.n), P.ofLp 1 ≠ (J.vertex k).ofLp 1) : (J.vertex i).ofLp 1 < P.ofLp 1 ∧ P.ofLp 1 < (J.vertex (i + 1)).ofLp 1 ∨ (J.vertex (i + 1)).ofLp 1 < P.ofLp 1 ∧ P.ofLp 1 < (J.vertex i).ofLp 1

At a height different from both endpoint heights, a point of an edge lies strictly between those heights.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edge_eq_of_mem_edgeSegments_of_height_ne_vertices (J : PolygonalCircle) {P : Plane} {i j : ZMod J.n} (hi : P ∈ J.edgeSegment i) (hj : P ∈ J.edgeSegment j) (hheight : ∀ (k : ZMod J.n), P.ofLp 1 ≠ (J.vertex k).ofLp 1) : i = j

Two edges containing the same point away from all vertices are the same edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exists_nonhorizontal_edge (J : PolygonalCircle) : ∃ (i : ZMod J.n), (J.vertex i).ofLp 1 ≠ (J.vertex (i + 1)).ofLp 1

A polygon has a nonhorizontal edge. Otherwise, at a leftmost vertex the two incident horizontal edges overlap in more than their common endpoint.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.not_edgeCrossed_of_horizontal (J : PolygonalCircle) {i : ZMod J.n} (hAB : (J.vertex i).ofLp 1 = (J.vertex (i + 1)).ofLp 1) (R : Plane) : ¬J.EdgeCrossed i R

Horizontal edges are never crossed.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.eventually_edgeCrossed_iff (J : PolygonalCircle) {P : Plane} (hP : P ∉ J.carrier) (i : ZMod J.n) : ∀ᶠ (Q : Plane) in nhds P, J.EdgeCrossed i Q ↔ if i ∈ J.upLeftEdges P then P.ofLp 1 ≤ Q.ofLp 1 else if i ∈ J.downLeftEdges P then Q.ofLp 1 < P.ofLp 1 else J.EdgeCrossed i P

Near a point off the polygon, each edge's crossing status is: switched by the query height for the flipping edges, constant otherwise.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.index_locallyConstant (J : PolygonalCircle) {P : Plane} (hP : P ∉ J.carrier) : ∀ᶠ (Q : Plane) in nhds P, J.index Q = J.index P

Sub-boundary (Moise Ch. 2, Thm. 1, Lemma 2, local constancy of the index).

Off the polygon the crossing index is locally constant. The proof is elementary casework: for Q near P, the crossing status of each edge is unchanged unless the ray endpoint passes a vertex height, and at a vertex height the half-open convention makes the count change by 0 or 2 (the two edges at that vertex are both gained or both lost when they point to the same side, and exchanged when they point to opposite sides).

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exists_index_eq_one (J : PolygonalCircle) : ∃ P ∉ J.carrier, J.index P = 1

Sub-boundary (Moise Ch. 2, Thm. 1, Lemma 2, existence of an inside point).

Some point off the polygon has index one: take a height that is no vertex height but is attained by the polygon, let P₁ be the leftmost polygon point at that height, and move slightly right of P₁. (Moise's construction; requires knowing the polygon is not contained in a single horizontal line, which follows from the embedding fields.)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.indexRegion (J : PolygonalCircle) (k : ℕ) : Set Plane

The part of the polygon complement having crossing index k. Only k = 0, 1 are nonempty.

Equations

• J.indexRegion k = {P : LeanEval.Topology.ClassificationOfSurfaces.Moise.Plane | P ∉ J.carrier ∧ J.index P = k}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isOpen_indexRegion (J : PolygonalCircle) (k : ℕ) : IsOpen (J.indexRegion k)

Every index region is open, since the carrier is closed and the index is locally constant on its complement.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.indexRegion_zero_nonempty (J : PolygonalCircle) : (J.indexRegion 0).Nonempty

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.indexRegion_one_nonempty (J : PolygonalCircle) : (J.indexRegion 1).Nonempty

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.not_isBounded_indexRegion_zero (J : PolygonalCircle) : ¬Bornology.IsBounded (J.indexRegion 0)

The index-zero region is unbounded: it contains points arbitrarily high above the polygon.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.disjoint_indexRegion_zero_one (J : PolygonalCircle) : Disjoint (J.indexRegion 0) (J.indexRegion 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.indexRegion_zero_union_one (J : PolygonalCircle) : J.indexRegion 0 ∪ J.indexRegion 1 = J.carrierᶜ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.frontier_compl_carrier (J : PolygonalCircle) : frontier J.carrierᶜ = J.carrier

The polygon is the frontier of its full complement.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.frontier_indexRegion_zero_subset_carrier (J : PolygonalCircle) : frontier (J.indexRegion 0) ⊆ J.carrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.frontier_indexRegion_one_subset_carrier (J : PolygonalCircle) : frontier (J.indexRegion 1) ⊆ J.carrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.carrier_subset_frontier_indexRegion_union (J : PolygonalCircle) : J.carrier ⊆ frontier (J.indexRegion 0) ∪ frontier (J.indexRegion 1)

Every polygon point is approached by at least one of the two index sides. The remaining two-sided frontier step is to show that it is approached by both.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.index_eq_of_isPreconnected (J : PolygonalCircle) {s : Set Plane} (hs : IsPreconnected s) (hsub : s ⊆ J.carrierᶜ) {P Q : Plane} (hP : P ∈ s) (hQ : Q ∈ s) : J.index P = J.index Q

The crossing index is constant on every preconnected subset of the polygon complement.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.index_eq_of_joinedIn_compl (J : PolygonalCircle) {P Q : Plane} (h : JoinedIn J.carrierᶜ P Q) : J.index P = J.index Q

A path in the polygon complement has constant crossing index.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.JoinedIn.mono_indexRegion (J : PolygonalCircle) {N : Set Plane} {P Q : Plane} {k : ℕ} (h : JoinedIn (N \ J.carrier) P Q) (hindex : J.index P = k) : JoinedIn (N ∩ J.indexRegion k) P Q

A path in a neighborhood of the polygon complement whose initial point has index k stays in the index-k part of that neighborhood.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.TwoGateStrip (J : PolygonalCircle) : Type

The precise output needed from Moise's informal strip construction. The two gates are not labelled as inside and outside: every strip-complement point merely has to be path-joinable to one of them. The crossing index subsequently proves that the gates lie on different sides, so this interface also covers Moise's a priori "Möbius strip" possibility.

• strip : Set Plane

  The open strip neighborhood.

• isOpen_strip : IsOpen self.strip
• carrier_subset : J.carrier ⊆ self.strip
• gateA : Plane

  Two candidate path-component representatives.

• gateB : Plane

  The gateB declaration.

• gateA_mem : self.gateA ∈ self.strip \ J.carrier
• gateB_mem : self.gateB ∈ self.strip \ J.carrier
• reaches {P : Plane} : P ∈ self.strip \ J.carrier → JoinedIn (self.strip \ J.carrier) self.gateA P ∨ JoinedIn (self.strip \ J.carrier) self.gateB P

  Every point of the punctured strip reaches one of the two gates.

• gateA_approaches : J.carrier ⊆ closure {P : Plane | P ∈ self.strip \ J.carrier ∧ JoinedIn (self.strip \ J.carrier) self.gateA P}

  Both gate components accumulate on every point of the core polygon.

• gateB_approaches : J.carrier ⊆ closure {P : Plane | P ∈ self.strip \ J.carrier ∧ JoinedIn (self.strip \ J.carrier) self.gateB P}

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.StripScales.toTwoGateStrip (J : PolygonalCircle) (S : J.StripScales) : J.TwoGateStrip

The explicit polygon strip provides the two-gate local separation data used by the crossing index argument.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exists_twoGateStrip (J : PolygonalCircle) : Nonempty J.TwoGateStrip

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.TwoGateStrip.gateAComponent (J : PolygonalCircle) (S : J.TwoGateStrip) : Set Plane

The path component represented by the first gate, written as an ambient set.

Equations

• One or more equations did not get rendered due to their size.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.TwoGateStrip.gateBComponent (J : PolygonalCircle) (S : J.TwoGateStrip) : Set Plane

The path component represented by the second gate, written as an ambient set.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.TwoGateStrip.gateAComponent_subset_indexRegion (J : PolygonalCircle) (S : J.TwoGateStrip) {k : ℕ} (hk : J.index S.gateA = k) : gateAComponent J S ⊆ J.indexRegion k

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.TwoGateStrip.gateBComponent_subset_indexRegion (J : PolygonalCircle) (S : J.TwoGateStrip) {k : ℕ} (hk : J.index S.gateB = k) : gateBComponent J S ⊆ J.indexRegion k

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.TwoGateStrip.carrier_subset_frontier_indexRegion_of_gateA (J : PolygonalCircle) (S : J.TwoGateStrip) {k : ℕ} (hk : J.index S.gateA = k) : J.carrier ⊆ frontier (J.indexRegion k)

If gate A has index k, every carrier point belongs to the frontier of the index-k region.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.TwoGateStrip.carrier_subset_frontier_indexRegion_of_gateB (J : PolygonalCircle) (S : J.TwoGateStrip) {k : ℕ} (hk : J.index S.gateB = k) : J.carrier ⊆ frontier (J.indexRegion k)

If gate B has index k, every carrier point belongs to the frontier of the index-k region.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.indexRegion_inter_neighborhood_nonempty (J : PolygonalCircle) {N : Set Plane} (hN : IsOpen N) (hcarrierN : J.carrier ⊆ N) {k : ℕ} (hk : (J.indexRegion k).Nonempty) : (N ∩ J.indexRegion k).Nonempty

Every nonempty index region meets every open neighborhood of the polygon. A point is joined to the neighborhood by the visibility segment from exists_segment_to_open_neighborhood, and the index is constant on that segment.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.TwoGateStrip.index_gateA_ne_index_gateB (J : PolygonalCircle) (S : J.TwoGateStrip) : J.index S.gateA ≠ J.index S.gateB

The crossing index rules out the a priori possibility that the punctured strip has only one path component.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.TwoGateStrip.frontier_indexRegion_zero (J : PolygonalCircle) (S : J.TwoGateStrip) : frontier (J.indexRegion 0) = J.carrier

Every point of the polygon is approached from the index-zero gate component.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.TwoGateStrip.frontier_indexRegion_one (J : PolygonalCircle) (S : J.TwoGateStrip) : frontier (J.indexRegion 1) = J.carrier

Every point of the polygon is approached from the index-one gate component.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.TwoGateStrip.isPathConnected_indexRegion (J : PolygonalCircle) (S : J.TwoGateStrip) (k : ℕ) (hk : k = 0 ∨ k = 1) : IsPathConnected (S.strip ∩ J.indexRegion k)

The two index sides of a two-gate strip are path connected. This is the formal form of the last sentence in Moise Ch. 2, Thm. 1, Lemma 1: the index forces the two gates to represent the two different strip components.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isPreconnected_indexRegion_of_strip (J : PolygonalCircle) (k : ℕ) {N : Set Plane} (hN : IsOpen N) (hcarrierN : J.carrier ⊆ N) (hstrip : IsPreconnected (N ∩ J.indexRegion k)) : IsPreconnected (J.indexRegion k)

If one index side is preconnected inside an open strip neighborhood of the polygon, then the whole index side is preconnected. The proof joins arbitrary points to the strip using exists_segment_to_open_neighborhood.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isBounded_indexRegion_one (J : PolygonalCircle) : Bornology.IsBounded (J.indexRegion 1)

The index-one region is bounded. Outside a ball containing the polygon, every point lies on a large connected circle with a point above the polygon, where the index is zero.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.compl_carrier_not_isPreconnected (J : PolygonalCircle) : ¬IsPreconnected J.carrierᶜ

Moise Ch. 2, Thm. 1, Lemma 2: the complement of a polygon is disconnected. Proved from the index machinery: the index-0 and index-1 loci are relatively open (local constancy), cover the complement (the index is a parity), and are both nonempty.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.polygonal_jordan_of_twoGateStrip (J : PolygonalCircle) (S : J.TwoGateStrip) : ∃ (inside : Set Plane) (outside : Set Plane), IsOpen inside ∧ IsOpen outside ∧ Disjoint inside outside ∧ inside ∪ outside = J.carrierᶜ ∧ IsConnected inside ∧ IsConnected outside ∧ Bornology.IsBounded inside ∧ ¬Bornology.IsBounded outside ∧ frontier inside = J.carrier ∧ frontier outside = J.carrier

Once the explicit two-gate strip has been constructed, all global parts of polygonal Jordan follow from the crossing index and the visibility-to-strip lemma.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.polygonal_jordan (J : PolygonalCircle) : ∃ (inside : Set Plane) (outside : Set Plane), IsOpen inside ∧ IsOpen outside ∧ Disjoint inside outside ∧ inside ∪ outside = J.carrierᶜ ∧ IsConnected inside ∧ IsConnected outside ∧ Bornology.IsBounded inside ∧ ¬Bornology.IsBounded outside ∧ frontier inside = J.carrier ∧ frontier outside = J.carrier

Jordan curve theorem for polygons (Moise Ch. 2, Thms. 1, 5, 6).

The complement of a polygon has exactly two connected components: a bounded interior and an unbounded exterior, both open, and the polygon is the frontier of each.

Must-fail check: the statement forces interior ∪ exterior = carrierᶜ with both sides connected and the frontiers equal to the carrier, so it cannot be satisfied by choosing junk open sets.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.interiorRegion (J : PolygonalCircle) : Set Plane

The interior region of a polygon (the bounded complementary component).

Equations

• J.interiorRegion = ⋯.choose

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exteriorRegion (J : PolygonalCircle) : Set Plane

The exterior region of a polygon (the unbounded complementary component).

Equations

• J.exteriorRegion = ⋯.choose

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isOpen_interiorRegion (J : PolygonalCircle) : IsOpen J.interiorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isOpen_exteriorRegion (J : PolygonalCircle) : IsOpen J.exteriorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.disjoint_interior_exterior (J : PolygonalCircle) : Disjoint J.interiorRegion J.exteriorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.interior_union_exterior (J : PolygonalCircle) : J.interiorRegion ∪ J.exteriorRegion = J.carrierᶜ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isConnected_interiorRegion (J : PolygonalCircle) : IsConnected J.interiorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isConnected_exteriorRegion (J : PolygonalCircle) : IsConnected J.exteriorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isBounded_interiorRegion (J : PolygonalCircle) : Bornology.IsBounded J.interiorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.not_isBounded_exteriorRegion (J : PolygonalCircle) : ¬Bornology.IsBounded J.exteriorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.frontier_interiorRegion (J : PolygonalCircle) : frontier J.interiorRegion = J.carrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.frontier_exteriorRegion (J : PolygonalCircle) : frontier J.exteriorRegion = J.carrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exteriorRegion_eq_indexRegion_zero (J : PolygonalCircle) : J.exteriorRegion = J.indexRegion 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.interiorRegion_eq_indexRegion_one (J : PolygonalCircle) : J.interiorRegion = J.indexRegion 1

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.closedRegion (J : PolygonalCircle) : Set Plane

The closed region bounded by a polygon: the closure of its interior region.

Equations

• J.closedRegion = closure J.interiorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.closedRegion_eq_union (J : PolygonalCircle) : J.closedRegion = J.interiorRegion ∪ J.carrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isCompact_closedRegion (J : PolygonalCircle) : IsCompact J.closedRegion