Coherent polygonal boundary maps for locally finite faces

The globally defined locally finite graph replacement is restricted to each standard triangular frontier. Since a shared abstract edge is represented by the same source-support points, the resulting boundary maps agree literally on overlaps. This is the compatibility needed before applying polygonal Schoenflies face by face.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.facePlaneHomeomorph_symm_mem_faceSide {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) (p : StandardFaceBoundary) (hp : ↑p ∈ standardTriangleCircle.edgeSegment i) : (K.facePlaneHomeomorph f).symm ⟨↑p, ⋯⟩ ∈ K.faceSide f i

The inverse standard-face chart takes cyclic side i into the corresponding native side.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundarySupportPoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (p : StandardFaceBoundary) : ↑K.support

The source-support point named by a standard face-boundary point.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundarySupportPoint_mem_edge {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) (p : StandardFaceBoundary) (hp : ↑p ∈ standardTriangleCircle.edgeSegment i) : faceBoundarySupportPoint f p ∈ PlaneGraphRealization.edgeInSupport (K.faceEdge f i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundarySupportPoint_mem_oneSkeleton {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (p : StandardFaceBoundary) : faceBoundarySupportPoint f p ∈ PlaneGraphRealization.oneSkeletonInSupport

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryLift {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) : StandardFaceBoundary → ↑PlaneGraphRealization.oneSkeletonInSupport

The canonical lift of a standard triangular frontier to the source one-skeleton.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_faceBoundarySupportPoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) : Continuous (faceBoundarySupportPoint f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuous_faceBoundaryLift {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) : Continuous (faceBoundaryLift f)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.injective_faceBoundaryLift {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) : Function.Injective (faceBoundaryLift f)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (p : Plane) : Plane

The global graph replacement expressed on one standard face frontier.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryMap_apply {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (p : StandardFaceBoundary) : faceBoundaryMap f ↑p = G.graphReplacementMap (faceBoundaryLift f p)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.continuousOn_faceBoundaryMap {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) : ContinuousOn (faceBoundaryMap f) (frontier standardFaceRegion)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryMap_injectiveOn {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) : Set.InjOn (faceBoundaryMap f) (frontier standardFaceRegion)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeSourcePoint_mem_frontier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) (r : ↑(Set.Icc 0 1)) : K.faceEdgeSourcePoint f i ↑r ∈ frontier standardFaceRegion

The globally oriented affine parameter on a standard side lies on the face frontier.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundarySupportPoint_sourcePoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) (r : ↑(Set.Icc 0 1)) : faceBoundarySupportPoint f ⟨K.faceEdgeSourcePoint f i ↑r, ⋯⟩ = PlaneGraphRealization.edgePathInSupport (K.faceEdge f i) r

On a standard face side, the canonical boundary lift is literally the global canonical source path of the corresponding abstract edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryMap_sourcePoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (i : ZMod 3) (r : ↑(Set.Icc 0 1)) : faceBoundaryMap f (K.faceEdgeSourcePoint f i ↑r) = (G.replacementArc (K.faceEdge f i)).completePath r

On every oriented source side, the face boundary map is the complete polygonal replacement path with the identical unit-interval parameter.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryMap_image_frontier {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) : faceBoundaryMap f '' frontier standardFaceRegion = faceReplacementCarrier f

The canonical face boundary map has exactly the assembled three-edge carrier as image.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryMap_image_polygon {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) : faceBoundaryMap f '' frontier standardFaceRegion = (facePolygonalCircle f).carrier

A finite source subdivision carrying all boundary breakpoints

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.FaceBreakpoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) : Type

All source breakpoints required on the three replacement sides of one face.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBreakpointPoint {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (b : FaceBreakpoint f) : Plane

Place one replacement-edge breakpoint on its globally oriented standard side.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBreakpointPoint_mem_standardEdge {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (b : FaceBreakpoint f) : faceBreakpointPoint f b ∈ standardTrianglePlaneComplex.cellCarrier (IntrinsicTwoComplex.faceStandardEdge b.fst)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBreakpointPoint_mem_standardOneSkeleton {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (b : FaceBreakpoint f) : faceBreakpointPoint f b ∈ standardTrianglePlaneComplex.oneSkeleton.support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundarySubdivision {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) : PlaneComplex

The common finite subdivision of the standard triangular boundary carrying every spoke join and every vertex of the three finite middle polygonal models.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundarySubdivision_subdivides {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) : (faceBoundarySubdivision f).Subdivides standardTrianglePlaneComplex.oneSkeleton

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundarySubdivision_support {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) : (faceBoundarySubdivision f).support = frontier standardFaceRegion

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeFirstBoundaryVertex {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) : standardTrianglePlaneComplex.oneSkeleton.Vertex

The first globally oriented standard corner, typed as a vertex of the standard boundary graph.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeFirstBoundaryVertex f i = id (K.faceEdgeFirstIndex f i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeSecondBoundaryVertex {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) : standardTrianglePlaneComplex.oneSkeleton.Vertex

The second globally oriented standard corner, typed as a vertex of the standard boundary graph.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeSecondBoundaryVertex f i = id (K.faceEdgeSecondIndex f i)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeFirstBoundaryVertex_position {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) : standardTrianglePlaneComplex.oneSkeleton.position (faceEdgeFirstBoundaryVertex f i) = standardTriangleVertex (K.faceEdgeFirstIndex f i)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceEdgeSecondBoundaryVertex_position {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) : standardTrianglePlaneComplex.oneSkeleton.position (faceEdgeSecondBoundaryVertex f i) = standardTriangleVertex (K.faceEdgeSecondIndex f i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardFaceEdgeFace_val_eq_boundaryEndpoints {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) : ↑(IntrinsicTwoComplex.standardFaceEdgeFace i) = {faceEdgeFirstBoundaryVertex f i, faceEdgeSecondBoundaryVertex f i}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardFaceEdge_endpoint_order {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) : standardTrianglePlaneComplex.oneSkeleton.edgeFirst (IntrinsicTwoComplex.standardFaceEdgeIndex i) = faceEdgeFirstBoundaryVertex f i ∧ standardTrianglePlaneComplex.oneSkeleton.edgeSecond (IntrinsicTwoComplex.standardFaceEdgeIndex i) = faceEdgeSecondBoundaryVertex f i ∨ standardTrianglePlaneComplex.oneSkeleton.edgeFirst (IntrinsicTwoComplex.standardFaceEdgeIndex i) = faceEdgeSecondBoundaryVertex f i ∧ standardTrianglePlaneComplex.oneSkeleton.edgeSecond (IntrinsicTwoComplex.standardFaceEdgeIndex i) = faceEdgeFirstBoundaryVertex f i

The arbitrary finite graph enumeration of a standard side either follows or reverses the global edge orientation.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardFaceEdgeParameter_sourcePoint_of_forward {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) (horient : standardTrianglePlaneComplex.oneSkeleton.edgeFirst (IntrinsicTwoComplex.standardFaceEdgeIndex i) = faceEdgeFirstBoundaryVertex f i ∧ standardTrianglePlaneComplex.oneSkeleton.edgeSecond (IntrinsicTwoComplex.standardFaceEdgeIndex i) = faceEdgeSecondBoundaryVertex f i) (r : ℝ) : (standardTrianglePlaneComplex.oneSkeleton.edgeParameter (IntrinsicTwoComplex.standardFaceEdgeIndex i)) (K.faceEdgeSourcePoint f i r) = r

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardFaceEdgeParameter_sourcePoint_of_reverse {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) (horient : standardTrianglePlaneComplex.oneSkeleton.edgeFirst (IntrinsicTwoComplex.standardFaceEdgeIndex i) = faceEdgeSecondBoundaryVertex f i ∧ standardTrianglePlaneComplex.oneSkeleton.edgeSecond (IntrinsicTwoComplex.standardFaceEdgeIndex i) = faceEdgeFirstBoundaryVertex f i) (r : ℝ) : (standardTrianglePlaneComplex.oneSkeleton.edgeParameter (IntrinsicTwoComplex.standardFaceEdgeIndex i)) (K.faceEdgeSourcePoint f i r) = 1 - r

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardFaceEdgeParameter_eq_faceEdgeParameter_of_forward {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) (horient : standardTrianglePlaneComplex.oneSkeleton.edgeFirst (IntrinsicTwoComplex.standardFaceEdgeIndex i) = faceEdgeFirstBoundaryVertex f i ∧ standardTrianglePlaneComplex.oneSkeleton.edgeSecond (IntrinsicTwoComplex.standardFaceEdgeIndex i) = faceEdgeSecondBoundaryVertex f i) {p : Plane} (hp : p ∈ standardTrianglePlaneComplex.cellCarrier (IntrinsicTwoComplex.faceStandardEdge i)) : (standardTrianglePlaneComplex.oneSkeleton.edgeParameter (IntrinsicTwoComplex.standardFaceEdgeIndex i)) p = (K.faceEdgeParameterAffine f i) p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.standardFaceEdgeParameter_eq_one_sub_faceEdgeParameter_of_reverse {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} (f : K.Face) (i : ZMod 3) (horient : standardTrianglePlaneComplex.oneSkeleton.edgeFirst (IntrinsicTwoComplex.standardFaceEdgeIndex i) = faceEdgeSecondBoundaryVertex f i ∧ standardTrianglePlaneComplex.oneSkeleton.edgeSecond (IntrinsicTwoComplex.standardFaceEdgeIndex i) = faceEdgeFirstBoundaryVertex f i) {p : Plane} (hp : p ∈ standardTrianglePlaneComplex.cellCarrier (IntrinsicTwoComplex.faceStandardEdge i)) : (standardTrianglePlaneComplex.oneSkeleton.edgeParameter (IntrinsicTwoComplex.standardFaceEdgeIndex i)) p = 1 - (K.faceEdgeParameterAffine f i) p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundarySubdivision_parameter_side_standard {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (i : ZMod 3) (b : EdgeBreakpoint (G.replacementArc (K.faceEdge f i))) {u : Finset (faceBoundarySubdivision f).Vertex} (hu : u ∈ (faceBoundarySubdivision f).simplexes) : (∀ p ∈ (faceBoundarySubdivision f).cellCarrier u, (standardTrianglePlaneComplex.oneSkeleton.edgeParameter (IntrinsicTwoComplex.standardFaceEdgeIndex i)) p ≤ (standardTrianglePlaneComplex.oneSkeleton.edgeParameter (IntrinsicTwoComplex.standardFaceEdgeIndex i)) (faceBreakpointPoint f ⟨i, b⟩)) ∨ ∀ p ∈ (faceBoundarySubdivision f).cellCarrier u, (standardTrianglePlaneComplex.oneSkeleton.edgeParameter (IntrinsicTwoComplex.standardFaceEdgeIndex i)) (faceBreakpointPoint f ⟨i, b⟩) ≤ (standardTrianglePlaneComplex.oneSkeleton.edgeParameter (IntrinsicTwoComplex.standardFaceEdgeIndex i)) p

Every face of the marked boundary subdivision lies on one side of every marked parameter, measured in the finite graph enumeration coordinate.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundarySubdivision_parameter_side {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (i : ZMod 3) (b : EdgeBreakpoint (G.replacementArc (K.faceEdge f i))) {u : Finset (faceBoundarySubdivision f).Vertex} (hu : u ∈ (faceBoundarySubdivision f).simplexes) (hui : (faceBoundarySubdivision f).cellCarrier u ⊆ standardTrianglePlaneComplex.cellCarrier (IntrinsicTwoComplex.faceStandardEdge i)) : (∀ p ∈ (faceBoundarySubdivision f).cellCarrier u, (K.faceEdgeParameterAffine f i) p ≤ edgeBreakpointParameter (G.replacementArc (K.faceEdge f i)) b) ∨ ∀ p ∈ (faceBoundarySubdivision f).cellCarrier u, edgeBreakpointParameter (G.replacementArc (K.faceEdge f i)) b ≤ (K.faceEdgeParameterAffine f i) p

On a subdivision face contained in one standard side, the marked-side test is the globally oriented edge-parameter test, independently of the graph enumeration orientation.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundarySubdivision_piece {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (i : ZMod 3) {u : Finset (faceBoundarySubdivision f).Vertex} (hu : u ∈ (faceBoundarySubdivision f).simplexes) (hui : (faceBoundarySubdivision f).cellCarrier u ⊆ standardTrianglePlaneComplex.cellCarrier (IntrinsicTwoComplex.faceStandardEdge i)) : (∀ p ∈ (faceBoundarySubdivision f).cellCarrier u, (K.faceEdgeParameterAffine f i) p ≤ 1 / 2) ∨ ((∀ p ∈ (faceBoundarySubdivision f).cellCarrier u, 1 / 2 ≤ (K.faceEdgeParameterAffine f i) p) ∧ ∀ p ∈ (faceBoundarySubdivision f).cellCarrier u, (K.faceEdgeParameterAffine f i) p ≤ 3 / 4) ∨ ∀ p ∈ (faceBoundarySubdivision f).cellCarrier u, 3 / 4 ≤ (K.faceEdgeParameterAffine f i) p

The two spoke joins split each subdivision face on a selected standard side into the left, middle, or right parameter range.

Affine formulas on subdivision pieces

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceMiddleSourceAffine {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (i : ZMod 3) : Plane →ᵃ[ℝ] Plane

The affine map from a standard face side into the source axis of the finite middle polygonal model.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceMiddleSourceAffine_apply {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (i : ZMod 3) (p : Plane) : (faceMiddleSourceAffine f i) p = planePoint (↑(G.replacementArc (K.faceEdge f i)).parameterization.length * ((G.replacementArc (K.faceEdge f i)).exitData.left + ((G.replacementArc (K.faceEdge f i)).exitData.right - (G.replacementArc (K.faceEdge f i)).exitData.left) * (4 * (K.faceEdgeParameterAffine f i) p - 2))) 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryMap_affineOn_left {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (i : ZMod 3) {E : Set Plane} (hside : E ⊆ standardTrianglePlaneComplex.cellCarrier (IntrinsicTwoComplex.faceStandardEdge i)) (hle : ∀ p ∈ E, (K.faceEdgeParameterAffine f i) p ≤ 1 / 2) : IsAffineOn (faceBoundaryMap f) E

The boundary map is affine on every subset of a standard side contained in the first spoke range.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryMap_affineOn_right {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (i : ZMod 3) {E : Set Plane} (hside : E ⊆ standardTrianglePlaneComplex.cellCarrier (IntrinsicTwoComplex.faceStandardEdge i)) (hge : ∀ p ∈ E, 3 / 4 ≤ (K.faceEdgeParameterAffine f i) p) : IsAffineOn (faceBoundaryMap f) E

The boundary map is affine on every subset of a standard side contained in the final spoke range.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryMap_affineOn_middle {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (i : ZMod 3) {E : Set Plane} (hside : E ⊆ standardTrianglePlaneComplex.cellCarrier (IntrinsicTwoComplex.faceStandardEdge i)) (hmid0 : ∀ p ∈ E, 1 / 2 ≤ (K.faceEdgeParameterAffine f i) p) (hmid1 : ∀ p ∈ E, (K.faceEdgeParameterAffine f i) p ≤ 3 / 4) (hsource : ∃ s ∈ (G.replacementArc (K.faceEdge f i)).parameterization.source.simplexes, Set.MapsTo (⇑(faceMiddleSourceAffine f i)) E ((G.replacementArc (K.faceEdge f i)).parameterization.source.cellCarrier s)) : IsAffineOn (faceBoundaryMap f) E

A middle side piece is affine once its affine source image lies in one simplex of the finite polygonal segment model.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundarySubdivision_middleSource {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (i : ZMod 3) {u : Finset (faceBoundarySubdivision f).Vertex} (hu : u ∈ (faceBoundarySubdivision f).simplexes) (hui : (faceBoundarySubdivision f).cellCarrier u ⊆ standardTrianglePlaneComplex.cellCarrier (IntrinsicTwoComplex.faceStandardEdge i)) (hcard : u.card = 2) (hmid0 : ∀ p ∈ (faceBoundarySubdivision f).cellCarrier u, 1 / 2 ≤ (K.faceEdgeParameterAffine f i) p) (hmid1 : ∀ p ∈ (faceBoundarySubdivision f).cellCarrier u, (K.faceEdgeParameterAffine f i) p ≤ 3 / 4) : ∃ s ∈ (G.replacementArc (K.faceEdge f i)).parameterization.source.simplexes, Set.MapsTo (⇑(faceMiddleSourceAffine f i)) ((faceBoundarySubdivision f).cellCarrier u) ((G.replacementArc (K.faceEdge f i)).parameterization.source.cellCarrier s)

The marked middle-model vertices ensure that a two-vertex subdivision face maps into one simplex of the finite segment model.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryMap_affineOn_subdivision {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) (u : Finset (faceBoundarySubdivision f).Vertex) : u ∈ (faceBoundarySubdivision f).simplexes → IsAffineOn (faceBoundaryMap f) ((faceBoundarySubdivision f).cellCarrier u)

The canonical face boundary map is affine on every simplex of its finite marked subdivision.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.LocallyFiniteTriangleComplex.faceBoundaryMap_isPLOnSet {S : Type u_1} [TopologicalSpace S] {K : LocallyFiniteTriangleComplex S} {G : K.PlaneGraphRealization} (f : K.Face) : IsPLOnSet (frontier standardFaceRegion) (faceBoundaryMap f)

The coherent standard-triangle boundary map is genuinely PL on the polygonal frontier.