Polygonal boundaries of intrinsic two-simplexes

The edge approximation of an intrinsic finite complex constructs each replacement edge in its own finite line arrangement. A two-cell extension needs the three edges of one abstract face in one common plane complex. This file enumerates only the one-dimensional arrangement faces which actually carry those three edges, resolves all their segments simultaneously, and extracts the resulting simple polygonal cycle.

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceReplacementArc {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : K.CentralPolygonalArc hcont hinj D C (K.faceEdge t i)

The selected replacement arc on cyclic edge i of the intrinsic face t.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceReplacementArc t i = K.replacementArc hcont hinj D C (K.faceEdge t i)

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.FaceGraphSimplex {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : Type

A one-dimensional face in the private arrangement of one replacement edge, together with the proof that it is subordinate to that edge.

Equations

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

@[instance_reducible]

noncomputable instance LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceGraphSimplexFintype {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : Fintype (FaceGraphSimplex t i)

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceGraphSimplexFintype t i = id inferInstance

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.FaceGraphSegment {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) : Type

An ordered pair of vertices in a subordinate one-dimensional face, indexed also by the abstract edge to which it belongs.

Equations

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

@[instance_reducible]

noncomputable instance LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceGraphSegmentFintype {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) : Fintype (FaceGraphSegment t)

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceGraphSegmentFintype t = id inferInstance

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.FaceBoundaryPiece {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) : Type

Segment labels for the common face arrangement. The left summand lists actual graph segments. The right summand inserts the three abstract vertex images explicitly as degenerate segments, making them canonical arrangement vertices.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.FaceBoundaryPiece t = (LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.FaceGraphSegment t ⊕ ZMod 3)

@[instance_reducible]

noncomputable instance LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryPieceFintype {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) : Fintype (FaceBoundaryPiece t)

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryPieceFintype t = id inferInstance

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceGraphSegmentLeft {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (p : FaceGraphSegment t) : Plane

The faceGraphSegmentLeft declaration.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceGraphSegmentRight {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (p : FaceGraphSegment t) : Plane

The faceGraphSegmentRight declaration.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryLeft {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (p : FaceBoundaryPiece t) : Plane

The faceBoundaryLeft declaration.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryRight {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (p : FaceBoundaryPiece t) : Plane

The faceBoundaryRight declaration.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceReplacementCarrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) : Set Plane

The union of the three complete replacement-edge carriers around one intrinsic face.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryPiece_segment_subset {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (p : FaceBoundaryPiece t) : segment ℝ (faceBoundaryLeft t p) (faceBoundaryRight t p) ⊆ faceReplacementCarrier t

Every listed family segment lies in the replacement boundary carrier.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_faceBoundaryPiece_segment {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) {x : Plane} (hx : x ∈ faceReplacementCarrier t) : ∃ (p : FaceBoundaryPiece t), x ∈ segment ℝ (faceBoundaryLeft t p) (faceBoundaryRight t p)

Every boundary-carrier point lies on one of the explicitly indexed family segments.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryChain {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) : BrokenLineData Set.univ

The common auxiliary chain listing every relevant segment around one intrinsic face.

Equations

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

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryComplex {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) : PlaneComplex

One finite plane complex carrying all three replacement edges face-to-face.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryComplex_support {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) : (faceBoundaryComplex t).support = faceReplacementCarrier t

The common face complex has exactly the union of the three replacement edges as support.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceVertexPiece {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : FaceBoundaryPiece t

The explicit degenerate family piece used to mark abstract corner i.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceVertexPiece t i = Sum.inr i

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryVertex {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : (faceBoundaryComplex t).Vertex

The canonical common-arrangement vertex at abstract corner i.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryVertex_position {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : (faceBoundaryComplex t).position (faceBoundaryVertex t i) = h (K.vertexPoint (K.faceUsedVertex t i))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryVertex_face {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : {faceBoundaryVertex t i} ∈ (faceBoundaryComplex t).simplexes

Every abstract corner is a zero-face of the common boundary complex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_faceBoundaryPiece_segment_on_edge {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) {x : Plane} (hx : x ∈ (faceReplacementArc t i).completeCarrier) : ∃ (p : FaceBoundaryPiece t), x ∈ segment ℝ (faceBoundaryLeft t p) (faceBoundaryRight t p) ∧ segment ℝ (faceBoundaryLeft t p) (faceBoundaryRight t p) ⊆ (faceReplacementArc t i).completeCarrier

A family segment on edge i containing the given edge-carrier point, together with its subordination to that one edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_faceBoundary_face_on_edge {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) {x : Plane} (hx : x ∈ (faceReplacementArc t i).completeCarrier) : ∃ s ∈ (faceBoundaryChain t).arrangementMesh.toPlaneComplex.simplexes, x ∈ (faceBoundaryChain t).arrangementMesh.toPlaneComplex.cellCarrier s ∧ (faceBoundaryChain t).arrangementMesh.toPlaneComplex.cellCarrier s ⊆ (faceReplacementArc t i).completeCarrier

The common arrangement has a face subordinate to edge i through every point of that edge.

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeComplex {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : PlaneComplex

The subcomplex of the common face arrangement carried by cyclic edge i.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeComplex_support {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : (faceEdgeComplex t i).support = (faceReplacementArc t i).completeCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryVertex_face_edge_start {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : {faceBoundaryVertex t i} ∈ (faceEdgeComplex t i).simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryVertex_face_edge_finish {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : {faceBoundaryVertex t (i + 1)} ∈ (faceEdgeComplex t i).simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.isPreconnected_faceEdgeComplex_support {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : IsPreconnected (faceEdgeComplex t i).support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeVertexPath {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : (faceEdgeComplex t i).vertexGraph.Path (faceBoundaryVertex t i) (faceBoundaryVertex t (i + 1))

A loop-free path through cyclic replacement edge i, oriented from corner i to corner i+1.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeVertexPath t i = Classical.choice ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeComplex_vertexGraph_le {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : (faceEdgeComplex t i).vertexGraph ≤ (faceBoundaryComplex t).vertexGraph

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryEdgePath {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : (faceBoundaryComplex t).vertexGraph.Path (faceBoundaryVertex t i) (faceBoundaryVertex t (i + 1))

The oriented edge path, regarded in the common boundary complex.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryEdgePath_position_mem {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) {v : (faceBoundaryComplex t).Vertex} (hv : v ∈ (↑(faceBoundaryEdgePath t i)).support) : (faceBoundaryComplex t).position v ∈ (faceReplacementArc t i).completeCarrier

Every vertex visited by the oriented path for edge i lies geometrically on that replacement edge.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeGeometricPath {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : Path ((faceEdgeComplex t i).position (faceBoundaryVertex t i)) ((faceEdgeComplex t i).position (faceBoundaryVertex t (i + 1)))

The straight geometric path traced by the selected graph path on one replacement edge.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.range_faceEdgeGeometricPath {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : Set.range ⇑(faceEdgeGeometricPath t i) = (faceReplacementArc t i).completeCarrier

The selected finite graph path covers the entire polygonal replacement edge. The key input is that a connected subpath of an embedded arc containing both endpoints must be the whole arc.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.range_faceBoundaryEdgePath {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : Set.range ⇑((faceBoundaryComplex t).walkGeometricPath ↑(faceBoundaryEdgePath t i)) = (faceReplacementArc t i).completeCarrier

The same edge path, mapped into the common face-boundary complex, still covers the complete replacement edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryVertex_ne_next {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : faceBoundaryVertex t i ≠ faceBoundaryVertex t (i + 1)

Distinct cyclic corners remain distinct as vertices of the common arrangement.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryEdgePath_length_pos {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : 0 < (↑(faceBoundaryEdgePath t i)).length

Every oriented replacement-edge path contains at least one edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryEdgePath_support_disjoint_next_tail {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : (↑(faceBoundaryEdgePath t i)).support.Disjoint (↑(faceBoundaryEdgePath t (i + 1))).support.tail

Consecutive replacement-edge paths share only their common endpoint, which is removed from the tail of the second path.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryTwoEdgePath {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : (faceBoundaryComplex t).vertexGraph.Path (faceBoundaryVertex t i) (faceBoundaryVertex t (i + 1 + 1))

The first two oriented replacement edges form a simple path from corner i to the second cyclic successor of i. The unreduced successor expression keeps dependent elaboration cheap.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryTwoEdgePath_tail_disjoint_closing_tail {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : (↑(faceBoundaryTwoEdgePath t i)).support.tail.Disjoint (↑(faceBoundaryEdgePath t (i + 1 + 1))).support.tail

The tail of the first two boundary edges is disjoint from the tail of the closing edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.one_lt_faceBoundaryTwoEdgePath_length {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : 1 < (↑(faceBoundaryTwoEdgePath t i)).length

The two-edge boundary path has length at least two.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryCycleWalk {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : (faceBoundaryComplex t).vertexGraph.Walk (faceBoundaryVertex t i) (faceBoundaryVertex t i)

The three oriented replacement-edge paths, with the final cyclic endpoint identified.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryCycleWalk_isCycle {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : (faceBoundaryCycleWalk t i).IsCycle

The boundary walk extracted from the common arrangement is a simple graph cycle.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.range_faceBoundaryCycleWalk {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) (i : ZMod 3) : Set.range ⇑((faceBoundaryComplex t).walkGeometricPath (faceBoundaryCycleWalk t i)) = (faceReplacementArc t i).completeCarrier ∪ (faceReplacementArc t (i + 1)).completeCarrier ∪ (faceReplacementArc t (i + 1 + 1)).completeCarrier

The geometric range of the boundary cycle is the union of its three complete replacement edges.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePolygonalCircle {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) : PolygonalCircle

The simple polygonal circle formed by the three replacement edges around t.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePolygonalCircle_carrier {K : IntrinsicTwoComplex} {h : K.realization → Plane} {hcont : Continuous h} {hinj : Function.Injective h} {D : K.VertexDiskControl h} {C : K.CentralTubeControl hcont hinj D} (t : K.Face) : (facePolygonalCircle t).carrier = faceReplacementCarrier t

The extracted polygonal circle has exactly the prescribed three-edge replacement boundary.