Polygonal crosscuts

The set-theoretic part of Moise Chapter 2, Theorems 7 and 8. Three polygonal arcs with common endpoints form three polygons. When the third arc is a chord inside the first polygon, the two polygons containing the chord lie inside the first polygon. This is the cutting lemma used in the free-triangle induction of Chapter 3.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.segment_split_inter {a b p : Plane} (hp : p ∈ segment ℝ a b) (hpa : p ≠ a) (hpb : p ≠ b) : segment ℝ a p ∩ segment ℝ p b = {p}

Splitting a nondegenerate segment at a non-endpoint produces two subsegments meeting only at the split point.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.insertZeroVertex (J : PolygonalCircle) (p : Plane) : ZMod (J.n + 1) → Plane

Vertex sequence obtained by inserting p in edge zero. Its cyclic order is p, v₁, ..., vₙ₋₁, v₀.

Equations

• J.insertZeroVertex p i = if i.val = 0 then p else J.vertex ↑i.val

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.insertZeroVertex_zero (J : PolygonalCircle) (p : Plane) : J.insertZeroVertex p 0 = p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.insertZeroVertex_natCast (J : PolygonalCircle) (p : Plane) {m : ℕ} (hm0 : 0 < m) (hm : m < J.n + 1) : J.insertZeroVertex p ↑m = J.vertex ↑m

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.insertZeroEdgeSegment (J : PolygonalCircle) (p : Plane) (i : ZMod (J.n + 1)) : Set Plane

The prospective edges of insertZero, before packaging the simple-polygon proofs.

Equations

• J.insertZeroEdgeSegment p i = segment ℝ (J.insertZeroVertex p i) (J.insertZeroVertex p (i + 1))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.insertZeroEdgeSegment_zero (J : PolygonalCircle) (p : Plane) : J.insertZeroEdgeSegment p 0 = segment ℝ p (J.vertex 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.insertZeroEdgeSegment_middle (J : PolygonalCircle) (p : Plane) {m : ℕ} (hm0 : 0 < m) (hm : m < J.n) : J.insertZeroEdgeSegment p ↑m = J.edgeSegment ↑m

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.insertZeroEdgeSegment_last (J : PolygonalCircle) (p : Plane) : J.insertZeroEdgeSegment p ↑J.n = segment ℝ (J.vertex 0) p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.insertZeroVertex_adjacent_ne (J : PolygonalCircle) {p : Plane} (hp0 : p ≠ J.vertex 0) (hp1 : p ≠ J.vertex 1) (i : ZMod (J.n + 1)) : J.insertZeroVertex p i ≠ J.insertZeroVertex p (i + 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.insertZero_consecutive_inter (J : PolygonalCircle) {p : Plane} (hp : p ∈ J.edgeSegment 0) (hp0 : p ≠ J.vertex 0) (hp1 : p ≠ J.vertex 1) (i : ZMod (J.n + 1)) : J.insertZeroEdgeSegment p i ∩ J.insertZeroEdgeSegment p (i + 1) = {J.insertZeroVertex p (i + 1)}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.vertex_zero_not_mem_insertZero_first (J : PolygonalCircle) {p : Plane} (hp : p ∈ J.edgeSegment 0) (hp0 : p ≠ J.vertex 0) (hp1 : p ≠ J.vertex 1) : J.vertex 0 ∉ segment ℝ p (J.vertex 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.vertex_one_not_mem_insertZero_last (J : PolygonalCircle) {p : Plane} (hp : p ∈ J.edgeSegment 0) (hp0 : p ≠ J.vertex 0) (hp1 : p ≠ J.vertex 1) : J.vertex 1 ∉ segment ℝ (J.vertex 0) p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.disjoint_insertZero_first_previous (J : PolygonalCircle) {p : Plane} (hp : p ∈ J.edgeSegment 0) (hp0 : p ≠ J.vertex 0) (hp1 : p ≠ J.vertex 1) : Disjoint (segment ℝ p (J.vertex 1)) (J.edgeSegment ↑(J.n - 1))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.disjoint_insertZero_last_next (J : PolygonalCircle) {p : Plane} (hp : p ∈ J.edgeSegment 0) (hp0 : p ≠ J.vertex 0) (hp1 : p ≠ J.vertex 1) : Disjoint (segment ℝ (J.vertex 0) p) (J.edgeSegment 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.insertZero_first_subset_edge_zero (J : PolygonalCircle) {p : Plane} (hp : p ∈ J.edgeSegment 0) : segment ℝ p (J.vertex 1) ⊆ J.edgeSegment 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.insertZero_last_subset_edge_zero (J : PolygonalCircle) {p : Plane} (hp : p ∈ J.edgeSegment 0) : segment ℝ (J.vertex 0) p ⊆ J.edgeSegment 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.insertZero_nonadjacent_disjoint (J : PolygonalCircle) {p : Plane} (hp : p ∈ J.edgeSegment 0) (hp0 : p ≠ J.vertex 0) (hp1 : p ≠ J.vertex 1) (i j : ZMod (J.n + 1)) (hij : i ≠ j) (hprev : i ≠ j + 1) (hnext : j ≠ i + 1) : J.insertZeroEdgeSegment p i ∩ J.insertZeroEdgeSegment p j = ∅

Splitting edge zero preserves disjointness of every pair of non-adjacent edges.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.segment_split_union {a b p : Plane} (hp : p ∈ segment ℝ a b) : segment ℝ a p ∪ segment ℝ p b = segment ℝ a b

A point on a segment splits it into two subsegments whose union is the original segment.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.insertZero (J : PolygonalCircle) (p : Plane) (hp : p ∈ J.edgeSegment 0) (hp0 : p ≠ J.vertex 0) (hp1 : p ≠ J.vertex 1) : PolygonalCircle

Subdivide edge zero at a non-endpoint. The cyclic order is p, v₁, ..., vₙ₋₁, v₀.

Equations

• J.insertZero p hp hp0 hp1 = { n := J.n + 1, three_le := ⋯, vertex := J.insertZeroVertex p, adjacent_ne := ⋯, consecutive_inter := ⋯, nonadjacent_disjoint := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.insertZero_n (J : PolygonalCircle) (p : Plane) (hp : p ∈ J.edgeSegment 0) (hp0 : p ≠ J.vertex 0) (hp1 : p ≠ J.vertex 1) : (J.insertZero p hp hp0 hp1).n = J.n + 1

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.insertZero_vertex_zero (J : PolygonalCircle) (p : Plane) (hp : p ∈ J.edgeSegment 0) (hp0 : p ≠ J.vertex 0) (hp1 : p ≠ J.vertex 1) : (J.insertZero p hp hp0 hp1).vertex 0 = p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.insertZero_carrier (J : PolygonalCircle) (p : Plane) (hp : p ∈ J.edgeSegment 0) (hp0 : p ≠ J.vertex 0) (hp1 : p ≠ J.vertex 1) : (J.insertZero p hp hp0 hp1).carrier = J.carrier

Inserting a vertex into an edge does not change the polygon carrier.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.rotate (J : PolygonalCircle) (a : ZMod J.n) : PolygonalCircle

Cyclically reindex a polygon so that the old index a becomes the new index zero.

Equations

• J.rotate a = { n := J.n, three_le := ⋯, vertex := fun (i : ZMod J.n) => J.vertex (i + a), adjacent_ne := ⋯, consecutive_inter := ⋯, nonadjacent_disjoint := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.rotate_n (J : PolygonalCircle) (a : ZMod J.n) : (J.rotate a).n = J.n

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.rotate_vertex (J : PolygonalCircle) (a i : ZMod J.n) : (J.rotate a).vertex i = J.vertex (i + a)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.rotate_edgeSegment (J : PolygonalCircle) (a i : ZMod J.n) : (J.rotate a).edgeSegment i = J.edgeSegment (i + a)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.rotate_carrier (J : PolygonalCircle) (a : ZMod J.n) : (J.rotate a).carrier = J.carrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.regions_eq_of_carrier_eq {J J' : PolygonalCircle} (hcarrier : J.carrier = J'.carrier) : J.interiorRegion = J'.interiorRegion ∧ J.exteriorRegion = J'.exteriorRegion

The bounded and unbounded complementary components depend only on the polygon carrier, not on its cyclic indexing.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.rotate_interiorRegion (J : PolygonalCircle) (a : ZMod J.n) : (J.rotate a).interiorRegion = J.interiorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.rotate_exteriorRegion (J : PolygonalCircle) (a : ZMod J.n) : (J.rotate a).exteriorRegion = J.exteriorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.insertZero_interiorRegion (J : PolygonalCircle) (p : Plane) (hp : p ∈ J.edgeSegment 0) (hp0 : p ≠ J.vertex 0) (hp1 : p ≠ J.vertex 1) : (J.insertZero p hp hp0 hp1).interiorRegion = J.interiorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.insertZero_exteriorRegion (J : PolygonalCircle) (p : Plane) (hp : p ∈ J.edgeSegment 0) (hp0 : p ≠ J.vertex 0) (hp1 : p ≠ J.vertex 1) : (J.insertZero p hp hp0 hp1).exteriorRegion = J.exteriorRegion

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.IsVertexPoint (J : PolygonalCircle) (p : Plane) : Prop

A point is a vertex of one of the cyclic presentations of a polygon.

Equations

• J.IsVertexPoint p = ∃ (i : ZMod J.n), J.vertex i = p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.IsVertexPoint.mem_edgeSegment_iff {J : PolygonalCircle} {p : Plane} (hp : J.IsVertexPoint p) (i : ZMod J.n) : p ∈ J.edgeSegment i ↔ p = J.vertex i ∨ p = J.vertex (i + 1)

A point known to be a polygon vertex lies on an edge exactly when it is one of that edge's two endpoints.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isVertexPoint_rotate_iff (J : PolygonalCircle) (a : ZMod J.n) (p : Plane) : (J.rotate a).IsVertexPoint p ↔ J.IsVertexPoint p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.isVertexPoint_insertZero (J : PolygonalCircle) (p : Plane) (hp : p ∈ J.edgeSegment 0) (hp0 : p ≠ J.vertex 0) (hp1 : p ≠ J.vertex 1) {q : Plane} (hq : J.IsVertexPoint q) : (J.insertZero p hp hp0 hp1).IsVertexPoint q

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exists_refinement_vertex_zero (J : PolygonalCircle) {p : Plane} (hp : p ∈ J.carrier) : ∃ (J' : PolygonalCircle), J'.carrier = J.carrier ∧ J'.vertex 0 = p ∧ ∀ (q : Plane), J.IsVertexPoint q → J'.IsVertexPoint q

Insert a boundary point as vertex zero without changing the carrier, while retaining every old vertex. Endpoint cases need only a cyclic reindexing; an interior edge point uses insertZero.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.exists_refinement_vertices (J : PolygonalCircle) (F : Finset Plane) (hF : ∀ p ∈ F, p ∈ J.carrier) : ∃ (J' : PolygonalCircle), J'.carrier = J.carrier ∧ ∀ p ∈ F, J'.IsVertexPoint p

Refine a polygonal presentation so that every point of a prescribed finite subset of its carrier is a polygon vertex, without changing the carrier.

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

A straight crosscut of a polygonal disk: its endpoints lie on the polygon, while every other point of the segment lies in the polygon interior.

• P : Plane

  The P declaration.

• Q : Plane

  The Q declaration.

• ne : self.P ≠ self.Q
• P_mem : self.P ∈ J.carrier
• Q_mem : self.Q ∈ J.carrier
• interior_subset : segment ℝ self.P self.Q \ {self.P, self.Q} ⊆ J.interiorRegion

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.congrCarrier {J : PolygonalCircle} (C : J.ProperChord) {J' : PolygonalCircle} (hcarrier : J'.carrier = J.carrier) : J'.ProperChord

Transport a proper chord across a different cyclic polygon presentation with the same carrier.

Equations

• C.congrCarrier hcarrier = { P := C.P, Q := C.Q, ne := ⋯, P_mem := ⋯, Q_mem := ⋯, interior_subset := ⋯ }

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.rotate {J : PolygonalCircle} (C : J.ProperChord) (a : ZMod J.n) : (J.rotate a).ProperChord

Reindexing the boundary polygon does not change a proper chord.

Equations

• C.rotate a = { P := C.P, Q := C.Q, ne := ⋯, P_mem := ⋯, Q_mem := ⋯, interior_subset := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.segment_inter_carrier {J : PolygonalCircle} (C : J.ProperChord) : segment ℝ C.P C.Q ∩ J.carrier = {C.P, C.Q}

The chord meets the original polygon precisely at its endpoints.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.interior_nonempty {J : PolygonalCircle} (C : J.ProperChord) : (segment ℝ C.P C.Q \ {C.P, C.Q}).Nonempty

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.exists_endpoint_edges {J : PolygonalCircle} (C : J.ProperChord) : ∃ (i : ZMod J.n) (j : ZMod J.n), C.P ∈ J.edgeSegment i ∧ C.Q ∈ J.edgeSegment j

Each endpoint of a proper chord lies on a concrete polygon edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.endpoint_edges_ne {J : PolygonalCircle} (C : J.ProperChord) {i j : ZMod J.n} (hi : C.P ∈ J.edgeSegment i) (hj : C.Q ∈ J.edgeSegment j) : i ≠ j

The endpoints of a proper chord cannot lie on one polygon edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.exists_rotated_endpoint_edges {J : PolygonalCircle} (C : J.ProperChord) : ∃ (a : ZMod J.n) (k : ℕ), 0 < k ∧ k < J.n ∧ C.P ∈ (J.rotate a).edgeSegment 0 ∧ C.Q ∈ (J.rotate a).edgeSegment ↑k

Normalize a proper chord so that its first endpoint lies on edge zero and its second endpoint lies on an edge with a positive ordinary index.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.exists_vertex_normalization {J : PolygonalCircle} (C : J.ProperChord) : ∃ (J' : PolygonalCircle) (k : ℕ), 2 ≤ k ∧ k + 1 < J'.n ∧ J'.carrier = J.carrier ∧ J'.vertex 0 = C.P ∧ J'.vertex ↑k = C.Q ∧ ∃ (C' : J'.ProperChord), C'.P = C.P ∧ C'.Q = C.Q

After subdividing boundary edges and cyclically reindexing, both chord endpoints are vertices, with the first at index zero and the second at a strictly positive ordinary index.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.symm {J : PolygonalCircle} (C : J.ProperChord) : J.ProperChord

Reverse the orientation of a proper chord.

Equations

• C.symm = { P := C.Q, Q := C.P, ne := ⋯, P_mem := ⋯, Q_mem := ⋯, interior_subset := ⋯ }

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardCutVertex {J : PolygonalCircle} (k : ℕ) : ZMod (k + 1) → Plane

Vertex sequence for the polygon consisting of vertices 0,...,k and the closing chord.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardCutVertex k i = J.vertex ↑i.val

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardCutVertex_natCast {J : PolygonalCircle} {k m : ℕ} (hm : m < k + 1) : forwardCutVertex k ↑m = J.vertex ↑m

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.edgeBeforeChord_inter_chord {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hk2 : 2 ≤ k) (hk : k + 1 < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) : J.edgeSegment ↑(k - 1) ∩ segment ℝ C.Q C.P = {C.Q}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.chord_inter_firstEdge {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hk2 : 2 ≤ k) (hk : k + 1 < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) : segment ℝ C.Q C.P ∩ J.edgeSegment 0 = {C.P}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.chord_disjoint_middleEdge {J : PolygonalCircle} (C : J.ProperChord) {k m : ℕ} (hm0 : 0 < m) (hmk : m + 1 < k) (hk : k < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) : Disjoint (segment ℝ C.Q C.P) (J.edgeSegment ↑m)

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardCutEdgeSegment {J : PolygonalCircle} (k : ℕ) (i : ZMod (k + 1)) : Set Plane

The forwardCutEdgeSegment declaration.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardCutEdgeSegment_of_lt {J : PolygonalCircle} {k m : ℕ} (hm : m < k) : forwardCutEdgeSegment k ↑m = J.edgeSegment ↑m

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardCutEdgeSegment_last {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} : k < J.n → ∀ (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q), forwardCutEdgeSegment k ↑k = segment ℝ C.Q C.P

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardCutVertex_adjacent_ne {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} : 2 ≤ k → k < J.n → ∀ (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) (i : ZMod (k + 1)), forwardCutVertex k i ≠ forwardCutVertex k (i + 1)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardCut_consecutive_inter {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hk2 : 2 ≤ k) (hk : k + 1 < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) (i : ZMod (k + 1)) : forwardCutEdgeSegment k i ∩ forwardCutEdgeSegment k (i + 1) = {forwardCutVertex k (i + 1)}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardCut_nonadjacent_disjoint {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hk2 : 2 ≤ k) (hk : k + 1 < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) (i j : ZMod (k + 1)) (hij : i ≠ j) (hprev : i ≠ j + 1) (hnext : j ≠ i + 1) : forwardCutEdgeSegment k i ∩ forwardCutEdgeSegment k j = ∅

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardCutCircle {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hk2 : 2 ≤ k) (hk : k + 1 < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) : PolygonalCircle

Close the forward boundary arc from vertex 0 to vertex k by a proper chord.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardArc {J : PolygonalCircle} (k : ℕ) : Set Plane

The forward boundary arc consisting of old edges 0,...,k-1.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardArc k = ⋃ (m : Fin k), J.edgeSegment ↑↑m

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardCutCircle_carrier {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hk2 : 2 ≤ k) (hk : k + 1 < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) : (C.forwardCutCircle hk2 hk hP hQ).carrier = forwardArc k ∪ segment ℝ C.Q C.P

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.endpoints_mem_forwardArc {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hk2 : 2 ≤ k) : k < J.n → ∀ (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q), C.P ∈ forwardArc k ∧ C.Q ∈ forwardArc k

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardArc_interior_nonempty {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hk2 : 2 ≤ k) : k < J.n → ∀ (hP : J.vertex 0 = C.P), J.vertex ↑k = C.Q → (forwardArc k \ {C.P, C.Q}).Nonempty

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardArc_subset_carrier {J : PolygonalCircle} {k : ℕ} : forwardArc k ⊆ J.carrier

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.backwardArc {J : PolygonalCircle} (k : ℕ) : Set Plane

The complementary boundary arc, expressed as a forward arc after rotating vertex k to index zero.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.backwardArc k = LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardArc (J.n - k)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.backwardArc_subset_carrier {J : PolygonalCircle} {k : ℕ} : backwardArc k ⊆ J.carrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.rotate_edgeSegment_nat {J : PolygonalCircle} {k m : ℕ} : k < J.n → m + k < J.n → (J.rotate ↑k).edgeSegment ↑m = J.edgeSegment (↑m + ↑k)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardArc_union_backwardArc {J : PolygonalCircle} {k : ℕ} (hk : k < J.n) : forwardArc k ∪ backwardArc k = J.carrier

The two cyclic boundary arcs cover the original polygon carrier.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.endpoints_mem_backwardArc {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hkpos : 0 < k) (hk2 : k + 1 < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) : C.P ∈ backwardArc k ∧ C.Q ∈ backwardArc k

The complementary arc has the same two endpoints as the forward arc.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardArc_inter_chord {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hk2 : 2 ≤ k) (hk : k < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) : forwardArc k ∩ segment ℝ C.P C.Q = {C.P, C.Q}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.backwardArc_inter_chord {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hk2 : 2 ≤ k) (hk : k + 1 < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) : backwardArc k ∩ segment ℝ C.P C.Q = {C.P, C.Q}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardArc_inter_backwardArc {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hk2 : 2 ≤ k) (hk : k + 1 < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) : forwardArc k ∩ backwardArc k = {C.P, C.Q}

The two complementary cyclic boundary arcs meet only at their endpoints.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.backwardCutCircle {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hk2 : 2 ≤ k) (hk : k + 1 < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) : PolygonalCircle

Close the complementary boundary arc by the same chord, using a cyclic rotation.

Equations

• C.backwardCutCircle hk2 hk hP hQ = (C.symm.rotate ↑k).forwardCutCircle ⋯ ⋯ ⋯ ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.backwardCutCircle_carrier {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hk2 : 2 ≤ k) (hk : k + 1 < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) : (C.backwardCutCircle hk2 hk hP hQ).carrier = backwardArc k ∪ segment ℝ C.P C.Q

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.backwardArc_interior_nonempty {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hk2 : 2 ≤ k) (hk : k + 1 < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) : (backwardArc k \ {C.P, C.Q}).Nonempty

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.SegmentCrossed (v w P : Plane) : Prop

Crossing predicate for one oriented segment, separated from cyclic indexing.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.edgeCrossed_iff_segmentCrossed (J : PolygonalCircle) (i : ZMod J.n) (P : Plane) : J.EdgeCrossed i P ↔ SegmentCrossed (J.vertex i) (J.vertex (i + 1)) P

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.crossingX_comm {v w : Plane} {y : ℝ} (h : v.ofLp 1 ≠ w.ofLp 1) : crossingX v w y = crossingX w v y

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.segmentCrossed_comm (v w P : Plane) : SegmentCrossed v w P ↔ SegmentCrossed w v P

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

Number of crossed polygon edges before reducing modulo two, indexed by ordinary naturals.

Equations

• J.crossingCount P = ∑ m ∈ Finset.range J.n, if J.EdgeCrossed (↑m) P then 1 else 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.index_eq_crossingCount_mod (J : PolygonalCircle) (P : Plane) : J.index P = J.crossingCount P % 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.rotate_edgeCrossed_iff (J : PolygonalCircle) (a i : ZMod J.n) (P : Plane) : (J.rotate a).EdgeCrossed i P ↔ J.EdgeCrossed (i + a) P

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardCutCircle_edgeCrossed_of_lt {J : PolygonalCircle} (C : J.ProperChord) {k m : ℕ} (hk2 : 2 ≤ k) (hk : k + 1 < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) (hm : m < k) (P : Plane) : (C.forwardCutCircle hk2 hk hP hQ).EdgeCrossed (↑m) P ↔ J.EdgeCrossed (↑m) P

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.forwardCutCircle_edgeCrossed_last {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hk2 : 2 ≤ k) (hk : k + 1 < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) (P : Plane) : (C.forwardCutCircle hk2 hk hP hQ).EdgeCrossed (↑k) P ↔ SegmentCrossed C.P C.Q P

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.crossingCount_forwardCutCircle {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hk2 : 2 ≤ k) (hk : k + 1 < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) (P : Plane) : (C.forwardCutCircle hk2 hk hP hQ).crossingCount P = (∑ m ∈ Finset.range k, if J.EdgeCrossed (↑m) P then 1 else 0) + if SegmentCrossed C.P C.Q P then 1 else 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.crossingCount_backwardCutCircle {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hk2 : 2 ≤ k) (hk : k + 1 < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) (P : Plane) : (C.backwardCutCircle hk2 hk hP hQ).crossingCount P = (∑ m ∈ Finset.range (J.n - k), if J.EdgeCrossed (↑(m + k)) P then 1 else 0) + if SegmentCrossed C.P C.Q P then 1 else 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.index_parity_cutCircles {J : PolygonalCircle} (C : J.ProperChord) {k : ℕ} (hk2 : 2 ≤ k) (hk : k + 1 < J.n) (hP : J.vertex 0 = C.P) (hQ : J.vertex ↑k = C.Q) (P : Plane) : J.index P = ((C.forwardCutCircle hk2 hk hP hQ).index P + (C.backwardCutCircle hk2 hk hP hQ).index P) % 2

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

The carrier data of a polygonal theta graph. J12, J13, and J23 are the polygons formed by the indicated pairs of arcs.

• P : Plane

  The P declaration.

• Q : Plane

  The Q declaration.

• B1 : Set Plane

  The B1 declaration.

• B2 : Set Plane

  The B2 declaration.

• B3 : Set Plane

  The B3 declaration.

• J12 : PolygonalCircle

  The J12 declaration.

• J13 : PolygonalCircle

  The J13 declaration.

• J23 : PolygonalCircle

  The J23 declaration.

• P_mem_B1 : self.P ∈ self.B1
• Q_mem_B1 : self.Q ∈ self.B1
• P_mem_B2 : self.P ∈ self.B2
• Q_mem_B2 : self.Q ∈ self.B2
• P_mem_B3 : self.P ∈ self.B3
• Q_mem_B3 : self.Q ∈ self.B3
• B1_inter_B2 : self.B1 ∩ self.B2 = {self.P, self.Q}
• B1_inter_B3 : self.B1 ∩ self.B3 = {self.P, self.Q}
• B2_inter_B3 : self.B2 ∩ self.B3 = {self.P, self.Q}
• carrier12 : self.J12.carrier = self.B1 ∪ self.B2
• carrier13 : self.J13.carrier = self.B1 ∪ self.B3
• carrier23 : self.J23.carrier = self.B2 ∪ self.B3
• chord_subset : self.B3 ⊆ {self.P, self.Q} ∪ self.J12.interiorRegion
• B1_interior_nonempty : (self.B1 \ {self.P, self.Q}).Nonempty
• B2_interior_nonempty : (self.B2 \ {self.P, self.Q}).Nonempty
• chord_interior_nonempty : (self.B3 \ {self.P, self.Q}).Nonempty
• index_parity (x : Plane) : x ∉ self.J12.carrier → x ∉ self.J13.carrier → x ∉ self.J23.carrier → self.J12.index x = (self.J13.index x + self.J23.index x) % 2

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalCircle.ProperChord.exists_polygonalTheta {J : PolygonalCircle} (C : J.ProperChord) : ∃ (G : PolygonalTheta), G.J12.carrier = J.carrier ∧ G.P = C.P ∧ G.Q = C.Q ∧ G.B3 = segment ℝ C.P C.Q

Every proper straight chord of a polygon determines the finite polygonal theta graph used in Moise Chapter 2, Theorems 7 and 8.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.MeshCrosscut (G : PolygonalTheta) (M : TriangleMesh) : Type

A theta crosscut realized by an edge of a triangle mesh of the original polygonal disk. This is the exact interface between the separation theorem of Chapter 2 and the cutting induction of Chapter 3.

• support_eq : M.toPlaneComplex.support = G.J12.closedRegion
• chordEdge : Finset M.Vertex

  The chordEdge declaration.

• chordEdge_mem : self.chordEdge ∈ M.edges
• chordVertices : M.position '' ↑self.chordEdge = {G.P, G.Q}
• chordCarrier : (convexHull ℝ) (M.position '' ↑self.chordEdge) = G.B3

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.endpoints_subset_carrier12 (G : PolygonalTheta) : {G.P, G.Q} ⊆ G.J12.carrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.exterior12_disjoint_B3 (G : PolygonalTheta) : Disjoint G.J12.exteriorRegion G.B3

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.exterior12_subset_exterior13 (G : PolygonalTheta) : G.J12.exteriorRegion ⊆ G.J13.exteriorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.B2_diff_endpoints_subset_exterior13 (G : PolygonalTheta) : G.B2 \ {G.P, G.Q} ⊆ G.J13.exteriorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.interior13_subset_interior12 (G : PolygonalTheta) : G.J13.interiorRegion ⊆ G.J12.interiorRegion

def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.swap12 (G : PolygonalTheta) : PolygonalTheta

Exchange the two boundary arcs of a theta graph.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.exterior12_subset_exterior23 (G : PolygonalTheta) : G.J12.exteriorRegion ⊆ G.J23.exteriorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.B1_diff_endpoints_subset_exterior23 (G : PolygonalTheta) : G.B1 \ {G.P, G.Q} ⊆ G.J23.exteriorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.interior23_subset_interior12 (G : PolygonalTheta) : G.J23.interiorRegion ⊆ G.J12.interiorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.interior13_subset_exterior23 (G : PolygonalTheta) : G.J13.interiorRegion ⊆ G.J23.exteriorRegion

The interior of one cut-off polygon lies in the exterior of the other.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.interior23_subset_exterior13 (G : PolygonalTheta) : G.J23.interiorRegion ⊆ G.J13.exteriorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.disjoint_interior13_interior23 (G : PolygonalTheta) : Disjoint G.J13.interiorRegion G.J23.interiorRegion

The two polygons cut off by the chord have disjoint interiors.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.closedRegion13_inter_closedRegion23 (G : PolygonalTheta) : G.J13.closedRegion ∩ G.J23.closedRegion = G.B3

The two closed subdisks cut off by a proper chord meet exactly in that chord.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.interior12_diff_chord_subset (G : PolygonalTheta) : G.J12.interiorRegion \ G.B3 ⊆ G.J13.interiorRegion ∪ G.J23.interiorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.closedRegion_eq_union (G : PolygonalTheta) : G.J12.closedRegion = G.J13.closedRegion ∪ G.J23.closedRegion

Moise Chapter 2, Theorem 8(2): the two chord polygons exactly fill the original closed polygonal disk.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.MeshCrosscut.swap12 {G : PolygonalTheta} {M : TriangleMesh} (C : G.MeshCrosscut M) : G.swap12.MeshCrosscut M

Exchange the two sides of a realized mesh crosscut.

Equations

• C.swap12 = { support_eq := ⋯, chordEdge := C.chordEdge, chordEdge_mem := ⋯, chordVertices := ⋯, chordCarrier := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.MeshCrosscut.triangle_interior_side {G : PolygonalTheta} {M : TriangleMesh} (C : G.MeshCrosscut M) (T : M.Triangle) : interior (M.triangleCarrier ↑T) ⊆ G.J13.interiorRegion ∨ interior (M.triangleCarrier ↑T) ⊆ G.J23.interiorRegion

A mesh triangle lies wholly on one side of a realized crosscut.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.MeshCrosscut.side13Mesh {G : PolygonalTheta} {M : TriangleMesh} : G.MeshCrosscut M → TriangleMesh

Select the maximal triangles lying on the J13 side of the crosscut.

Equations

• x✝.side13Mesh = M.restrictTriangles fun (t : Finset M.Vertex) => (interior (M.triangleCarrier t) ∩ G.J13.interiorRegion).Nonempty

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.MeshCrosscut.side23Mesh {G : PolygonalTheta} {M : TriangleMesh} : G.MeshCrosscut M → TriangleMesh

Select the maximal triangles lying on the J23 side of the crosscut.

Equations

• x✝.side23Mesh = M.restrictTriangles fun (t : Finset M.Vertex) => (interior (M.triangleCarrier t) ∩ G.J23.interiorRegion).Nonempty

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.MeshCrosscut.swap12_side13Mesh {G : PolygonalTheta} {M : TriangleMesh} (C : G.MeshCrosscut M) : C.swap12.side13Mesh = C.side23Mesh

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.MeshCrosscut.swap12_side23Mesh {G : PolygonalTheta} {M : TriangleMesh} (C : G.MeshCrosscut M) : C.swap12.side23Mesh = C.side13Mesh

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.MeshCrosscut.side13Mesh_support {G : PolygonalTheta} {M : TriangleMesh} (C : G.MeshCrosscut M) : C.side13Mesh.toPlaneComplex.support = G.J13.closedRegion

Restricting along a realized crosscut gives exactly the first closed polygonal subdisk.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.MeshCrosscut.side23Mesh_support {G : PolygonalTheta} {M : TriangleMesh} (C : G.MeshCrosscut M) : C.side23Mesh.toPlaneComplex.support = G.J23.closedRegion

Restricting along a realized crosscut gives exactly the second closed polygonal subdisk.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.MeshCrosscut.mem_side13Mesh_triangles_iff {G : PolygonalTheta} {M : TriangleMesh} (C : G.MeshCrosscut M) {t : Finset M.Vertex} : t ∈ C.side13Mesh.triangles ↔ t ∈ M.triangles ∧ interior (M.triangleCarrier t) ⊆ G.J13.interiorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.MeshCrosscut.mem_side23Mesh_triangles_iff {G : PolygonalTheta} {M : TriangleMesh} (C : G.MeshCrosscut M) {t : Finset M.Vertex} : t ∈ C.side23Mesh.triangles ↔ t ∈ M.triangles ∧ interior (M.triangleCarrier t) ⊆ G.J23.interiorRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.MeshCrosscut.side_triangles_union {G : PolygonalTheta} {M : TriangleMesh} (C : G.MeshCrosscut M) : C.side13Mesh.triangles ∪ C.side23Mesh.triangles = M.triangles

The two restricted triangle sets partition the original mesh.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.MeshCrosscut.disjoint_side_triangles {G : PolygonalTheta} {M : TriangleMesh} (C : G.MeshCrosscut M) : Disjoint C.side13Mesh.triangles C.side23Mesh.triangles

No maximal triangle occurs on both sides of the crosscut.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.MeshCrosscut.side13_triangles_nonempty {G : PolygonalTheta} {M : TriangleMesh} (C : G.MeshCrosscut M) : C.side13Mesh.triangles.Nonempty

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.MeshCrosscut.side23_triangles_nonempty {G : PolygonalTheta} {M : TriangleMesh} (C : G.MeshCrosscut M) : C.side23Mesh.triangles.Nonempty

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.MeshCrosscut.card_side13_triangles_lt {G : PolygonalTheta} {M : TriangleMesh} (C : G.MeshCrosscut M) : C.side13Mesh.triangles.card < M.triangles.card

Each side of a proper realized crosscut has strictly fewer maximal triangles.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.PolygonalTheta.MeshCrosscut.card_side23_triangles_lt {G : PolygonalTheta} {M : TriangleMesh} (C : G.MeshCrosscut M) : C.side23Mesh.triangles.card < M.triangles.card