Polygonal boundaries of locally finite two-simplexes

The globally coherent locally finite edge replacement assigns a finite polygonal arc to every abstract edge. For each maximal face this file resolves its three edge complexes in one finite line arrangement and extracts the resulting simple polygonal cycle. Shared abstract edges use literally the same replacement arc, so adjacent face fillings will have identical boundaries.

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceReplacementArc {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (t : K.Face) (i : ZMod 3) : G.CentralPolygonalArc (K.faceEdge t i)

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

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceReplacementArc t i = G.replacementArc (K.faceEdge t i)

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.FaceGraphSimplex {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceGraphSimplexFintype {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (t : K.Face) (i : ZMod 3) : Fintype (FaceGraphSimplex t i)

Equations

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

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.FaceGraphSegment {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceGraphSegmentFintype {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (t : K.Face) : Fintype (FaceGraphSegment t)

Equations

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

@[reducible, inline]

noncomputable abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.FaceBoundaryPiece {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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

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

@[instance_reducible]

noncomputable instance LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryPieceFintype {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (t : K.Face) : Fintype (FaceBoundaryPiece t)

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceGraphSegmentLeft {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceGraphSegmentRight {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceBoundaryLeft {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceBoundaryRight {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceReplacementCarrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceReplacementCarrier_inter_next {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (t : K.Face) (i : ZMod 3) : (faceReplacementArc t i).completeCarrier ∩ (faceReplacementArc t (i + 1)).completeCarrier = {G.vertexImage (K.faceVertex t (i + 1))}

Consecutive replacement edges around one face meet exactly at their shared cyclic vertex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryPiece_segment_subset {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.exists_faceBoundaryPiece_segment {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceBoundaryChain {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceBoundaryComplex {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceBoundaryComplex_support {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceVertexPiece {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (t : K.Face) (i : ZMod 3) : FaceBoundaryPiece t

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

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryVertex {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceBoundaryVertex_position {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (t : K.Face) (i : ZMod 3) : (faceBoundaryComplex t).position (faceBoundaryVertex t i) = G.vertexImage (K.faceVertex t i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryVertex_face {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.exists_faceBoundaryPiece_segment_on_edge {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.exists_faceBoundary_face_on_edge {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceEdgeComplex {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceEdgeComplex_support {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (t : K.Face) (i : ZMod 3) : (faceEdgeComplex t i).support = (faceReplacementArc t i).completeCarrier

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryVertex_face_edge_start {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (t : K.Face) (i : ZMod 3) : {faceBoundaryVertex t i} ∈ (faceEdgeComplex t i).simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryVertex_face_edge_finish {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (t : K.Face) (i : ZMod 3) : {faceBoundaryVertex t (i + 1)} ∈ (faceEdgeComplex t i).simplexes

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.isPreconnected_faceEdgeComplex_support {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (t : K.Face) (i : ZMod 3) : IsPreconnected (faceEdgeComplex t i).support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeVertexPath {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceEdgeVertexPath t i = Classical.choice ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeComplex_vertexGraph_le {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (t : K.Face) (i : ZMod 3) : (faceEdgeComplex t i).vertexGraph ≤ (faceBoundaryComplex t).vertexGraph

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryEdgePath {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceBoundaryEdgePath_position_mem {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceEdgeGeometricPath {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.range_faceEdgeGeometricPath {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.range_faceBoundaryEdgePath {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceBoundaryVertex_ne_next {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceBoundaryEdgePath_length_pos {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceBoundaryEdgePath_support_disjoint_next_tail {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceBoundaryTwoEdgePath {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceBoundaryTwoEdgePath_tail_disjoint_closing_tail {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.one_lt_faceBoundaryTwoEdgePath_length {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceBoundaryCycleWalk {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.faceBoundaryCycleWalk_isCycle {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.range_faceBoundaryCycleWalk {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.facePolygonalCircle {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (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.LocallyFiniteTriangleComplex.facePolygonalCircle_carrier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (t : K.Face) : (facePolygonalCircle t).carrier = faceReplacementCarrier t

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