Polygonal realization of Gallier--Xu P2

This file packages the local two-disk cut model from DiskSquare for finite cyclic presentations. The first layer normalizes the cyclic position of a nondegenerate positively oriented cut and supplies an exact selected-face homeomorphism. It is deliberately stated in terms of the existing P2Cut data, so the presentation-level quotient comparison can use the same side indices and no second formulation of P2 is introduced.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.sourceBoundaryLength_eq_cutLength (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (P.boundary cut.face.face).length = cut.left.length + cut.right.length

The selected source face has as many stored sides as the two linear cut pieces together.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveCutRotation (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : ℕ

Rotation of the linear cut word that recovers the stored source boundary. This version is used after reducing to the positive traversal orientation.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveCutRotation P cut horientation = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rotate_cutBoundary_eq_sourceBoundary (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : (cut.left ++ cut.right).rotate (positiveCutRotation P cut horientation) = P.boundary cut.face.face

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveCutSideIndex (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (_hr : 0 < cut.right.length) (i : Fin (P.boundary cut.face.face).length) : Fin (cut.left.length + cut.right.length)

The linear cut-word index carrying a stored source side.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveCutSideIndex_val (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (i : Fin (P.boundary cut.face.face).length) : ↑(positiveCutSideIndex P cut horientation hl hr i) = (↑i + positiveCutRotation P cut horientation) % (cut.left.length + cut.right.length)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveCutSideIndex_injective (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) : Function.Injective (positiveCutSideIndex P cut horientation hl hr)

Cyclic alignment of the source boundary is injective on side indices.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveCutSideIndex_surjective (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) : Function.Surjective (positiveCutSideIndex P cut horientation hl hr)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.cutBoundary_get_positiveCutSideIndex (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (i : Fin (P.boundary cut.face.face).length) : (cut.left ++ cut.right)[↑(positiveCutSideIndex P cut horientation hl hr i)] = (P.boundary cut.face.face)[↑i]

Lookup at the rotated linear cut index recovers the stored source dart.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedCellHomeomorph (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) : PolygonCell (P.boundary cut.face.face).length ≃ₜ DiskSquare.ParamChildGluing cut.left.length cut.right.length

The selected source face, with its cyclic starting point aligned to the cut, is exactly the local one-polygon-to-two-child quotient model.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedCellHomeomorph_side (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (i : Fin (P.boundary cut.face.face).length) (t : ↑unitInterval) : (positiveSelectedCellHomeomorph P cut horientation hl hr) ((PolygonCell.side i) t) = (DiskSquare.sourceChildGluingHomeomorph cut.left.length cut.right.length hl hr) ((PolygonCell.side (positiveCutSideIndex P cut horientation hl hr i)) t)

Exact side computation for the cyclically aligned selected-face homeomorphism.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveLeftSideIndex (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (i : Fin (P.boundary cut.face.face).length) (hleft : ↑(positiveCutSideIndex P cut horientation hl hr i) < cut.left.length) : Fin cut.left.length

A rotated source side lying in the left cut piece, viewed with its local left index.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveLeftSideIndex_val (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (i : Fin (P.boundary cut.face.face).length) (hleft : ↑(positiveCutSideIndex P cut horientation hl hr i) < cut.left.length) : ↑(positiveLeftSideIndex P cut horientation hl hr i hleft) = ↑(positiveCutSideIndex P cut horientation hl hr i)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRightSideIndex (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (i : Fin (P.boundary cut.face.face).length) (hright : cut.left.length ≤ ↑(positiveCutSideIndex P cut horientation hl hr i)) : Fin cut.right.length

A rotated source side lying in the right cut piece, viewed with its local right index.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRightSideIndex_val (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (i : Fin (P.boundary cut.face.face).length) (hright : cut.left.length ≤ ↑(positiveCutSideIndex P cut horientation hl hr i)) : ↑(positiveRightSideIndex P cut horientation hl hr i hright) = ↑(positiveCutSideIndex P cut horientation hl hr i) - cut.left.length

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.left_get_positiveLeftSideIndex (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (i : Fin (P.boundary cut.face.face).length) (hleft : ↑(positiveCutSideIndex P cut horientation hl hr i) < cut.left.length) : cut.left.get (positiveLeftSideIndex P cut horientation hl hr i hleft) = (P.boundary cut.face.face).get i

In the left branch, the local cut-piece lookup is the stored source dart.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.right_get_positiveRightSideIndex (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (i : Fin (P.boundary cut.face.face).length) (hright : cut.left.length ≤ ↑(positiveCutSideIndex P cut horientation hl hr i)) : cut.right.get (positiveRightSideIndex P cut horientation hl hr i hright) = (P.boundary cut.face.face).get i

In the right branch, the local cut-piece lookup is the stored source dart.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedCellHomeomorph_side_of_lt (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (i : Fin (P.boundary cut.face.face).length) (t : ↑unitInterval) (hleft : ↑(positiveCutSideIndex P cut horientation hl hr i) < cut.left.length) : (positiveSelectedCellHomeomorph P cut horientation hl hr) ((PolygonCell.side i) t) = Quotient.mk'' (Sum.inl ((PolygonCell.side (Fin.castAdd 1 (positiveLeftSideIndex P cut horientation hl hr i hleft))) t))

Exact selected-face computation for a side belonging to the left cut piece.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedCellHomeomorph_side_of_not_lt (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (i : Fin (P.boundary cut.face.face).length) (t : ↑unitInterval) (hright : cut.left.length ≤ ↑(positiveCutSideIndex P cut horientation hl hr i)) : (positiveSelectedCellHomeomorph P cut horientation hl hr) ((PolygonCell.side i) t) = Quotient.mk'' (Sum.inr ((PolygonCell.side ((positiveRightSideIndex P cut horientation hl hr i hright).addNat 1)) t))

Exact selected-face computation for a side belonging to the right cut piece.

The fresh seam inside the actual split presentation

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positive_split_boundary_selected_length (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : ((split P cut).boundary (oldFace P cut cut.face.face)).length = cut.left.length + 1

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positive_split_boundary_right_length (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : ((split P cut).boundary (rightFace P cut)).length = cut.right.length + 1

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedFreshIndex (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : Fin ((split P cut).boundary (oldFace P cut cut.face.face)).length

Stored target index of the positive fresh dart in the selected child.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedFreshIndex P cut horientation = ⟨cut.left.length, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedFreshIndex_val (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : ↑(positiveSelectedFreshIndex P cut horientation) = cut.left.length

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRightFreshIndex (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : Fin ((split P cut).boundary (rightFace P cut)).length

Stored target index of the negative fresh dart in the right child.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRightFreshIndex P cut horientation = ⟨0, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRightFreshIndex_val (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : ↑(positiveRightFreshIndex P cut horientation) = 0

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedFreshOccurrence (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : (split P cut).BoundaryOccurrence

The selected child's fresh-edge boundary occurrence.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRightFreshOccurrence (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : (split P cut).BoundaryOccurrence

The right child's fresh-edge boundary occurrence.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedBoundary_get_fresh (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : (selectedBoundary P cut).get ⟨cut.left.length, ⋯⟩ = SurfaceCellComplex.SignedDart.pos (freshEdge P)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRightBoundary_get_fresh (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : (rightBoundary P cut).get ⟨0, ⋯⟩ = SurfaceCellComplex.SignedDart.neg (freshEdge P)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedFreshOccurrence_dart (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : (positiveSelectedFreshOccurrence P cut horientation).dart = SurfaceCellComplex.SignedDart.pos (freshEdge P)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRightFreshOccurrence_dart (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : (positiveRightFreshOccurrence P cut horientation).dart = SurfaceCellComplex.SignedDart.neg (freshEdge P)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedFreshOccurrence_edge (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : (positiveSelectedFreshOccurrence P cut horientation).edge = freshEdge P

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRightFreshOccurrence_edge (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : (positiveRightFreshOccurrence P cut horientation).edge = freshEdge P

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedFreshOccurrence_ne_right (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : positiveSelectedFreshOccurrence P cut horientation ≠ positiveRightFreshOccurrence P cut horientation

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveFresh_not_boundary (P : FiniteCyclicPresentation) (cut : P.P2Cut) : ¬(split P cut).IsBoundaryEdge (freshEdge P)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveFreshPairing (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : (split P cut).BoundaryPairing

The exact reversed-parameter pairing carried by the fresh P2 seam.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveFreshPairing_source (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : (positiveFreshPairing P cut horientation).source = positiveSelectedFreshOccurrence P cut horientation

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveFreshPairing_target (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : (positiveFreshPairing P cut horientation).target = positiveRightFreshOccurrence P cut horientation

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveFreshPairing_direction (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : (positiveFreshPairing P cut horientation).direction = PolygonGluing.ParameterDirection.opposite

Embedding the local child quotient in the target realization

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedChildCellHomeomorph (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : PolygonCell (cut.left.length + 1) ≃ₜ PolygonCell ((split P cut).boundary (oldFace P cut cut.face.face)).length

Phantom side-count transport from the local selected child to the actual target face.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRightChildCellHomeomorph (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : PolygonCell (cut.right.length + 1) ≃ₜ PolygonCell ((split P cut).boundary (rightFace P cut)).length

Phantom side-count transport from the local right child to the actual target face.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedChildSideIndex (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (i : Fin (cut.left.length + 1)) : Fin ((split P cut).boundary (oldFace P cut cut.face.face)).length

The target selected-child index corresponding to a local child side.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedChildSideIndex P cut horientation i = ⟨↑i, ⋯⟩

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRightChildSideIndex (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (i : Fin (cut.right.length + 1)) : Fin ((split P cut).boundary (rightFace P cut)).length

The target right-child index corresponding to a local child side.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRightChildSideIndex P cut horientation i = ⟨↑i, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedChildCellHomeomorph_side (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (i : Fin (cut.left.length + 1)) (t : ↑unitInterval) : (positiveSelectedChildCellHomeomorph P cut horientation) ((PolygonCell.side i) t) = (PolygonCell.side (positiveSelectedChildSideIndex P cut horientation i)) t

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRightChildCellHomeomorph_side (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (i : Fin (cut.right.length + 1)) (t : ↑unitInterval) : (positiveRightChildCellHomeomorph P cut horientation) ((PolygonCell.side i) t) = (PolygonCell.side (positiveRightChildSideIndex P cut horientation i)) t

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveChildPairPreMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : DiskSquare.ChildPair cut.left.length cut.right.length → (split P cut).PolygonalPreRealization

Include the two local child cells into the corresponding two faces of the split pre-realization.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_positiveChildPairPreMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : Continuous (positiveChildPairPreMap P cut horientation)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveChildPairPreMap_inl (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (z : PolygonCell (cut.left.length + 1)) : positiveChildPairPreMap P cut horientation (Sum.inl z) = ⟨oldFace P cut cut.face.face, (positiveSelectedChildCellHomeomorph P cut horientation) z⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveChildPairPreMap_inr (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (z : PolygonCell (cut.right.length + 1)) : positiveChildPairPreMap P cut horientation (Sum.inr z) = ⟨rightFace P cut, (positiveRightChildCellHomeomorph P cut horientation) z⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveChildPairMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (validP : P.IsSurfaceValid) : DiskSquare.ChildPair cut.left.length cut.right.length → (split P cut).PolygonalRealization ⋯

Send a local child point to its class in the complete split realization.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_positiveChildPairMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (validP : P.IsSurfaceValid) : Continuous (positiveChildPairMap P cut horientation validP)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveChildPairPreMap_fresh_inl (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (t : ↑unitInterval) : positiveChildPairPreMap P cut horientation (Sum.inl ((PolygonCell.side (Fin.last cut.left.length)) t)) = ((split P cut).occurrenceSide (positiveSelectedFreshOccurrence P cut horientation)).point t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveChildPairPreMap_fresh_inr (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (t : ↑unitInterval) : positiveChildPairPreMap P cut horientation (Sum.inr ((PolygonCell.side 0) t)) = ((split P cut).occurrenceSide (positiveRightFreshOccurrence P cut horientation)).point t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveChildPairMap_fresh_seam (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (validP : P.IsSurfaceValid) (t : ↑unitInterval) : positiveChildPairMap P cut horientation validP (Sum.inl ((PolygonCell.side (Fin.last cut.left.length)) t)) = positiveChildPairMap P cut horientation validP (Sum.inr ((PolygonCell.side 0) (unitInterval.symm t)))

The local seam generator is exactly the fresh-edge gluing already present in the target polygonal quotient.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveChildPairMap_respects (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (validP : P.IsSurfaceValid) {x y : DiskSquare.ChildPair cut.left.length cut.right.length} (hxy : Relation.EqvGen (DiskSquare.ParamChildSeamGenerator cut.left.length cut.right.length) x y) : positiveChildPairMap P cut horientation validP x = positiveChildPairMap P cut horientation validP y

The target quotient map is constant on the complete local child-seam relation.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveChildGluingMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (validP : P.IsSurfaceValid) : DiskSquare.ParamChildGluing cut.left.length cut.right.length → (split P cut).PolygonalRealization ⋯

Include the locally glued pair of P2 children into the complete target realization.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_positiveChildGluingMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (validP : P.IsSurfaceValid) : Continuous (positiveChildGluingMap P cut horientation validP)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveChildGluingMap_mk (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (validP : P.IsSurfaceValid) (x : DiskSquare.ChildPair cut.left.length cut.right.length) : positiveChildGluingMap P cut horientation validP (Quotient.mk'' x) = positiveChildPairMap P cut horientation validP x

The selected source face as a map into the split realization

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : PolygonCell (P.boundary cut.face.face).length → (split P cut).PolygonalRealization ⋯

The positive, nondegenerate selected source face, cut into the two target children and then included in the complete split quotient.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_positiveSelectedFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : Continuous (positiveSelectedFaceMap P cut horientation hl hr validP)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedFaceMap_side_of_lt (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (i : Fin (P.boundary cut.face.face).length) (t : ↑unitInterval) (hleft : ↑(positiveCutSideIndex P cut horientation hl hr i) < cut.left.length) : positiveSelectedFaceMap P cut horientation hl hr validP ((PolygonCell.side i) t) = (split P cut).polygonalMk ⋯ ⟨oldFace P cut cut.face.face, (PolygonCell.side (positiveSelectedChildSideIndex P cut horientation (Fin.castAdd 1 (positiveLeftSideIndex P cut horientation hl hr i hleft)))) t⟩

A selected source side in the left cut piece lands on the exact old side of the selected target child.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedFaceMap_side_of_not_lt (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (i : Fin (P.boundary cut.face.face).length) (t : ↑unitInterval) (hright : cut.left.length ≤ ↑(positiveCutSideIndex P cut horientation hl hr i)) : positiveSelectedFaceMap P cut horientation hl hr validP ((PolygonCell.side i) t) = (split P cut).polygonalMk ⋯ ⟨rightFace P cut, (PolygonCell.side (positiveRightChildSideIndex P cut horientation ((positiveRightSideIndex P cut horientation hl hr i hright).addNat 1))) t⟩

A selected source side in the right cut piece lands on the exact old side of the right target child.

The complete forward pre-realization map

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.split_boundary_old_length_of_ne (P : FiniteCyclicPresentation) (cut : P.P2Cut) {f : P.Face} (hface : f ≠ cut.face.face) : ((split P cut).boundary (oldFace P cut f)).length = (P.boundary f).length

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.retainedCellHomeomorph (P : FiniteCyclicPresentation) (cut : P.P2Cut) {f : P.Face} (hface : f ≠ cut.face.face) : PolygonCell (P.boundary f).length ≃ₜ PolygonCell ((split P cut).boundary (oldFace P cut f)).length

A retained source face differs from its target copy only by a phantom side-count equality.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.retainedCellHomeomorph P cut hface = LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.rotateHomeomorph ⋯ 0

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.retainedSideIndex (P : FiniteCyclicPresentation) (cut : P.P2Cut) {f : P.Face} (hface : f ≠ cut.face.face) (i : Fin (P.boundary f).length) : Fin ((split P cut).boundary (oldFace P cut f)).length

Target index corresponding to a side of a retained source face.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.retainedSideIndex P cut hface i = ⟨↑i, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.retainedCellHomeomorph_side (P : FiniteCyclicPresentation) (cut : P.P2Cut) {f : P.Face} (hface : f ≠ cut.face.face) (i : Fin (P.boundary f).length) (t : ↑unitInterval) : (retainedCellHomeomorph P cut hface) ((PolygonCell.side i) t) = (PolygonCell.side (retainedSideIndex P cut hface i)) t

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.retainedFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) {f : P.Face} (hface : f ≠ cut.face.face) (validP : P.IsSurfaceValid) : PolygonCell (P.boundary f).length → (split P cut).PolygonalRealization ⋯

A retained face maps directly to its unchanged target face class.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_retainedFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) {f : P.Face} (hface : f ≠ cut.face.face) (validP : P.IsSurfaceValid) : Continuous (retainedFaceMap P cut hface validP)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (f : P.Face) : PolygonCell (P.boundary f).length → (split P cut).PolygonalRealization ⋯

Facewise forward map: cut the selected face and retain every other face.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_positiveFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (f : P.Face) : Continuous (positiveFaceMap P cut horientation hl hr validP f)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positivePreMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : P.PolygonalPreRealization → (split P cut).PolygonalRealization ⋯

Continuous forward map on the entire source polygonal pre-realization.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_positivePreMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : Continuous (positivePreMap P cut horientation hl hr validP)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positivePreMap_selected (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (z : PolygonCell (P.boundary cut.face.face).length) : positivePreMap P cut horientation hl hr validP ⟨cut.face.face, z⟩ = positiveSelectedFaceMap P cut horientation hl hr validP z

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positivePreMap_retained (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) {f : P.Face} (hface : f ≠ cut.face.face) (z : PolygonCell (P.boundary f).length) : positivePreMap P cut horientation hl hr validP ⟨f, z⟩ = retainedFaceMap P cut hface validP z

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positivePreMap_selected_side_of_lt (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (i : Fin (P.boundary cut.face.face).length) (t : ↑unitInterval) (hleft : ↑(positiveCutSideIndex P cut horientation hl hr i) < cut.left.length) : positivePreMap P cut horientation hl hr validP ⟨cut.face.face, (PolygonCell.side i) t⟩ = (split P cut).polygonalMk ⋯ ⟨oldFace P cut cut.face.face, (PolygonCell.side (positiveSelectedChildSideIndex P cut horientation (Fin.castAdd 1 (positiveLeftSideIndex P cut horientation hl hr i hleft)))) t⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positivePreMap_selected_side_of_not_lt (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (i : Fin (P.boundary cut.face.face).length) (t : ↑unitInterval) (hright : cut.left.length ≤ ↑(positiveCutSideIndex P cut horientation hl hr i)) : positivePreMap P cut horientation hl hr validP ⟨cut.face.face, (PolygonCell.side i) t⟩ = (split P cut).polygonalMk ⋯ ⟨rightFace P cut, (PolygonCell.side (positiveRightChildSideIndex P cut horientation ((positiveRightSideIndex P cut horientation hl hr i hright).addNat 1))) t⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positivePreMap_retained_side (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) {f : P.Face} (hface : f ≠ cut.face.face) (i : Fin (P.boundary f).length) (t : ↑unitInterval) : positivePreMap P cut horientation hl hr validP ⟨f, (PolygonCell.side i) t⟩ = (split P cut).polygonalMk ⋯ ⟨oldFace P cut f, (PolygonCell.side (retainedSideIndex P cut hface i)) t⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.oldFace_injective (P : FiniteCyclicPresentation) (cut : P.P2Cut) : Function.Injective (oldFace P cut)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.oldFace_ne_rightFace (P : FiniteCyclicPresentation) (cut : P.P2Cut) (f : P.Face) : oldFace P cut f ≠ rightFace P cut

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveMapOccurrence (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (o : P.BoundaryOccurrence) : (split P cut).BoundaryOccurrence

Transport a source boundary occurrence to the child or retained target face that carries the same old edge after a positive nondegenerate split.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveMapOccurrence_selected_of_lt (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (i : Fin (P.boundary cut.face.face).length) (hleft : ↑(positiveCutSideIndex P cut horientation hl hr i) < cut.left.length) : positiveMapOccurrence P cut horientation hl hr ⟨cut.face.face, i⟩ = ⟨oldFace P cut cut.face.face, positiveSelectedChildSideIndex P cut horientation (Fin.castAdd 1 (positiveLeftSideIndex P cut horientation hl hr i hleft))⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveMapOccurrence_selected_of_not_lt (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (i : Fin (P.boundary cut.face.face).length) (hleft : ¬↑(positiveCutSideIndex P cut horientation hl hr i) < cut.left.length) : positiveMapOccurrence P cut horientation hl hr ⟨cut.face.face, i⟩ = ⟨rightFace P cut, positiveRightChildSideIndex P cut horientation ((positiveRightSideIndex P cut horientation hl hr i ⋯).addNat 1)⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveMapOccurrence_retained (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) {f : P.Face} (hface : f ≠ cut.face.face) (i : Fin (P.boundary f).length) : positiveMapOccurrence P cut horientation hl hr ⟨f, i⟩ = ⟨oldFace P cut f, retainedSideIndex P cut hface i⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positivePreMap_occurrenceSide (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (o : P.BoundaryOccurrence) (t : ↑unitInterval) : positivePreMap P cut horientation hl hr validP ((P.occurrenceSide o).point t) = (split P cut).polygonalMk ⋯ (((split P cut).occurrenceSide (positiveMapOccurrence P cut horientation hl hr o)).point t)

Exact side-point computation for the complete forward occurrence transport.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveMapOccurrence_dart (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (o : P.BoundaryOccurrence) : (positiveMapOccurrence P cut horientation hl hr o).dart = P1.castSuccDart o.dart

The transported occurrence carries exactly the retained old dart.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveMapOccurrence_edge (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (o : P.BoundaryOccurrence) : (positiveMapOccurrence P cut horientation hl hr o).edge = Fin.castSucc o.edge

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveMapOccurrence_injective (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) : Function.Injective (positiveMapOccurrence P cut horientation hl hr)

Distinct source boundary positions remain distinct after routing the selected face between its two P2 children.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveMapPairing (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (pairing : P.BoundaryPairing) : (split P cut).BoundaryPairing

Transport an old-edge source pairing to the corresponding pairing of target occurrences.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveMapPairing_source (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (pairing : P.BoundaryPairing) : (positiveMapPairing P cut horientation hl hr pairing).source = positiveMapOccurrence P cut horientation hl hr pairing.source

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveMapPairing_target (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (pairing : P.BoundaryPairing) : (positiveMapPairing P cut horientation hl hr pairing).target = positiveMapOccurrence P cut horientation hl hr pairing.target

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveMapPairing_direction (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (pairing : P.BoundaryPairing) : (positiveMapPairing P cut horientation hl hr pairing).direction = pairing.direction

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positivePreMap_pairing_eq (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (pairing : P.BoundaryPairing) (t : ↑unitInterval) : positivePreMap P cut horientation hl hr validP (pairing.identification.source.point t) = positivePreMap P cut horientation hl hr validP (pairing.identification.target.point (pairing.identification.parameter t))

Every source gluing generator has equal images under the complete forward P2 map.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positivePreMap_respects (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) {x y : P.PolygonalPreRealization} (hxy : (P.PolygonalGluingRel validP) x y) : positivePreMap P cut horientation hl hr validP x = positivePreMap P cut horientation hl hr validP y

The forward pre-map is constant on the complete source gluing relation.

Local inverse maps for the two target children

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveChildGluingInvMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : DiskSquare.ParamChildGluing cut.left.length cut.right.length → P.PolygonalRealization validP

Collapse the local child quotient back to the selected source face class.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_positiveChildGluingInvMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : Continuous (positiveChildGluingInvMap P cut horientation hl hr validP)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveChildGluingInvMap_selectedCell (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (z : PolygonCell (P.boundary cut.face.face).length) : positiveChildGluingInvMap P cut horientation hl hr validP ((positiveSelectedCellHomeomorph P cut horientation hl hr) z) = P.polygonalMk validP ⟨cut.face.face, z⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedChildToGluing (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : PolygonCell ((split P cut).boundary (oldFace P cut cut.face.face)).length → DiskSquare.ParamChildGluing cut.left.length cut.right.length

Include a point of the actual selected target child into the local child quotient.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_positiveSelectedChildToGluing (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : Continuous (positiveSelectedChildToGluing P cut horientation)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRightChildToGluing (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : PolygonCell ((split P cut).boundary (rightFace P cut)).length → DiskSquare.ParamChildGluing cut.left.length cut.right.length

Include a point of the actual right target child into the local child quotient.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_positiveRightChildToGluing (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) : Continuous (positiveRightChildToGluing P cut horientation)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedChildToGluing_apply (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (z : PolygonCell (cut.left.length + 1)) : positiveSelectedChildToGluing P cut horientation ((positiveSelectedChildCellHomeomorph P cut horientation) z) = Quotient.mk'' (Sum.inl z)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRightChildToGluing_apply (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (z : PolygonCell (cut.right.length + 1)) : positiveRightChildToGluing P cut horientation ((positiveRightChildCellHomeomorph P cut horientation) z) = Quotient.mk'' (Sum.inr z)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedChildInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : PolygonCell ((split P cut).boundary (oldFace P cut cut.face.face)).length → P.PolygonalRealization validP

Inverse map on the selected target child.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_positiveSelectedChildInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : Continuous (positiveSelectedChildInvFaceMap P cut horientation hl hr validP)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRightChildInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : PolygonCell ((split P cut).boundary (rightFace P cut)).length → P.PolygonalRealization validP

Inverse map on the right target child.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_positiveRightChildInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : Continuous (positiveRightChildInvFaceMap P cut horientation hl hr validP)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.retainedInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) {f : P.Face} (hface : f ≠ cut.face.face) (validP : P.IsSurfaceValid) : PolygonCell ((split P cut).boundary (oldFace P cut f)).length → P.PolygonalRealization validP

Inverse map on a retained target face.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_retainedInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) {f : P.Face} (hface : f ≠ cut.face.face) (validP : P.IsSurfaceValid) : Continuous (retainedInvFaceMap P cut hface validP)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.retainedInvFaceMap_apply (P : FiniteCyclicPresentation) (cut : P.P2Cut) {f : P.Face} (hface : f ≠ cut.face.face) (validP : P.IsSurfaceValid) (z : PolygonCell (P.boundary f).length) : retainedInvFaceMap P cut hface validP ((retainedCellHomeomorph P cut hface) z) = P.polygonalMk validP ⟨f, z⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveOldInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (f : P.Face) : PolygonCell ((split P cut).boundary (oldFace P cut f)).length → P.PolygonalRealization validP

Inverse map at an old target-face position, selecting the cut-child inverse exactly at the chosen source face.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_positiveOldInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (f : P.Face) : Continuous (positiveOldInvFaceMap P cut horientation hl hr validP f)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveIndexedInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (j : Fin (P.faces.length + 1)) : PolygonCell ((split P cut).boundary ((faceEquiv P cut) j)).length → P.PolygonalRealization validP

Inverse face map indexed before applying the explicit target faceEquiv.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveIndexedInvFaceMap_last (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : positiveIndexedInvFaceMap P cut horientation hl hr validP (Fin.last P.faces.length) = positiveRightChildInvFaceMap P cut horientation hl hr validP

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveIndexedInvFaceMap_castSucc (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (f : P.Face) : positiveIndexedInvFaceMap P cut horientation hl hr validP (Fin.castSucc f) = positiveOldInvFaceMap P cut horientation hl hr validP f

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_positiveIndexedInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (j : Fin (P.faces.length + 1)) : Continuous (positiveIndexedInvFaceMap P cut horientation hl hr validP j)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (q : (split P cut).Face) : PolygonCell ((split P cut).boundary q).length → P.PolygonalRealization validP

Inverse face map on the actual target face type.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_positiveInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (q : (split P cut).Face) : Continuous (positiveInvFaceMap P cut horientation hl hr validP q)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveInvFaceMap_oldFace (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (f : P.Face) : positiveInvFaceMap P cut horientation hl hr validP (oldFace P cut f) = positiveOldInvFaceMap P cut horientation hl hr validP f

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveInvFaceMap_rightFace (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : positiveInvFaceMap P cut horientation hl hr validP (rightFace P cut) = positiveRightChildInvFaceMap P cut horientation hl hr validP

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveInvPreMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : (split P cut).PolygonalPreRealization → P.PolygonalRealization validP

Continuous inverse map on the complete split polygonal pre-realization.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_positiveInvPreMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : Continuous (positiveInvPreMap P cut horientation hl hr validP)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveInvPreMap_oldFace (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (f : P.Face) (z : PolygonCell ((split P cut).boundary (oldFace P cut f)).length) : positiveInvPreMap P cut horientation hl hr validP ⟨oldFace P cut f, z⟩ = positiveOldInvFaceMap P cut horientation hl hr validP f z

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveInvPreMap_rightFace (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (z : PolygonCell ((split P cut).boundary (rightFace P cut)).length) : positiveInvPreMap P cut horientation hl hr validP ⟨rightFace P cut, z⟩ = positiveRightChildInvFaceMap P cut horientation hl hr validP z

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveOldInvFaceMap_selected (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : positiveOldInvFaceMap P cut horientation hl hr validP cut.face.face = positiveSelectedChildInvFaceMap P cut horientation hl hr validP

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveOldInvFaceMap_retained (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) {f : P.Face} (hface : f ≠ cut.face.face) : positiveOldInvFaceMap P cut horientation hl hr validP f = retainedInvFaceMap P cut hface validP

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveSelectedChildInvFaceMap_apply (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (z : PolygonCell (cut.left.length + 1)) : positiveSelectedChildInvFaceMap P cut horientation hl hr validP ((positiveSelectedChildCellHomeomorph P cut horientation) z) = positiveChildGluingInvMap P cut horientation hl hr validP (Quotient.mk'' (Sum.inl z))

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRightChildInvFaceMap_apply (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (z : PolygonCell (cut.right.length + 1)) : positiveRightChildInvFaceMap P cut horientation hl hr validP ((positiveRightChildCellHomeomorph P cut horientation) z) = positiveChildGluingInvMap P cut horientation hl hr validP (Quotient.mk'' (Sum.inr z))

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveInvPreMap_retained_apply (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) {f : P.Face} (hface : f ≠ cut.face.face) (z : PolygonCell (P.boundary f).length) : positiveInvPreMap P cut horientation hl hr validP ⟨oldFace P cut f, (retainedCellHomeomorph P cut hface) z⟩ = P.polygonalMk validP ⟨f, z⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveInvPreMap_selectedChild_apply (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (z : PolygonCell (cut.left.length + 1)) : positiveInvPreMap P cut horientation hl hr validP ⟨oldFace P cut cut.face.face, (positiveSelectedChildCellHomeomorph P cut horientation) z⟩ = positiveChildGluingInvMap P cut horientation hl hr validP (Quotient.mk'' (Sum.inl z))

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveInvPreMap_rightChild_apply (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (z : PolygonCell (cut.right.length + 1)) : positiveInvPreMap P cut horientation hl hr validP ⟨rightFace P cut, (positiveRightChildCellHomeomorph P cut horientation) z⟩ = positiveChildGluingInvMap P cut horientation hl hr validP (Quotient.mk'' (Sum.inr z))

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveInvPreMap_fresh_seam (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (t : ↑unitInterval) : positiveInvPreMap P cut horientation hl hr validP ⟨oldFace P cut cut.face.face, (positiveSelectedChildCellHomeomorph P cut horientation) ((PolygonCell.side (Fin.last cut.left.length)) t)⟩ = positiveInvPreMap P cut horientation hl hr validP ⟨rightFace P cut, (positiveRightChildCellHomeomorph P cut horientation) ((PolygonCell.side 0) (unitInterval.symm t))⟩

The inverse pre-map identifies the target's fresh seam for the same local quotient reason used by the forward construction.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveInvPreMap_mapOccurrence_side (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (o : P.BoundaryOccurrence) (t : ↑unitInterval) : positiveInvPreMap P cut horientation hl hr validP (((split P cut).occurrenceSide (positiveMapOccurrence P cut horientation hl hr o)).point t) = P.polygonalMk validP ((P.occurrenceSide o).point t)

On every old boundary side, the inverse pre-map exactly undoes occurrence transport.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.exists_positiveMapOccurrence_eq_of_edge_castSucc (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (q : (split P cut).BoundaryOccurrence) (e : P.Edge) (hedge : q.edge = Fin.castSucc e) : ∃ (o : P.BoundaryOccurrence), positiveMapOccurrence P cut horientation hl hr o = q

Every target boundary occurrence on an old edge is the transported copy of a source occurrence. The two omitted target occurrences are exactly the fresh seam.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.targetPairing_edge_eq_source_edge {P : FiniteCyclicPresentation} (pairing : P.BoundaryPairing) : pairing.target.edge = pairing.source.edge

Compatible boundary occurrences in a pairing carry the same unoriented edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.targetPairing_direction_eq_of_source_target_eq {P : FiniteCyclicPresentation} (p q : P.BoundaryPairing) (hsource : p.source = q.source) (htarget : p.target = q.target) : p.direction = q.direction

Once source and target occurrences agree, compatibility forces the same parameter direction.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.targetPairing_eq_of_source_target_direction_eq {P : FiniteCyclicPresentation} (p q : P.BoundaryPairing) (hsource : p.source = q.source) (htarget : p.target = q.target) (hdirection : p.direction = q.direction) : p = q

Boundary pairings are determined by their two occurrences and parameter direction.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveFreshOccurrence_cases (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (validP : P.IsSurfaceValid) (q : (split P cut).BoundaryOccurrence) (hedge : q.edge = freshEdge P) : q = positiveSelectedFreshOccurrence P cut horientation ∨ q = positiveRightFreshOccurrence P cut horientation

The two explicitly constructed fresh occurrences exhaust the fresh edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.exists_positiveMapPairing_eq_of_source_edge_castSucc (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (q : (split P cut).BoundaryPairing) (e : P.Edge) (hsourceEdge : q.source.edge = Fin.castSucc e) : ∃ (r : P.BoundaryPairing), positiveMapPairing P cut horientation hl hr r = q

A target pairing based at an old edge is exactly the transported pairing of the two corresponding source occurrences.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveInvPreMap_fresh_occurrence_seam (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (t : ↑unitInterval) : positiveInvPreMap P cut horientation hl hr validP (((split P cut).occurrenceSide (positiveSelectedFreshOccurrence P cut horientation)).point t) = positiveInvPreMap P cut horientation hl hr validP (((split P cut).occurrenceSide (positiveRightFreshOccurrence P cut horientation)).point (unitInterval.symm t))

Occurrence-side form of the exact fresh-seam equality for the inverse pre-map.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveInvPreMap_pairing_eq (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (q : (split P cut).BoundaryPairing) (t : ↑unitInterval) : positiveInvPreMap P cut horientation hl hr validP (q.identification.source.point t) = positiveInvPreMap P cut horientation hl hr validP (q.identification.target.point (q.identification.parameter t))

The inverse pre-map identifies every target gluing generator: old-edge generators are transported source pairings, while the final edge is the fresh child seam.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveInvPreMap_respects (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) {x y : (split P cut).PolygonalPreRealization} (hxy : ((split P cut).PolygonalGluingRel ⋯) x y) : positiveInvPreMap P cut horientation hl hr validP x = positiveInvPreMap P cut horientation hl hr validP y

The inverse pre-map is constant on the complete target gluing relation.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRealizationMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : P.PolygonalRealization validP → (split P cut).PolygonalRealization ⋯

Forward map after descent through the source polygonal quotient.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRealizationInvMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : (split P cut).PolygonalRealization ⋯ → P.PolygonalRealization validP

Inverse map after descent through the target polygonal quotient.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRealizationMap_polygonalMk (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (x : P.PolygonalPreRealization) : positiveRealizationMap P cut horientation hl hr validP (P.polygonalMk validP x) = positivePreMap P cut horientation hl hr validP x

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRealizationInvMap_polygonalMk (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (y : (split P cut).PolygonalPreRealization) : positiveRealizationInvMap P cut horientation hl hr validP ((split P cut).polygonalMk ⋯ y) = positiveInvPreMap P cut horientation hl hr validP y

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRealizationInvMap_childGluing (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (q : DiskSquare.ParamChildGluing cut.left.length cut.right.length) : positiveRealizationInvMap P cut horientation hl hr validP (positiveChildGluingMap P cut horientation validP q) = positiveChildGluingInvMap P cut horientation hl hr validP q

On the locally glued child pair, the descended inverse is the explicit collapse map.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRealizationMap_childGluingInv (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (q : DiskSquare.ParamChildGluing cut.left.length cut.right.length) : positiveRealizationMap P cut horientation hl hr validP (positiveChildGluingInvMap P cut horientation hl hr validP q) = positiveChildGluingMap P cut horientation validP q

The descended forward map sends the explicit child-collapse class back to the same local child quotient class.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveChildGluingMap_selectedChildToGluing (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (validP : P.IsSurfaceValid) (z : PolygonCell ((split P cut).boundary (oldFace P cut cut.face.face)).length) : positiveChildGluingMap P cut horientation validP (positiveSelectedChildToGluing P cut horientation z) = (split P cut).polygonalMk ⋯ ⟨oldFace P cut cut.face.face, z⟩

Including a selected-child point in the local child quotient and then in the global quotient is its ordinary polygonal quotient class.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveChildGluingMap_rightChildToGluing (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (validP : P.IsSurfaceValid) (z : PolygonCell ((split P cut).boundary (rightFace P cut)).length) : positiveChildGluingMap P cut horientation validP (positiveRightChildToGluing P cut horientation z) = (split P cut).polygonalMk ⋯ ⟨rightFace P cut, z⟩

Including a right-child point in the local child quotient and then in the global quotient is its ordinary polygonal quotient class.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRealization_left_inverse_mk (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (x : P.PolygonalPreRealization) : positiveRealizationInvMap P cut horientation hl hr validP (positivePreMap P cut horientation hl hr validP x) = P.polygonalMk validP x

The descended inverse is a left inverse on every source pre-realization point.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRealization_right_inverse_mk (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (y : (split P cut).PolygonalPreRealization) : positiveRealizationMap P cut horientation hl hr validP (positiveInvPreMap P cut horientation hl hr validP y) = (split P cut).polygonalMk ⋯ y

The descended forward map is a right inverse on every target pre-realization point.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRealizationEquivData (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : P.RealizationEquivData (split P cut) validP ⋯

Complete cut-and-paste certificate for a positive, nondegenerate P2 face split.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveRealizationHomeomorph (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : P.PolygonalRealization validP ≃ₜ (split P cut).PolygonalRealization ⋯

Explicit homeomorphism induced by a positive, nondegenerate P2 face split.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positivePolygonallyEquivalent (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : P.PolygonallyEquivalent (split P cut) validP ⋯

Propositional realization-invariance form for a positive, nondegenerate P2 face split.

Transport across reversal of the chosen cut orientation

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.flipFaceIndexEquiv (P : FiniteCyclicPresentation) (cut : P.P2Cut) : Fin (P.faces.length + 1) ≃ Fin (P.faces.length + 1)

Swap the selected-face position with the fresh right-child position.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.flipFaceIndexEquiv P cut = Equiv.swap (Fin.castSucc cut.face.face) (Fin.last P.faces.length)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.flipFaceEquiv (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (split P cut.flip).Face ≃ (split P cut).Face

Reversing a cut exchanges its two child faces and fixes every retained face.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.flipFaceEquiv_old_selected (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (flipFaceEquiv P cut) (oldFace P cut.flip cut.face.face) = rightFace P cut

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.flipFaceEquiv_right (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (flipFaceEquiv P cut) (rightFace P cut.flip) = oldFace P cut cut.face.face

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.flipFaceEquiv_old_of_ne (P : FiniteCyclicPresentation) (cut : P.P2Cut) {f : P.Face} (hface : f ≠ cut.face.face) : (flipFaceEquiv P cut) (oldFace P cut.flip f) = oldFace P cut f

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.swapFaceEquiv (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (split P cut.swap).Face ≃ (split P cut).Face

Swapping the two cut pieces exchanges the child faces and fixes every retained face.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.swapFaceEquiv_old_selected (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (swapFaceEquiv P cut) (oldFace P cut.swap cut.face.face) = rightFace P cut

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.swapFaceEquiv_right (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (swapFaceEquiv P cut) (rightFace P cut.swap) = oldFace P cut cut.face.face

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.swapFaceEquiv_old_of_ne (P : FiniteCyclicPresentation) (cut : P.P2Cut) {f : P.Face} (hface : f ≠ cut.face.face) : (swapFaceEquiv P cut) (oldFace P cut.swap f) = oldFace P cut f

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.swapRawEdgeRelabeling (P : FiniteCyclicPresentation) (_cut : P.P2Cut) : EdgeRelabeling (Fin (P.edgeCount + 1)) (Fin (P.edgeCount + 1))

The raw edge relabeling for a swapped cut reverses precisely the fresh edge.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.swapEdgeRelabeling (P : FiniteCyclicPresentation) (cut : P.P2Cut) : EdgeRelabeling (split P cut.swap).Edge (split P cut).Edge

The raw swapped-cut relabeling at the two split presentations' exact edge types.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.swapEdgeRelabeling_edgeEquiv (P : FiniteCyclicPresentation) (cut : P.P2Cut) (e : Fin (P.edgeCount + 1)) : (swapRawEdgeRelabeling P cut).edgeEquiv e = e

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.swapEdgeRelabeling_pos_fresh (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (swapRawEdgeRelabeling P cut).mapDart (SurfaceCellComplex.SignedDart.pos (freshEdge P)) = SurfaceCellComplex.SignedDart.neg (freshEdge P)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.swapEdgeRelabeling_neg_fresh (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (swapRawEdgeRelabeling P cut).mapDart (SurfaceCellComplex.SignedDart.neg (freshEdge P)) = SurfaceCellComplex.SignedDart.pos (freshEdge P)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.swapEdgeRelabeling_castSucc (P : FiniteCyclicPresentation) (cut : P.P2Cut) (d : P.Dart) : (swapRawEdgeRelabeling P cut).mapDart (P1.castSuccDart d) = P1.castSuccDart d

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.map_swapEdgeRelabeling_retainWord (P : FiniteCyclicPresentation) (cut : P.P2Cut) (word : List P.Dart) : List.map (swapRawEdgeRelabeling P cut).mapDart (retainWord word) = retainWord word

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.map_swap_selectedBoundary (P : FiniteCyclicPresentation) (cut : P.P2Cut) : List.map (swapRawEdgeRelabeling P cut).mapDart (selectedBoundary P cut.swap) ~r rightBoundary P cut

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.map_swap_rightBoundary (P : FiniteCyclicPresentation) (cut : P.P2Cut) : List.map (swapRawEdgeRelabeling P cut).mapDart (rightBoundary P cut.swap) ~r selectedBoundary P cut

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.map_boundary_swap_old_selected (P : FiniteCyclicPresentation) (cut : P.P2Cut) : List.map (swapEdgeRelabeling P cut).mapDart ((split P cut.swap).boundary (oldFace P cut.swap cut.face.face)) ~r (split P cut).boundary (rightFace P cut)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.map_boundary_swap_right (P : FiniteCyclicPresentation) (cut : P.P2Cut) : List.map (swapEdgeRelabeling P cut).mapDart ((split P cut.swap).boundary (rightFace P cut.swap)) ~r (split P cut).boundary (oldFace P cut cut.face.face)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.map_boundary_swap_old_of_ne (P : FiniteCyclicPresentation) (cut : P.P2Cut) {f : P.Face} (hface : f ≠ cut.face.face) : List.map (swapEdgeRelabeling P cut).mapDart ((split P cut.swap).boundary (oldFace P cut.swap f)) = (split P cut).boundary (oldFace P cut f)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.swapSignedPresentationIso (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (split P cut.swap).SignedPresentationIso (split P cut)

Swapping the two displayed P2 pieces changes only child order and fresh-edge orientation.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.flipEdgeRelabeling (P : FiniteCyclicPresentation) (cut : P.P2Cut) : EdgeRelabeling (split P cut.flip).Edge (split P cut).Edge

Identity edge relabeling between the definitionally equal edge types of the two reversed-cut splits. Naming the transport keeps the signed-isomorphism boundary proof transparent.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.flipEdgeRelabeling_mapDart (P : FiniteCyclicPresentation) (cut : P.P2Cut) (d : (split P cut.flip).Dart) : (flipEdgeRelabeling P cut).mapDart d = d

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.map_flipEdgeRelabeling (P : FiniteCyclicPresentation) (cut : P.P2Cut) (word : List (split P cut.flip).Dart) : List.map (flipEdgeRelabeling P cut).mapDart word = word

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.map_boundary_flip_old_selected (P : FiniteCyclicPresentation) (cut : P.P2Cut) : List.map (flipEdgeRelabeling P cut).mapDart ((split P cut.flip).boundary (oldFace P cut.flip cut.face.face)) = (split P cut).boundary (rightFace P cut)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.map_boundary_flip_right (P : FiniteCyclicPresentation) (cut : P.P2Cut) : List.map (flipEdgeRelabeling P cut).mapDart ((split P cut.flip).boundary (rightFace P cut.flip)) = (split P cut).boundary (oldFace P cut cut.face.face)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.map_boundary_flip_old_of_ne (P : FiniteCyclicPresentation) (cut : P.P2Cut) {f : P.Face} (hface : f ≠ cut.face.face) : List.map (flipEdgeRelabeling P cut).mapDart ((split P cut.flip).boundary (oldFace P cut.flip f)) = (split P cut).boundary (oldFace P cut f)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.flipSignedPresentationIso (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (split P cut.flip).SignedPresentationIso (split P cut)

The split presentations obtained from the two orientations of a cut differ only by swapping the two child faces.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.negativePolygonallyEquivalent (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = true) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : P.PolygonallyEquivalent (split P cut) validP ⋯

A negative-orientation nondegenerate cut reduces to the positive theorem after reversing the cut and swapping the two child faces.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.nondegeneratePolygonallyEquivalent (P : FiniteCyclicPresentation) (cut : P.P2Cut) (hl : 0 < cut.left.length) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : P.PolygonallyEquivalent (split P cut) validP ⋯

Every nondegenerate P2 split preserves the faithful polygonal realization, independently of the chosen traversal orientation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Subdivision.preservesPolygonalRealization : PreservesPolygonalRealization

Every ordinary P2 subdivision preserves the faithful polygonal realization.

For an ordinary-valid source, the exceptional empty-word-sphere alternative in P2Subdivision is impossible, so the public move relation supplies exactly the two positivity hypotheses required by the local two-disk gluing model.