Combinatorial selections for finite-cyclic reduction

This file supplies the finite graph and cyclic-list selections used by the recursive Gallier--Xu normalization. In particular, connected presentations with more than one face expose a genuinely adjacent pair, and either occurrence of their common edge can be placed at the head of a suitably oriented cyclic boundary.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.unorientedIsoOfOrientedBoundaries {P Q : FiniteCyclicPresentation} (edgeRelabeling : EdgeRelabeling P.Edge Q.Edge) (faceEquiv : P.Face ≃ Q.Face) (reverseFace : P.Face → Bool) (boundary_rotated : ∀ (f : P.Face), List.map edgeRelabeling.mapDart (P.orientedBoundary { face := f, orientation := reverseFace f }) ~r Q.boundary (faceEquiv f)) : P.UnorientedPresentationIso Q

Build an unoriented presentation isomorphism from equations stated using oriented source faces and stored target faces. Reversing both sides converts this convenient input convention to the target-oriented convention of UnorientedPresentationIso.

Equations

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

Deleting a selected edge name

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.edgeCountAfterDelete (P : FiniteCyclicPresentation) : ℕ

The edge count after deleting one selected edge.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.edgeCountAfterDelete P = P.edgeCount - 1

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.edgeCountAfterDelete_add_one (P : FiniteCyclicPresentation) (e : P.Edge) : edgeCountAfterDelete P + 1 = P.edgeCount

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.edgeToLast (P : FiniteCyclicPresentation) (e : P.Edge) : P.Edge ≃ Fin (edgeCountAfterDelete P + 1)

Rename an arbitrary selected edge to the last position of the one-larger edge type.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.edgeToLast_selected (P : FiniteCyclicPresentation) (e : P.Edge) : (edgeToLast P e) e = P1.freshEdge (edgeCountAfterDelete P)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.renamedTail (P : FiniteCyclicPresentation) (e : P.Edge) (word : List P.Dart) : List (SurfaceCellComplex.SignedDart (Fin (edgeCountAfterDelete P + 1)))

Rename a word after moving the selected edge to the fresh-last index.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.lowerTail (P : FiniteCyclicPresentation) (e : P.Edge) (word : List P.Dart) : List (SurfaceCellComplex.SignedDart (Fin (edgeCountAfterDelete P)))

Contract the now-unused last edge name from a renamed word.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.freshEdge_not_mem_renamedTail (P : FiniteCyclicPresentation) (e : P.Edge) (word : List P.Dart) (he : e ∉ List.map edgeOfDart word) : P1.freshEdge (edgeCountAfterDelete P) ∉ List.map edgeOfDart (renamedTail P e word)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.retainWord_lowerTail (P : FiniteCyclicPresentation) (e : P.Edge) (word : List P.Dart) (he : e ∉ List.map edgeOfDart word) : P2.retainWord (lowerTail P e word) = renamedTail P e word

Lowering and re-embedding a renamed word which avoids the selected edge recovers that exact renamed word.

Moving a selected face pair to the endpoints

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.lastFace (P : FiniteCyclicPresentation) (f : P.Face) : P.Face

The last face index, using an existing face to certify nonemptiness.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.lastFace P f = ⟨P.faces.length - 1, ⋯⟩

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.faceToEndpoints (P : FiniteCyclicPresentation) (f g : P.Face) : P.Face ≃ P.Face

Move f to index zero and a distinct g to the final index.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.faceToEndpoints_selected (P : FiniteCyclicPresentation) (f g : P.Face) (hfg : f ≠ g) : (faceToEndpoints P f g) f = ⟨0, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.faceToEndpoints_right (P : FiniteCyclicPresentation) (f g : P.Face) : (faceToEndpoints P f g) g = lastFace P f

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.faceCountBetween (P : FiniteCyclicPresentation) : ℕ

Number of untouched faces after selecting two distinct endpoints.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.faceCountBetween P = P.faces.length - 2

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.middleFacePosition (P : FiniteCyclicPresentation) (f g : P.Face) (hfg : f ≠ g) (i : Fin (faceCountBetween P)) : P.Face

The ith interior position between zero and the final face index.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.middleFacePosition P f g hfg i = ⟨↑i + 1, ⋯⟩

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.middleOriginalFace (P : FiniteCyclicPresentation) (f g : P.Face) (hfg : f ≠ g) (i : Fin (faceCountBetween P)) : P.Face

The original face occupying an interior position after moving the selected pair to the endpoints.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.middleOriginalFaces (P : FiniteCyclicPresentation) (f g : P.Face) (hfg : f ≠ g) : List P.Face

Enumerate the original faces not selected as endpoints, in their transported order.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.middleOriginalFace_ne_selected (P : FiniteCyclicPresentation) (f g : P.Face) (hfg : f ≠ g) (i : Fin (faceCountBetween P)) : middleOriginalFace P f g hfg i ≠ f

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.middleOriginalFace_ne_right (P : FiniteCyclicPresentation) (f g : P.Face) (hfg : f ≠ g) (i : Fin (faceCountBetween P)) : middleOriginalFace P f g hfg i ≠ g

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.middleOriginalFaces_length (P : FiniteCyclicPresentation) (f g : P.Face) (hfg : f ≠ g) : (middleOriginalFaces P f g hfg).length = faceCountBetween P

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.face_eq_selected_or_right_or_middle (P : FiniteCyclicPresentation) (f g q : P.Face) (hfg : f ≠ g) : q = f ∨ q = g ∨ ∃ (i : Fin (faceCountBetween P)), q = middleOriginalFace P f g hfg i

Every face is the selected face, the right face, or a uniquely positioned untouched face.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.exists_ne_step_of_reflTransGen {α : Type u_1} {r : α → α → Prop} {a b : α} (h : Relation.ReflTransGen r a b) (hne : a ≠ b) : ∃ (x : α) (y : α), r x y ∧ x ≠ y

A nontrivial reflexive-transitive path contains a genuinely non-reflexive step.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.faceAdjacent_comm (P : FiniteCyclicPresentation) (f g : P.Face) : P.FaceAdjacent f g ↔ P.FaceAdjacent g f

Face adjacency is symmetric.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.add_faceEdgeMultiplicity_le_edgeMultiplicity (P : FiniteCyclicPresentation) (f g : P.Face) (e : P.Edge) (hfg : f ≠ g) : P.faceEdgeMultiplicity f e + P.faceEdgeMultiplicity g e ≤ P.edgeMultiplicity e

The contributions of two distinct faces are bounded by the total edge multiplicity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.add_three_faceEdgeMultiplicity_le_edgeMultiplicity (P : FiniteCyclicPresentation) (f g q : P.Face) (e : P.Edge) (hfg : f ≠ g) (hfq : f ≠ q) (hgq : g ≠ q) : P.faceEdgeMultiplicity f e + P.faceEdgeMultiplicity g e + P.faceEdgeMultiplicity q e ≤ P.edgeMultiplicity e

Three distinct face contributions are bounded by total edge multiplicity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.edge_not_mem_boundary_of_other (P : FiniteCyclicPresentation) (valid : P.IsSurfaceValid) (f g q : P.Face) (e : P.Edge) (hfg : f ≠ g) (hfq : f ≠ q) (hgq : g ≠ q) (hef : e ∈ List.map edgeOfDart (P.boundary f)) (heg : e ∈ List.map edgeOfDart (P.boundary g)) : e ∉ List.map edgeOfDart (P.boundary q)

Once two distinct faces contain an edge of surface multiplicity at most two, no third face contains that edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.exists_distinct_faceAdjacent (P : FiniteCyclicPresentation) (connected : P.IsConnected) (hmany : 1 < P.faces.length) : ∃ (f : P.Face) (g : P.Face), f ≠ g ∧ P.FaceAdjacent f g

A connected presentation with at least two faces contains two distinct adjacent faces.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.exists_tail_isRotated_cons_of_mem {α : Type u_1} {a : α} {word : List α} (ha : a ∈ word) : ∃ (tail : List α), word ~r a :: tail

Any member of a linear list can be moved to its head by a cyclic rotation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.exists_dart_of_mem_map_edgeOfDart {α : Type u_1} {e : α} {word : List (SurfaceCellComplex.SignedDart α)} (he : e ∈ List.map edgeOfDart word) : ∃ d ∈ word, edgeOfDart d = e

Recover a signed occurrence from membership in the projected unoriented edge word.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.PositiveOccurrence (P : FiniteCyclicPresentation) (f : P.Face) (e : P.Edge) : Type

A common edge displayed positively at the head of an oriented cyclic face boundary.

• orientedFace : P.OrientedFace

  The orientedFace declaration.

• face_eq : self.orientedFace.face = f
• tail : List P.Dart

  The tail declaration.

• boundary_rotated : P.orientedBoundary self.orientedFace ~r SurfaceCellComplex.SignedDart.pos e :: self.tail

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.NegativeOccurrence (P : FiniteCyclicPresentation) (f : P.Face) (e : P.Edge) : Type

A common edge displayed negatively at the head of an oriented cyclic face boundary.

• orientedFace : P.OrientedFace

  The orientedFace declaration.

• face_eq : self.orientedFace.face = f
• tail : List P.Dart

  The tail declaration.

• boundary_rotated : P.orientedBoundary self.orientedFace ~r SurfaceCellComplex.SignedDart.neg e :: self.tail

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.exists_positiveOccurrence (P : FiniteCyclicPresentation) (f : P.Face) (e : P.Edge) (he : e ∈ List.map edgeOfDart (P.boundary f)) : Nonempty (PositiveOccurrence P f e)

Choose the traversal orientation which displays a selected edge occurrence positively.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.PositiveOccurrence.flip {P : FiniteCyclicPresentation} {f : P.Face} {e : P.Edge} (occurrence : PositiveOccurrence P f e) : NegativeOccurrence P f e

Reverse a positive displayed occurrence to obtain a negative displayed occurrence.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.PositiveOccurrence.edge_mem_boundary {P : FiniteCyclicPresentation} {f : P.Face} {e : P.Edge} (occurrence : PositiveOccurrence P f e) : e ∈ List.map edgeOfDart (P.boundary f)

The underlying stored face contains the positively displayed edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.NegativeOccurrence.edge_mem_boundary {P : FiniteCyclicPresentation} {f : P.Face} {e : P.Edge} (occurrence : NegativeOccurrence P f e) : e ∈ List.map edgeOfDart (P.boundary f)

The underlying stored face contains the negatively displayed edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.PositiveOccurrence.edge_not_mem_tail {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (occurrence : PositiveOccurrence P f e) (valid : P.IsSurfaceValid) (hfg : f ≠ g) (heg : e ∈ List.map edgeOfDart (P.boundary g)) : e ∉ List.map edgeOfDart occurrence.tail

In two distinct incident faces, the displayed occurrence consumes the entire multiplicity contributed by its face, so the same edge does not occur again in its tail.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.NegativeOccurrence.edge_not_mem_tail {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (occurrence : NegativeOccurrence P f e) (valid : P.IsSurfaceValid) (hfg : f ≠ g) (heg : e ∈ List.map edgeOfDart (P.boundary g)) : e ∉ List.map edgeOfDart occurrence.tail

The corresponding no-second-occurrence statement for a negatively displayed face.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.mergeLeftWord {P : FiniteCyclicPresentation} {f : P.Face} {e : P.Edge} (occurrence : PositiveOccurrence P f e) : List (SurfaceCellComplex.SignedDart (Fin (edgeCountAfterDelete P)))

The lowered left word used by the canonical contextual merge.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.mergeRightWord {P : FiniteCyclicPresentation} {g : P.Face} {e : P.Edge} (occurrence : NegativeOccurrence P g e) : List (SurfaceCellComplex.SignedDart (Fin (edgeCountAfterDelete P)))

The lowered right word used by the canonical contextual merge.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.mergeMiddleWords (P : FiniteCyclicPresentation) (e : P.Edge) (f g : P.Face) (hfg : f ≠ g) : List (List (SurfaceCellComplex.SignedDart (Fin (edgeCountAfterDelete P))))

Lower and enumerate all faces not selected for a merge.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.mergeMiddleWords_length (P : FiniteCyclicPresentation) (e : P.Edge) (f g : P.Face) (hfg : f ≠ g) : (mergeMiddleWords P e f g hfg).length = faceCountBetween P

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.mergeMiddleWords_get (P : FiniteCyclicPresentation) (e : P.Edge) (f g : P.Face) (hfg : f ≠ g) (i : Fin (faceCountBetween P)) : (mergeMiddleWords P e f g hfg).get ⟨↑i, ⋯⟩ = lowerTail P e (P.boundary (middleOriginalFace P f g hfg i))

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.faceCountBetween_add_two (P : FiniteCyclicPresentation) (f g : P.Face) (hfg : f ≠ g) : faceCountBetween P + 2 = P.faces.length

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.mergeSource {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (hfg : f ≠ g) : FiniteCyclicPresentation

The canonical contextual P2 source associated to two oppositely displayed adjacent faces.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.mergeTarget {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (hfg : f ≠ g) : FiniteCyclicPresentation

The presentation after merging the selected adjacent faces and deleting their separator.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.mergeSource_faces_length {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (hfg : f ≠ g) : (mergeSource left right hfg).faces.length = P.faces.length

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.mergeTarget_faces_length {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (hfg : f ≠ g) : (mergeTarget left right hfg).faces.length = P.faces.length - 1

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.mergeFaceEquiv {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (hfg : f ≠ g) : P.Face ≃ (mergeSource left right hfg).Face

Reindex the input faces to the selected/interior/right ordering of its contextual merge source.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.mergeFaceEquiv_selected {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (hfg : f ≠ g) : (mergeFaceEquiv left right hfg) f = FaceMerge.ContextMerge.selectedFace (mergeLeftWord left) (mergeRightWord right) (mergeMiddleWords P e f g hfg)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.mergeFaceEquiv_right {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (hfg : f ≠ g) : (mergeFaceEquiv left right hfg) g = FaceMerge.ContextMerge.rightFace (mergeLeftWord left) (mergeRightWord right) (mergeMiddleWords P e f g hfg)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.mergeFaceEquiv_middle {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (hfg : f ≠ g) (i : Fin (faceCountBetween P)) : (mergeFaceEquiv left right hfg) (middleOriginalFace P f g hfg i) = FaceMerge.ContextMerge.untouchedSourceFace (mergeLeftWord left) (mergeRightWord right) (mergeMiddleWords P e f g hfg) ⟨↑i, ⋯⟩

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.mergeReverseFace {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (q : P.Face) : Bool

Reverse precisely the two selected source faces according to the traversals used to expose their separator; untouched faces retain their stored orientation.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.mergeUnorientedIso {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (hfg : f ≠ g) (valid : P.IsSurfaceValid) : P.UnorientedPresentationIso (mergeSource left right hfg)

The arbitrary adjacent pair is the canonical contextual merge source after renaming the separator, reordering faces, and choosing the two displayed traversal orientations.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.mergeSource_isSurfaceValid {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (hfg : f ≠ g) (validP : P.IsSurfaceValid) : (mergeSource left right hfg).IsSurfaceValid

The specialized unoriented comparison used by an adjacent-face merge preserves ordinary validity. Reversing either selected face cannot create a duplicate: both selected faces contain the fresh separator, untouched faces do not, and the two selected occurrences have opposite signs.

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.markedMergeTarget {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (hfg : f ≠ g) : FiniteCyclicPresentation

The validity-safe result of merging an arbitrary adjacent pair while retaining its separator as a cancellable adjacent inverse marker.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.markedMergeTarget_isSurfaceValid {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (hfg : f ≠ g) (validP : P.IsSurfaceValid) : (markedMergeTarget left right hfg).IsSurfaceValid

An arbitrary marked merge preserves strict ordinary validity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.markedMergeTarget_isConnected {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (hfg : f ≠ g) (validP : P.IsSurfaceValid) (connectedP : P.IsConnected) : (markedMergeTarget left right hfg).IsConnected

An arbitrary marked merge preserves face-incidence connectivity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.markedMergeNormalizationEquivalent {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (hfg : f ≠ g) (validP : P.IsSurfaceValid) : NormalizationEquivalent { presentation := P, valid := validP } { presentation := markedMergeTarget left right hfg, valid := ⋯ }

Merge any oppositely displayed adjacent pair without a target-validity side condition. The retained inverse marker is canceled only after the face recursion, preventing intermediate cyclic duplicate faces.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.markedMergeTarget_faces_length {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (hfg : f ≠ g) : (markedMergeTarget left right hfg).faces.length = P.faces.length - 1

A marked merge removes exactly one face.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.markedMergePolygonallyEquivalent {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (hfg : f ≠ g) (validP : P.IsSurfaceValid) : P.PolygonallyEquivalent (markedMergeTarget left right hfg) validP ⋯

Faithful polygonal-realization invariance of the arbitrary marked merge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.mergeNormalizationEquivalent {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (hfg : f ≠ g) (validP : P.IsSurfaceValid) (validTarget : (mergeTarget left right hfg).IsSurfaceValid) : NormalizationEquivalent { presentation := P, valid := validP } { presentation := mergeTarget left right hfg, valid := validTarget }

Merge an arbitrary oppositely displayed adjacent pair. Target validity remains explicit: under the project's strict stored-word uniqueness clause, a merge can make its new word coincide cyclically with an untouched face.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.mergePolygonallyEquivalent {P : FiniteCyclicPresentation} {f g : P.Face} {e : P.Edge} (left : PositiveOccurrence P f e) (right : NegativeOccurrence P g e) (hfg : f ≠ g) (validP : P.IsSurfaceValid) (validTarget : (mergeTarget left right hfg).IsSurfaceValid) : P.PolygonallyEquivalent (mergeTarget left right hfg) validP validTarget

Faithful polygonal-realization invariance of the arbitrary adjacent-face merge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.exists_negativeOccurrence (P : FiniteCyclicPresentation) (f : P.Face) (e : P.Edge) (he : e ∈ List.map edgeOfDart (P.boundary f)) : Nonempty (NegativeOccurrence P f e)

Choose the traversal orientation which displays a selected edge occurrence negatively.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.exists_oppositelyDisplayedAdjacentFaces (P : FiniteCyclicPresentation) (connected : P.IsConnected) (hmany : 1 < P.faces.length) : ∃ (f : P.Face) (g : P.Face) (e : P.Edge), f ≠ g ∧ Nonempty (PositiveOccurrence P f e) ∧ Nonempty (NegativeOccurrence P g e)

A distinct adjacent pair can always be oriented with positive and negative occurrences of the same separator displayed at the heads of its two cyclic boundaries.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.OneFaceReduction (P : ValidPresentation) : Type

The validity-safe output of merging a connected presentation down to one face.

• target : ValidPresentation

  The target declaration.

• connected : self.target.presentation.IsConnected
• faces_length : self.target.presentation.faces.length = 1
• equivalent : NormalizationEquivalent P self.target

@[irreducible]

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Reduction.reduceToOneFace (P : ValidPresentation) (connectedP : P.presentation.IsConnected) : OneFaceReduction P

Repeated marked merges reduce every connected ordinary-valid presentation to one face.

Each merge retains its separator as an adjacent inverse marker. Consequently every recursive target remains strictly valid even when deleting the separator immediately would duplicate an untouched cyclic face word.

Equations

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