Relative polygonal boundary maps for intrinsic faces

The simultaneous intrinsic graph replacement is defined once on the global one-skeleton. This file restricts that one map to each closed face, in standard triangle coordinates. Consequently two neighboring face extensions will have literally the same boundary values on their shared edge. The construction below is topological; the finite conforming subdivision which certifies that it is PL is kept as a separate obligation.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardFaceRegion : Set Plane

The closed standard triangle used as the source model for every intrinsic face.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardFaceRegion = LeanEval.Topology.ClassificationOfSurfaces.Moise.standardTrianglePlaneComplex.support

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.StandardFaceBoundary : Type

Its polygonal frontier, as a subtype.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardFaceBoundary_mem_region (p : StandardFaceBoundary) : ↑p ∈ standardFaceRegion

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePlaneHomeomorph_symm_mem_edge {K : IntrinsicTwoComplex} (t : K.Face) (i : ZMod 3) {p : Plane} (hp : p ∈ standardTriangleCircle.edgeSegment i) : ↑((K.facePlaneHomeomorph t).symm ⟨p, ⋯⟩) ∈ K.faceCarrier ↑(K.faceEdge t i)

A point on a standard cyclic side lifts to the corresponding intrinsic edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.facePlaneHomeomorph_symm_mem_oneSkeleton {K : IntrinsicTwoComplex} (t : K.Face) (p : StandardFaceBoundary) : ↑((K.facePlaneHomeomorph t).symm ⟨↑p, ⋯⟩) ∈ K.oneSkeleton

The inverse standard-face chart sends the standard frontier into the global intrinsic one-skeleton.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryLift {K : IntrinsicTwoComplex} (t : K.Face) : StandardFaceBoundary → ↑K.oneSkeleton

The canonical lift of the standard triangular frontier to the global intrinsic one-skeleton.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryLift t p = ⟨↑((K.facePlaneHomeomorph t).symm ⟨↑p, ⋯⟩), ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.continuous_faceBoundaryLift {K : IntrinsicTwoComplex} (t : K.Face) : Continuous (faceBoundaryLift t)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.injective_faceBoundaryLift {K : IntrinsicTwoComplex} (t : K.Face) : Function.Injective (faceBoundaryLift t)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryMap {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 : Plane) : Plane

The global graph replacement, expressed on the standard frontier of one intrinsic face. Outside that frontier the value is deliberately irrelevant.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryMap_apply {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 : StandardFaceBoundary) : faceBoundaryMap t ↑p = K.graphReplacementMap hcont hinj D C ↑(faceBoundaryLift t p)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.continuousOn_faceBoundaryMap {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) : ContinuousOn (faceBoundaryMap t) (frontier standardFaceRegion)

The canonical face boundary map is continuous on the standard frontier.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryMap_injectiveOn {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.InjOn (faceBoundaryMap t) (frontier standardFaceRegion)

The canonical face boundary map is injective on the standard frontier.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryMap_image_frontier {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) : faceBoundaryMap t '' frontier standardFaceRegion = faceReplacementCarrier t

The canonical boundary parameterization has exactly the polygon assembled from the three global replacement edges as its image.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryMap_image_polygon {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) : faceBoundaryMap t '' frontier standardFaceRegion = (facePolygonalCircle t).carrier

The same exact image statement, expressed using the extracted polygonal circle.

A finite source subdivision carrying all boundary breakpoints

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceStandardEdge_card (i : ZMod 3) : (faceStandardEdge i).card = 2

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardFaceEdgeFace (i : ZMod 3) : standardTrianglePlaneComplex.oneSkeleton.EdgeFace

A cyclic side of the standard triangle, regarded as an edge of its one-skeleton.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardFaceEdgeFace i = ⟨LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceStandardEdge i, ⋯⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardFaceEdgeIndex (i : ZMod 3) : Fin (Fintype.card standardTrianglePlaneComplex.oneSkeleton.EdgeFace)

The finite graph enumeration index of a cyclic standard side.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardFaceEdgeIndex i = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardFaceEdgeAt_eq (i : ZMod 3) : standardTrianglePlaneComplex.oneSkeleton.edgeAt (standardFaceEdgeIndex i) = standardFaceEdgeFace i

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.FaceBreakpoint {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

All breakpoints needed on all three sides of one intrinsic face.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBreakpointPoint {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) (b : FaceBreakpoint t) : Plane

A replacement-edge breakpoint placed on the corresponding oriented standard side.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBreakpointPoint_mem_standardEdge {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) (b : FaceBreakpoint t) : faceBreakpointPoint t b ∈ standardTrianglePlaneComplex.cellCarrier (faceStandardEdge b.fst)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBreakpointPoint_mem_standardOneSkeleton {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) (b : FaceBreakpoint t) : faceBreakpointPoint t b ∈ standardTrianglePlaneComplex.oneSkeleton.support

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundarySubdivision {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

The common finite standard-boundary subdivision carrying the spoke joins and every vertex of every middle polygonal model.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundarySubdivision_subdivides {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) : (faceBoundarySubdivision t).Subdivides standardTrianglePlaneComplex.oneSkeleton

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundarySubdivision_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) : (faceBoundarySubdivision t).support = frontier standardFaceRegion

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardBoundaryVertex (j : Fin 3) : standardTrianglePlaneComplex.oneSkeleton.Vertex

A standard Fin 3 corner, typed as a vertex of the opaque one-skeleton object.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardBoundaryVertex j = id j

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.exists_faceStandardEdge_of_standardBoundaryEdge {s : Finset standardTrianglePlaneComplex.oneSkeleton.Vertex} (hcard : s.card = 2) : ∃ (i : ZMod 3), s = ↑(standardFaceEdgeFace i)

Every two-vertex simplex of the standard boundary graph is one of its three cyclic sides.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardFaceEdgeFace_cellCarrier (i : ZMod 3) : standardTrianglePlaneComplex.oneSkeleton.cellCarrier ↑(standardFaceEdgeFace i) = standardTrianglePlaneComplex.cellCarrier (faceStandardEdge i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeFirstBoundaryVertex {K : IntrinsicTwoComplex} (t : K.Face) (i : ZMod 3) : standardTrianglePlaneComplex.oneSkeleton.Vertex

The first oriented standard corner, typed as a vertex of the opaque one-skeleton object.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeFirstBoundaryVertex t i = id (K.faceEdgeFirstIndex t i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeSecondBoundaryVertex {K : IntrinsicTwoComplex} (t : K.Face) (i : ZMod 3) : standardTrianglePlaneComplex.oneSkeleton.Vertex

The second oriented standard corner, typed as a vertex of the opaque one-skeleton object.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeSecondBoundaryVertex t i = id (K.faceEdgeSecondIndex t i)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeFirstBoundaryVertex_position {K : IntrinsicTwoComplex} (t : K.Face) (i : ZMod 3) : standardTrianglePlaneComplex.oneSkeleton.position (faceEdgeFirstBoundaryVertex t i) = standardTriangleVertex (K.faceEdgeFirstIndex t i)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeSecondBoundaryVertex_position {K : IntrinsicTwoComplex} (t : K.Face) (i : ZMod 3) : standardTrianglePlaneComplex.oneSkeleton.position (faceEdgeSecondBoundaryVertex t i) = standardTriangleVertex (K.faceEdgeSecondIndex t i)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardFaceEdgeFace_val_eq_boundaryEndpoints {K : IntrinsicTwoComplex} (t : K.Face) (i : ZMod 3) : ↑(standardFaceEdgeFace i) = {faceEdgeFirstBoundaryVertex t i, faceEdgeSecondBoundaryVertex t i}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardFaceEdge_endpoint_order {K : IntrinsicTwoComplex} (t : K.Face) (i : ZMod 3) : standardTrianglePlaneComplex.oneSkeleton.edgeFirst (standardFaceEdgeIndex i) = faceEdgeFirstBoundaryVertex t i ∧ standardTrianglePlaneComplex.oneSkeleton.edgeSecond (standardFaceEdgeIndex i) = faceEdgeSecondBoundaryVertex t i ∨ standardTrianglePlaneComplex.oneSkeleton.edgeFirst (standardFaceEdgeIndex i) = faceEdgeSecondBoundaryVertex t i ∧ standardTrianglePlaneComplex.oneSkeleton.edgeSecond (standardFaceEdgeIndex i) = faceEdgeFirstBoundaryVertex t i

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeParameterAffine {K : IntrinsicTwoComplex} (t : K.Face) (i : ZMod 3) : Plane →ᵃ[ℝ] ℝ

The intrinsic edge parameter, pulled back as an ambient affine coordinate on the standard face plane.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeParameterAffine t i = (K.edgeCoordinateAffine (K.faceEdge t i)).comp (K.facePlaneInverseAffine t)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeParameterAffine_apply {K : IntrinsicTwoComplex} (t : K.Face) (i : ZMod 3) (p : Plane) : (faceEdgeParameterAffine t i) p = (K.facePlaneInverseAffine t) p (K.edgeSecond (K.faceEdge t i))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceEdgeParameterAffine_sourcePoint {K : IntrinsicTwoComplex} (t : K.Face) (i : ZMod 3) (r : ℝ) : (faceEdgeParameterAffine t i) (K.faceEdgeSourcePoint t i r) = r

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardFaceEdgeParameter_sourcePoint_of_forward {K : IntrinsicTwoComplex} (t : K.Face) (i : ZMod 3) (horient : standardTrianglePlaneComplex.oneSkeleton.edgeFirst (standardFaceEdgeIndex i) = faceEdgeFirstBoundaryVertex t i ∧ standardTrianglePlaneComplex.oneSkeleton.edgeSecond (standardFaceEdgeIndex i) = faceEdgeSecondBoundaryVertex t i) (r : ℝ) : (standardTrianglePlaneComplex.oneSkeleton.edgeParameter (standardFaceEdgeIndex i)) (K.faceEdgeSourcePoint t i r) = r

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.standardFaceEdgeParameter_sourcePoint_of_reverse {K : IntrinsicTwoComplex} (t : K.Face) (i : ZMod 3) (horient : standardTrianglePlaneComplex.oneSkeleton.edgeFirst (standardFaceEdgeIndex i) = faceEdgeSecondBoundaryVertex t i ∧ standardTrianglePlaneComplex.oneSkeleton.edgeSecond (standardFaceEdgeIndex i) = faceEdgeFirstBoundaryVertex t i) (r : ℝ) : (standardTrianglePlaneComplex.oneSkeleton.edgeParameter (standardFaceEdgeIndex i)) (K.faceEdgeSourcePoint t i r) = 1 - r

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

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundarySubdivision_parameter_side_standard {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) (b : EdgeBreakpoint (K.replacementArc hcont hinj D C (K.faceEdge t i))) {u : Finset (faceBoundarySubdivision t).Vertex} (hu : u ∈ (faceBoundarySubdivision t).simplexes) : (∀ p ∈ (faceBoundarySubdivision t).cellCarrier u, (standardTrianglePlaneComplex.oneSkeleton.edgeParameter (standardFaceEdgeIndex i)) p ≤ (standardTrianglePlaneComplex.oneSkeleton.edgeParameter (standardFaceEdgeIndex i)) (faceBreakpointPoint t ⟨i, b⟩)) ∨ ∀ p ∈ (faceBoundarySubdivision t).cellCarrier u, (standardTrianglePlaneComplex.oneSkeleton.edgeParameter (standardFaceEdgeIndex i)) (faceBreakpointPoint t ⟨i, b⟩) ≤ (standardTrianglePlaneComplex.oneSkeleton.edgeParameter (standardFaceEdgeIndex i)) p

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundarySubdivision_parameter_side {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) (b : EdgeBreakpoint (K.replacementArc hcont hinj D C (K.faceEdge t i))) {u : Finset (faceBoundarySubdivision t).Vertex} (hu : u ∈ (faceBoundarySubdivision t).simplexes) (hui : (faceBoundarySubdivision t).cellCarrier u ⊆ standardTrianglePlaneComplex.cellCarrier (faceStandardEdge i)) : (∀ p ∈ (faceBoundarySubdivision t).cellCarrier u, (faceEdgeParameterAffine t i) p ≤ edgeBreakpointParameter (K.replacementArc hcont hinj D C (K.faceEdge t i)) b) ∨ ∀ p ∈ (faceBoundarySubdivision t).cellCarrier u, edgeBreakpointParameter (K.replacementArc hcont hinj D C (K.faceEdge t i)) b ≤ (faceEdgeParameterAffine t i) p

On a subdivision face contained in one standard side, the same side test is exactly the intrinsic edge parameter test, independent of orientation.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundarySubdivision_piece {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) {u : Finset (faceBoundarySubdivision t).Vertex} (hu : u ∈ (faceBoundarySubdivision t).simplexes) (hui : (faceBoundarySubdivision t).cellCarrier u ⊆ standardTrianglePlaneComplex.cellCarrier (faceStandardEdge i)) : (∀ p ∈ (faceBoundarySubdivision t).cellCarrier u, (faceEdgeParameterAffine t i) p ≤ 1 / 2) ∨ ((∀ p ∈ (faceBoundarySubdivision t).cellCarrier u, 1 / 2 ≤ (faceEdgeParameterAffine t i) p) ∧ ∀ p ∈ (faceBoundarySubdivision t).cellCarrier u, (faceEdgeParameterAffine t i) p ≤ 3 / 4) ∨ ∀ p ∈ (faceBoundarySubdivision t).cellCarrier u, 3 / 4 ≤ (faceEdgeParameterAffine t i) p

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryMap_affineOn_of_lift {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) {E : Set Plane} {X : Set K.realization} (hfrontier : E ⊆ frontier standardFaceRegion) (hlift : ∀ (p : Plane) (hp : p ∈ E), ↑(faceBoundaryLift t ⟨p, ⋯⟩) ∈ X) (haffine : K.IsAffineOnSet (K.graphReplacementMap hcont hinj D C) X) : IsAffineOn (faceBoundaryMap t) E

Pull an intrinsic affine certificate back through the affine inverse face chart.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryMap_affineOn_left {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) {E : Set Plane} (hfrontier : E ⊆ frontier standardFaceRegion) (hside : E ⊆ standardTrianglePlaneComplex.cellCarrier (faceStandardEdge i)) (hle : ∀ p ∈ E, (faceEdgeParameterAffine t i) p ≤ 1 / 2) : IsAffineOn (faceBoundaryMap t) E

On a left spoke piece of a standard side, the canonical face boundary map is affine.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryMap_affineOn_right {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) {E : Set Plane} (hfrontier : E ⊆ frontier standardFaceRegion) (hside : E ⊆ standardTrianglePlaneComplex.cellCarrier (faceStandardEdge i)) (hge : ∀ p ∈ E, 3 / 4 ≤ (faceEdgeParameterAffine t i) p) : IsAffineOn (faceBoundaryMap t) E

On a right spoke piece of a standard side, the canonical face boundary map is affine.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryMap_affineOn_middle {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) {E : Set Plane} (hfrontier : E ⊆ frontier standardFaceRegion) (hside : E ⊆ standardTrianglePlaneComplex.cellCarrier (faceStandardEdge i)) (hmid0 : ∀ p ∈ E, 1 / 2 ≤ (faceEdgeParameterAffine t i) p) (hmid1 : ∀ p ∈ E, (faceEdgeParameterAffine t i) p ≤ 3 / 4) (hsource : ∃ s ∈ (K.replacementArc hcont hinj D C (K.faceEdge t i)).parameterization.source.simplexes, Set.MapsTo (fun (p : Plane) => (edgeMiddleSourceMap (K.replacementArc hcont hinj D C (K.faceEdge t i))) ((K.facePlaneInverseAffine t) p)) E ((K.replacementArc hcont hinj D C (K.faceEdge t i)).parameterization.source.cellCarrier s)) : IsAffineOn (faceBoundaryMap t) E

On a middle piece, affinity follows once its pulled-back source image lies in one face of the finite polygonal segment model.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundarySubdivision_middleSource {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) {u : Finset (faceBoundarySubdivision t).Vertex} (hu : u ∈ (faceBoundarySubdivision t).simplexes) (hui : (faceBoundarySubdivision t).cellCarrier u ⊆ standardTrianglePlaneComplex.cellCarrier (faceStandardEdge i)) (hcard : u.card = 2) (hmid0 : ∀ p ∈ (faceBoundarySubdivision t).cellCarrier u, 1 / 2 ≤ (faceEdgeParameterAffine t i) p) (hmid1 : ∀ p ∈ (faceBoundarySubdivision t).cellCarrier u, (faceEdgeParameterAffine t i) p ≤ 3 / 4) : ∃ s ∈ (K.replacementArc hcont hinj D C (K.faceEdge t i)).parameterization.source.simplexes, Set.MapsTo (fun (p : Plane) => (edgeMiddleSourceMap (K.replacementArc hcont hinj D C (K.faceEdge t i))) ((K.facePlaneInverseAffine t) p)) ((faceBoundarySubdivision t).cellCarrier u) ((K.replacementArc hcont hinj D C (K.faceEdge t i)).parameterization.source.cellCarrier s)

The marked middle-model vertices ensure that the pulled-back image of a two-vertex subdivision face is contained in one face of the finite segment model.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryMap_affineOn_subdivision {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) (u : Finset (faceBoundarySubdivision t).Vertex) : u ∈ (faceBoundarySubdivision t).simplexes → IsAffineOn (faceBoundaryMap t) ((faceBoundarySubdivision t).cellCarrier u)

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

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.IntrinsicTwoComplex.faceBoundaryMap_isPLOnSet {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) : IsPLOnSet (frontier standardFaceRegion) (faceBoundaryMap t)

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