Polygonal realization of one-sided-degenerate Gallier--Xu P2

This file lifts the local monogon--polygon disk theorem to finite cyclic presentations. The positive base case has an empty left cut word and a nonempty right cut word. Reversal and child swap transport that case to every ordinary-valid one-sided-degenerate cut.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.leftLength_eq_zero {P : FiniteCyclicPresentation} {cut : P.P2Cut} (hleft : cut.left = []) : cut.left.length = 0

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateCutSideIndex (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (_hleft : cut.left = []) (hr : 0 < cut.right.length) (i : Fin (P.boundary cut.face.face).length) : Fin cut.right.length

The rotated source side index, specialized to an empty-left cut.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateCutSideIndex_val (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (i : Fin (P.boundary cut.face.face).length) : ↑(rightDegenerateCutSideIndex P cut horientation hleft hr i) = (↑i + positiveCutRotation P cut horientation) % cut.right.length

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.sourceBoundaryLength_eq_rightLength (P : FiniteCyclicPresentation) (cut : P.P2Cut) (hleft : cut.left = []) : (P.boundary cut.face.face).length = cut.right.length

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateCutSideIndex_injective (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) : Function.Injective (rightDegenerateCutSideIndex P cut horientation hleft hr)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateCutSideIndex_surjective (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) : Function.Surjective (rightDegenerateCutSideIndex P cut horientation hleft hr)

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.zeroLeftCellHomeomorph {l : ℕ} (hl : l = 0) : PolygonCell 1 ≃ₜ PolygonCell (l + 1)

Phantom transport from the literal monogon to a selected child whose old-side count is propositionally zero.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.zeroLeftCellHomeomorph hl = LeanEval.Topology.ClassificationOfSurfaces.PolygonCell.rotateHomeomorph ⋯ 0

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.zeroLeftCellHomeomorph_side {l : ℕ} (hl : l = 0) (t : ↑unitInterval) : (zeroLeftCellHomeomorph hl) ((PolygonCell.side 0) t) = (PolygonCell.side (Fin.last l)) t

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.zeroLeftChildPairHomeomorph {l r : ℕ} (hl : l = 0) : DiskSquare.ChildPair 0 r ≃ₜ DiskSquare.ChildPair l r

The zeroLeftChildPairHomeomorph declaration.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.zeroLeftChildPair_generator_map {l r : ℕ} (hl : l = 0) {x y : DiskSquare.ChildPair 0 r} (hxy : DiskSquare.ParamChildSeamGenerator 0 r x y) : DiskSquare.ParamChildSeamGenerator l r ((zeroLeftChildPairHomeomorph hl) x) ((zeroLeftChildPairHomeomorph hl) y)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.zeroLeftCellHomeomorph_symm_side {l : ℕ} (hl : l = 0) (t : ↑unitInterval) : (zeroLeftCellHomeomorph hl).symm ((PolygonCell.side (Fin.last l)) t) = (PolygonCell.side 0) t

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.zeroLeftChildPair_generator_comap {l r : ℕ} (hl : l = 0) {x y : DiskSquare.ChildPair l r} (hxy : DiskSquare.ParamChildSeamGenerator l r x y) : DiskSquare.ParamChildSeamGenerator 0 r ((zeroLeftChildPairHomeomorph hl).symm x) ((zeroLeftChildPairHomeomorph hl).symm y)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.zeroLeftChildPair_eqvGen_iff {l r : ℕ} (hl : l = 0) (x y : DiskSquare.ChildPair 0 r) : Relation.EqvGen (DiskSquare.ParamChildSeamGenerator 0 r) x y ↔ Relation.EqvGen (DiskSquare.ParamChildSeamGenerator l r) ((zeroLeftChildPairHomeomorph hl) x) ((zeroLeftChildPairHomeomorph hl) y)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.zeroLeftChildGluingHomeomorph {l r : ℕ} (hl : l = 0) : DiskSquare.ParamChildGluing 0 r ≃ₜ DiskSquare.ParamChildGluing l r

The zeroLeftChildGluingHomeomorph declaration.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.zeroLeftChildGluingHomeomorph_mk_inr {l r : ℕ} (hl : l = 0) (z : PolygonCell (r + 1)) : (zeroLeftChildGluingHomeomorph hl) (Quotient.mk'' (Sum.inr z)) = Quotient.mk'' (Sum.inr z)

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

The selected source cell, cyclically aligned and then cut by the local degenerate disk homeomorphism.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateSelectedCellHomeomorph_side (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (i : Fin (P.boundary cut.face.face).length) (t : ↑unitInterval) : (rightDegenerateSelectedCellHomeomorph P cut horientation hleft hr) ((PolygonCell.side i) t) = Quotient.mk'' (Sum.inr ((PolygonCell.side ((rightDegenerateCutSideIndex P cut horientation hleft hr i).addNat 1)) t))

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

Cut the selected source face and include its local child quotient 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_rightDegenerateSelectedFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : Continuous (rightDegenerateSelectedFaceMap P cut horientation hleft hr validP)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateSelectedFaceMap_side (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (i : Fin (P.boundary cut.face.face).length) (t : ↑unitInterval) : rightDegenerateSelectedFaceMap P cut horientation hleft hr validP ((PolygonCell.side i) t) = (split P cut).polygonalMk ⋯ ⟨rightFace P cut, (PolygonCell.side (positiveRightChildSideIndex P cut horientation ((rightDegenerateCutSideIndex P cut horientation hleft hr i).addNat 1))) t⟩

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

Facewise forward map for an empty-left positive cut.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_rightDegenerateFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (f : P.Face) : Continuous (rightDegenerateFaceMap P cut horientation hleft hr validP f)

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

The rightDegeneratePreMap declaration.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_rightDegeneratePreMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : Continuous (rightDegeneratePreMap P cut horientation hleft hr validP)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegeneratePreMap_selected (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (z : PolygonCell (P.boundary cut.face.face).length) : rightDegeneratePreMap P cut horientation hleft hr validP ⟨cut.face.face, z⟩ = rightDegenerateSelectedFaceMap P cut horientation hleft hr validP z

@[simp]

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegeneratePreMap_selected_side (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (i : Fin (P.boundary cut.face.face).length) (t : ↑unitInterval) : rightDegeneratePreMap P cut horientation hleft hr validP ⟨cut.face.face, (PolygonCell.side i) t⟩ = (split P cut).polygonalMk ⋯ ⟨rightFace P cut, (PolygonCell.side (positiveRightChildSideIndex P cut horientation ((rightDegenerateCutSideIndex P cut horientation hleft hr i).addNat 1))) t⟩

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

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

Route every old source occurrence to the target occurrence carrying it after the split.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateMapOccurrence_selected (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (i : Fin (P.boundary cut.face.face).length) : rightDegenerateMapOccurrence P cut horientation hleft hr ⟨cut.face.face, i⟩ = ⟨rightFace P cut, positiveRightChildSideIndex P cut horientation ((rightDegenerateCutSideIndex P cut horientation hleft hr i).addNat 1)⟩

@[simp]

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegeneratePreMap_occurrenceSide (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (o : P.BoundaryOccurrence) (t : ↑unitInterval) : rightDegeneratePreMap P cut horientation hleft hr validP ((P.occurrenceSide o).point t) = (split P cut).polygonalMk ⋯ (((split P cut).occurrenceSide (rightDegenerateMapOccurrence P cut horientation hleft hr o)).point t)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateMapOccurrence_dart (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (o : P.BoundaryOccurrence) : (rightDegenerateMapOccurrence P cut horientation hleft hr o).dart = P1.castSuccDart o.dart

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateMapOccurrence_edge (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (o : P.BoundaryOccurrence) : (rightDegenerateMapOccurrence P cut horientation hleft hr o).edge = Fin.castSucc o.edge

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateMapOccurrence_injective (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) : Function.Injective (rightDegenerateMapOccurrence P cut horientation hleft hr)

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

The rightDegenerateMapPairing declaration.

Equations

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

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

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

Inverse map

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateChildGluingInvMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (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.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_rightDegenerateChildGluingInvMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : Continuous (rightDegenerateChildGluingInvMap P cut horientation hleft hr validP)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateChildGluingInvMap_selectedCell (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (z : PolygonCell (P.boundary cut.face.face).length) : rightDegenerateChildGluingInvMap P cut horientation hleft hr validP ((rightDegenerateSelectedCellHomeomorph P cut horientation hleft hr) z) = P.polygonalMk validP ⟨cut.face.face, z⟩

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateSelectedChildInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (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_rightDegenerateSelectedChildInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : Continuous (rightDegenerateSelectedChildInvFaceMap P cut horientation hleft hr validP)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateRightChildInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (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_rightDegenerateRightChildInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : Continuous (rightDegenerateRightChildInvFaceMap P cut horientation hleft hr validP)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateOldInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (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.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.continuous_rightDegenerateOldInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (f : P.Face) : Continuous (rightDegenerateOldInvFaceMap P cut horientation hleft hr validP f)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateIndexedInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (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 target faceEquiv.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateIndexedInvFaceMap_last (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : rightDegenerateIndexedInvFaceMap P cut horientation hleft hr validP (Fin.last P.faces.length) = rightDegenerateRightChildInvFaceMap P cut horientation hleft hr validP

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateIndexedInvFaceMap_castSucc (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (f : P.Face) : rightDegenerateIndexedInvFaceMap P cut horientation hleft hr validP (Fin.castSucc f) = rightDegenerateOldInvFaceMap P cut horientation hleft hr validP f

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (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_rightDegenerateInvFaceMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (q : (split P cut).Face) : Continuous (rightDegenerateInvFaceMap P cut horientation hleft hr validP q)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateInvFaceMap_oldFace (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (f : P.Face) : rightDegenerateInvFaceMap P cut horientation hleft hr validP (oldFace P cut f) = rightDegenerateOldInvFaceMap P cut horientation hleft hr validP f

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateInvFaceMap_rightFace (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : rightDegenerateInvFaceMap P cut horientation hleft hr validP (rightFace P cut) = rightDegenerateRightChildInvFaceMap P cut horientation hleft hr validP

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateInvPreMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (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_rightDegenerateInvPreMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : Continuous (rightDegenerateInvPreMap P cut horientation hleft hr validP)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateInvPreMap_oldFace (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (f : P.Face) (z : PolygonCell ((split P cut).boundary (oldFace P cut f)).length) : rightDegenerateInvPreMap P cut horientation hleft hr validP ⟨oldFace P cut f, z⟩ = rightDegenerateOldInvFaceMap P cut horientation hleft hr validP f z

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateInvPreMap_rightFace (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (z : PolygonCell ((split P cut).boundary (rightFace P cut)).length) : rightDegenerateInvPreMap P cut horientation hleft hr validP ⟨rightFace P cut, z⟩ = rightDegenerateRightChildInvFaceMap P cut horientation hleft hr validP z

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateOldInvFaceMap_selected (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : rightDegenerateOldInvFaceMap P cut horientation hleft hr validP cut.face.face = rightDegenerateSelectedChildInvFaceMap P cut horientation hleft hr validP

@[simp]

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateSelectedChildInvFaceMap_apply (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (z : PolygonCell (cut.left.length + 1)) : rightDegenerateSelectedChildInvFaceMap P cut horientation hleft hr validP ((positiveSelectedChildCellHomeomorph P cut horientation) z) = rightDegenerateChildGluingInvMap P cut horientation hleft hr validP (Quotient.mk'' (Sum.inl z))

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateRightChildInvFaceMap_apply (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (z : PolygonCell (cut.right.length + 1)) : rightDegenerateRightChildInvFaceMap P cut horientation hleft hr validP ((positiveRightChildCellHomeomorph P cut horientation) z) = rightDegenerateChildGluingInvMap P cut horientation hleft hr validP (Quotient.mk'' (Sum.inr z))

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

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

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

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

The inverse pre-map identifies the fresh target seam.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateInvPreMap_mapOccurrence_side (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (o : P.BoundaryOccurrence) (t : ↑unitInterval) : rightDegenerateInvPreMap P cut horientation hleft hr validP (((split P cut).occurrenceSide (rightDegenerateMapOccurrence P cut horientation hleft 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_rightDegenerateMapOccurrence_eq_of_edge_castSucc (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (q : (split P cut).BoundaryOccurrence) (e : P.Edge) (hedge : q.edge = Fin.castSucc e) : ∃ (o : P.BoundaryOccurrence), rightDegenerateMapOccurrence P cut horientation hleft hr o = q

Every target occurrence on an old edge is the transported copy of a source occurrence. The selected monogon and index zero of the right child are exactly the fresh seam.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.exists_rightDegenerateMapPairing_eq_of_source_edge_castSucc (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (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), rightDegenerateMapPairing P cut horientation hleft hr r = q

A target pairing based at an old edge is exactly the transported source pairing.

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

Occurrence-side form of the exact fresh-seam equality.

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

The inverse pre-map identifies every target gluing generator.

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

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

Descended equivalence

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateRealizationMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (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.rightDegenerateRealizationInvMap (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (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.rightDegenerateRealizationMap_polygonalMk (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (x : P.PolygonalPreRealization) : rightDegenerateRealizationMap P cut horientation hleft hr validP (P.polygonalMk validP x) = rightDegeneratePreMap P cut horientation hleft hr validP x

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateRealizationInvMap_polygonalMk (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (y : (split P cut).PolygonalPreRealization) : rightDegenerateRealizationInvMap P cut horientation hleft hr validP ((split P cut).polygonalMk ⋯ y) = rightDegenerateInvPreMap P cut horientation hleft hr validP y

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateRealizationInvMap_childGluing (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (q : DiskSquare.ParamChildGluing cut.left.length cut.right.length) : rightDegenerateRealizationInvMap P cut horientation hleft hr validP (positiveChildGluingMap P cut horientation validP q) = rightDegenerateChildGluingInvMap P cut horientation hleft hr validP q

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateRealizationMap_childGluingInv (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (q : DiskSquare.ParamChildGluing cut.left.length cut.right.length) : rightDegenerateRealizationMap P cut horientation hleft hr validP (rightDegenerateChildGluingInvMap P cut horientation hleft hr validP q) = positiveChildGluingMap P cut horientation validP q

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightDegenerateRealization_left_inverse_mk (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (x : P.PolygonalPreRealization) : rightDegenerateRealizationInvMap P cut horientation hleft hr validP (rightDegeneratePreMap P cut horientation hleft 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.rightDegenerateRealization_right_inverse_mk (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) (y : (split P cut).PolygonalPreRealization) : rightDegenerateRealizationMap P cut horientation hleft hr validP (rightDegenerateInvPreMap P cut horientation hleft 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.rightDegenerateRealizationEquivData (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (hleft : cut.left = []) (hr : 0 < cut.right.length) (validP : P.IsSurfaceValid) : P.RealizationEquivData (split P cut) validP ⋯

Complete realization-equivalence data for an empty-left positive P2 split.

Equations

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

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

Explicit homeomorphism for an empty-left positive P2 split.

Equations

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

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

Propositional realization invariance for an empty-left positive P2 split.

Transport to every one-sided-degenerate cut

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

A positive cut with an empty right word reduces to the base theorem by swapping its two displayed pieces.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.positiveOneSidedPolygonallyEquivalent (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = false) (honeSided : cut.left = [] ∧ 0 < cut.right.length ∨ 0 < cut.left.length ∧ cut.right = []) (validP : P.IsSurfaceValid) : P.PolygonallyEquivalent (split P cut) validP ⋯

Every positive one-sided-degenerate cut preserves polygonal realization.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.negativeOneSidedPolygonallyEquivalent (P : FiniteCyclicPresentation) (cut : P.P2Cut) (horientation : cut.face.orientation = true) (honeSided : cut.left = [] ∧ 0 < cut.right.length ∨ 0 < cut.left.length ∧ cut.right = []) (validP : P.IsSurfaceValid) : P.PolygonallyEquivalent (split P cut) validP ⋯

A negative one-sided cut reduces to the positive theorem after reversing the cut.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.oneSidedPolygonallyEquivalent (P : FiniteCyclicPresentation) (cut : P.P2Cut) (honeSided : cut.left = [] ∧ 0 < cut.right.length ∨ 0 < cut.left.length ∧ cut.right = []) (validP : P.IsSurfaceValid) : P.PolygonallyEquivalent (split P cut) validP ⋯

Every one-sided-degenerate P2 split preserves the faithful polygonal realization, independently of traversal orientation and of which displayed cut word is empty.