Exact two-face merging for finite cyclic presentations

Two displayed faces separated by a last-index edge are the canonical P2 split of the concatenation of their old boundary words, up to rotating the first child. This supplies the local merge used to reduce a connected presentation to one face. It covers both ordinary nondegenerate cuts and the one-sided monogon case.

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.target {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The one-face presentation obtained after merging the displayed pair.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.target U V = LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.oneFace (U ++ V)

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.source {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

Two displayed faces sharing only the last-index separator in the shown positions.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.targetCut {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) : (target U V).P2Cut

The canonical cut of the concatenated target word between U and V.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.targetCut U V = { face := { face := 0, orientation := false }, left := U, right := V, boundary_rotated := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.targetCut_left {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) : (targetCut U V).left = U

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.targetCut_right {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) : (targetCut U V).right = V

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.sourceSignedIsoSplitTarget {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) : (source U V).SignedPresentationIso (P2.split (target U V) (targetCut U V))

The displayed two-face source differs from the canonical target split only by rotating its first child boundary.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.target_isSurfaceValid {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (hUV : U ++ V ≠ []) (validSource : (source U V).IsSurfaceValid) : (target U V).IsSurfaceValid

Merging preserves ordinary validity whenever the resulting face is nonempty.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.targetCut_isOrdinary {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (hUV : U ++ V ≠ []) : (targetCut U V).IsNondegenerate ∨ (targetCut U V).left = [] ∧ 0 < (targetCut U V).right.length ∨ 0 < (targetCut U V).left.length ∧ (targetCut U V).right = []

The canonical cut is ordinary whenever the concatenated target is nonempty: it is either nondegenerate or exactly one-sided-degenerate.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.normalizationEquivalent {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (hUV : U ++ V ≠ []) (validSource : (source U V).IsSurfaceValid) : NormalizationEquivalent { presentation := source U V, valid := validSource } { presentation := target U V, valid := ⋯ }

Merge the displayed two faces into their concatenated one-face presentation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.polygonallyEquivalent {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (hUV : U ++ V ≠ []) (validSource : (source U V).IsSurfaceValid) : (source U V).PolygonallyEquivalent (target U V) validSource ⋯

Public realization-invariance form of exact two-face merging.

Merging through an arbitrary signed-isomorphic split

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.normalizationEquivalentOfSignedIso {P Q : FiniteCyclicPresentation} (cut : Q.P2Cut) (hcut : cut.IsNondegenerate ∨ cut.left = [] ∧ 0 < cut.right.length ∨ 0 < cut.left.length ∧ cut.right = []) (sourceIso : P.SignedPresentationIso (P2.split Q cut)) (validP : P.IsSurfaceValid) (validQ : Q.IsSurfaceValid) : NormalizationEquivalent { presentation := P, valid := validP } { presentation := Q, valid := validQ }

Any presentation signed-isomorphic to an ordinary canonical P2 split can be merged. This is the stable interface used when the two child faces occur among additional untouched faces: all face ordering and edge naming is confined to sourceIso.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.polygonallyEquivalentOfSignedIso {P Q : FiniteCyclicPresentation} (cut : Q.P2Cut) (hcut : cut.IsNondegenerate ∨ cut.left = [] ∧ 0 < cut.right.length ∨ 0 < cut.left.length ∧ cut.right = []) (sourceIso : P.SignedPresentationIso (P2.split Q cut)) (validP : P.IsSurfaceValid) (validQ : Q.IsSurfaceValid) : P.PolygonallyEquivalent Q validP validQ

Public realization-invariance form of merging through a signed-isomorphic split.

A merge among untouched faces

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.target {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : FiniteCyclicPresentation

Merge U and V into the first face while retaining the remaining face words W.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.target U V W = { edgeCount := n, faces := (U ++ V) :: W }

Marked merging

Deleting the separating edge immediately can make the merged word cyclically equal to an untouched face. The marked merge instead retains that edge as an adjacent inverse pair. Its two occurrences distinguish the merged face from every untouched face, so ordinary validity is preserved. A later contextual cancellation removes the marker after the face-merging recursion has finished.

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.markedTarget {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : FiniteCyclicPresentation

Merge the first and last displayed children while retaining their separator as an adjacent inverse pair in the merged face.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.markedTargetCut {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (markedTarget U V W).P2Cut

Cut the marked merged face immediately after the positive marker occurrence.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.markedTargetCut_isNondegenerate {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (markedTargetCut U V W).IsNondegenerate

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.targetCut {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (target U V W).P2Cut

The canonical cut of the first face of a contextual merge.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.targetCut_left {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (targetCut U V W).left = U

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.targetCut_right {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (targetCut U V W).right = V

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.source {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : FiniteCyclicPresentation

The canonical source for merging in context is the exact P2 split of the target.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.markedMiddleFaceEquiv {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (P1.expand (source U V W) (P1.freshEdge n)).Face ≃ (P2.split (markedTarget U V W) (markedTargetCut U V W)).Face

Match the face positions of the expanded contextual source with the split marked target.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.markedMiddleFaceEquiv U V W = finCongr ⋯

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.markedMiddleFaceEquiv_apply_val {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (f : (P1.expand (source U V W) (P1.freshEdge n)).Face) : ↑((markedMiddleFaceEquiv U V W) f) = ↑f

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.markedMiddleFaceEquiv_oldFace {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (f : (target U V W).Face) : (markedMiddleFaceEquiv U V W) ((P1.faceEquiv (source U V W) (P1.freshEdge n)) (P2.oldFace (target U V W) (targetCut U V W) f)) = P2.oldFace (markedTarget U V W) (markedTargetCut U V W) ⟨↑f, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.markedMiddleFaceEquiv_rightFace {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (markedMiddleFaceEquiv U V W) ((P1.faceEquiv (source U V W) (P1.freshEdge n)) (P2.rightFace (target U V W) (targetCut U V W))) = P2.rightFace (markedTarget U V W) (markedTargetCut U V W)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.selectedFace {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (source U V W).Face

The child occupying the selected old-face position.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.rightFace {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (source U V W).Face

The child appended by the P2 split.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.untouchedTargetFace {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (i : Fin W.length) : (target U V W).Face

The target face occupied by the ith untouched word.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.untouchedTargetFace U V W i = ⟨↑i + 1, ⋯⟩

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.untouchedSourceFace {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (i : Fin W.length) : (source U V W).Face

The source face occupied by the ith untouched word.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.source_boundary_selected {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (source U V W).boundary (selectedFace U V W) = P2.retainWord U ++ [SurfaceCellComplex.SignedDart.pos (P1.freshEdge n)]

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.source_boundary_right {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (source U V W).boundary (rightFace U V W) = [SurfaceCellComplex.SignedDart.neg (P1.freshEdge n)] ++ P2.retainWord V

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.target_boundary_untouched {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (i : Fin W.length) : (target U V W).boundary (untouchedTargetFace U V W i) = W.get i

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.source_boundary_untouched {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (i : Fin W.length) : (source U V W).boundary (untouchedSourceFace U V W i) = P2.retainWord (W.get i)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.expandSourceSignedIsoSplitMarkedTarget {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (P1.expand (source U V W) (P1.freshEdge n)).SignedPresentationIso (P2.split (markedTarget U V W) (markedTargetCut U V W))

P1 expansion of the retained separator in the contextual source is signed-isomorphic to the P2 split of the marked target.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.markedTarget_boundary_zero {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) : (markedTarget U V W).boundary 0 = P2.retainWord U ++ [SurfaceCellComplex.SignedDart.pos (P1.freshEdge n), SurfaceCellComplex.SignedDart.neg (P1.freshEdge n)] ++ P2.retainWord V

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.markedTarget_boundary_succ {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (i : Fin W.length) : (markedTarget U V W).boundary ⟨↑i + 1, ⋯⟩ = P2.retainWord (W.get i)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.markedTarget_boundary_succMap {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (i : Fin (List.map P2.retainWord W).length) : (markedTarget U V W).boundary i.succ = P2.retainWord (W.get ⟨↑i, ⋯⟩)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.markedTarget_isSurfaceValid {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (validSource : (source U V W).IsSurfaceValid) : (markedTarget U V W).IsSurfaceValid

The adjacent inverse marker makes the merged face distinct from every untouched face, so a marked merge preserves the project's strict ordinary validity predicate.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.markedTarget_isConnected {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (connectedSource : (source U V W).IsConnected) : (markedTarget U V W).IsConnected

The validity-safe marked merge preserves face-incidence connectivity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.markedNormalizationEquivalent {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (validSource : (source U V W).IsSurfaceValid) : NormalizationEquivalent { presentation := source U V W, valid := validSource } { presentation := markedTarget U V W, valid := ⋯ }

The validity-safe marked merge is a common P1/P2 subdivision: expand the old separator in the source and cut the marked parent along the fresh second subedge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.markedPolygonallyEquivalent {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (validSource : (source U V W).IsSurfaceValid) : (source U V W).PolygonallyEquivalent (markedTarget U V W) validSource ⋯

Faithful realization invariance of the validity-safe marked merge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.targetCut_isOrdinary {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (hUV : U ++ V ≠ []) : (targetCut U V W).IsNondegenerate ∨ (targetCut U V W).left = [] ∧ 0 < (targetCut U V W).right.length ∨ 0 < (targetCut U V W).left.length ∧ (targetCut U V W).right = []

The contextual cut is ordinary exactly under the same nonempty condition as the two-face special case.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.normalizationEquivalent {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (hUV : U ++ V ≠ []) (validTarget : (target U V W).IsSurfaceValid) : NormalizationEquivalent { presentation := source U V W, valid := ⋯ } { presentation := target U V W, valid := validTarget }

A validity-safe contextual merge. The target-validity hypothesis is explicit because merging can make two cyclic face words coincide, while IsSurfaceValid deliberately excludes duplicate faces.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.ContextMerge.normalizationEquivalentOfSignedIso {P : FiniteCyclicPresentation} {n : ℕ} (U V : List (SurfaceCellComplex.SignedDart (Fin n))) (W : List (List (SurfaceCellComplex.SignedDart (Fin n)))) (hUV : U ++ V ≠ []) (sourceIso : P.SignedPresentationIso (source U V W)) (validP : P.IsSurfaceValid) (validTarget : (target U V W).IsSurfaceValid) : NormalizationEquivalent { presentation := P, valid := validP } { presentation := target U V W, valid := validTarget }

Transport a contextual merge across the face ordering and edge naming of an arbitrary source presentation.

Arbitrary separator names

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.namedSource {n : ℕ} (a : Fin (n + 1)) (U V : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) : FiniteCyclicPresentation

Two displayed faces with an arbitrarily named, oppositely oriented separator.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.namedSourceSignedIso {n : ℕ} (a : Fin (n + 1)) (U V : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (haU : a ∉ List.map edgeOfDart U) (haV : a ∉ List.map edgeOfDart V) : (namedSource a U V).SignedPresentationIso (source (Cancellation.lowerTail a U) (Cancellation.lowerTail a V))

Rename the separator to last and delete that name from both remaining face words.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceMerge.namedNormalizationEquivalent {n : ℕ} (a : Fin (n + 1)) (U V : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (haU : a ∉ List.map edgeOfDart U) (haV : a ∉ List.map edgeOfDart V) (hUV : Cancellation.lowerTail a U ++ Cancellation.lowerTail a V ≠ []) (validSource : (namedSource a U V).IsSurfaceValid) : NormalizationEquivalent { presentation := namedSource a U V, valid := validSource } { presentation := target (Cancellation.lowerTail a U) (Cancellation.lowerTail a V), valid := ⋯ }

Merge two displayed faces with an arbitrary separator name.