Gallier--Xu P2 face subdivision

This file formalizes the second primitive subdivision from Gallier--Xu, Definition 6.3. A cyclic boundary is cut, in a chosen traversal orientation, into two pieces left and right. The presentation-level construction permits empty pieces so that it also expresses Gallier--Xu's exceptional empty-word-sphere conversion. The public P2Subdivision relation requires both pieces to be nonempty for an ordinary face subdivision. The selected face is replaced by two faces whose boundaries in that same orientation are

• left d, and
• d⁻¹ right,

where d is a fresh edge.

The orientation stored on the two target faces is the orientation chosen by the cut. In particular, a negatively oriented cut deliberately stores the inverses of the displayed words; it does not claim to preserve the old positive stored orientation. This convention makes reversing a cut exchange the two children exactly.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Cut (P : FiniteCyclicPresentation) : Type

A cyclic, oriented place at which to apply Gallier--Xu P2.

The decomposition is cyclic rather than tied to the stored head of the list. Empty left or right pieces are allowed.

• face : P.OrientedFace

  The face declaration.

• left : List P.Dart

  The left declaration.

• right : List P.Dart

  The right declaration.

• boundary_rotated : P.orientedBoundary self.face ~r self.left ++ self.right

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Cut.IsNondegenerate {P : FiniteCyclicPresentation} (cut : P.P2Cut) : Prop

A genuine face cut has an old boundary side on each side of the new cutting edge.

The raw P2Cut structure also represents the exceptional empty-word-sphere conversion, for which both pieces are necessarily empty.

Equations

• cut.IsNondegenerate = (cut.left ≠ [] ∧ cut.right ≠ [])

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Cut.isNondegenerate_iff_lengths_pos {P : FiniteCyclicPresentation} (cut : P.P2Cut) : cut.IsNondegenerate ↔ 0 < cut.left.length ∧ 0 < cut.right.length

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Cut.canonical {P : FiniteCyclicPresentation} (face : P.OrientedFace) (position : Fin ((P.orientedBoundary face).length + 1)) : P.P2Cut

Cut a chosen oriented representative at a linear position.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Cut.canonical_face {P : FiniteCyclicPresentation} (face : P.OrientedFace) (position : Fin ((P.orientedBoundary face).length + 1)) : (canonical face position).face = face

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Cut.canonical_zero_left {P : FiniteCyclicPresentation} (face : P.OrientedFace) : (canonical face 0).left = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Cut.canonical_zero_right {P : FiniteCyclicPresentation} (face : P.OrientedFace) : (canonical face 0).right = P.orientedBoundary face

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Cut.canonical_last_left {P : FiniteCyclicPresentation} (face : P.OrientedFace) : (canonical face (Fin.last (P.orientedBoundary face).length)).left = P.orientedBoundary face

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Cut.canonical_last_right {P : FiniteCyclicPresentation} (face : P.OrientedFace) : (canonical face (Fin.last (P.orientedBoundary face).length)).right = []

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Cut.swap {P : FiniteCyclicPresentation} (cut : P.P2Cut) : P.P2Cut

Move the cyclic cut point to the other end of the two pieces.

Equations

• cut.swap = { face := cut.face, left := cut.right, right := cut.left, boundary_rotated := ⋯ }

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Cut.flip {P : FiniteCyclicPresentation} (cut : P.P2Cut) : P.P2Cut

Reverse the traversal orientation of a cut.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Cut.swap_face {P : FiniteCyclicPresentation} (cut : P.P2Cut) : cut.swap.face = cut.face

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Cut.flip_face {P : FiniteCyclicPresentation} (cut : P.P2Cut) : cut.flip.face = cut.face.flip

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Cut.swap_swap {P : FiniteCyclicPresentation} (cut : P.P2Cut) : cut.swap.swap = cut

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Cut.flip_flip {P : FiniteCyclicPresentation} (cut : P.P2Cut) : cut.flip.flip = cut

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Cut.swap_flip {P : FiniteCyclicPresentation} (cut : P.P2Cut) : cut.swap.flip = cut.flip.swap

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Cut.isNondegenerate_swap {P : FiniteCyclicPresentation} (cut : P.P2Cut) : cut.swap.IsNondegenerate ↔ cut.IsNondegenerate

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Cut.isNondegenerate_flip {P : FiniteCyclicPresentation} (cut : P.P2Cut) : cut.flip.IsNondegenerate ↔ cut.IsNondegenerate

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.freshEdge (P : FiniteCyclicPresentation) : Fin (P.edgeCount + 1)

The fresh cutting edge.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.freshEdge P = LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.freshEdge P.edgeCount

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.retainWord {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))

Retain an old boundary word in the enlarged edge type.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.retainWord word = List.map LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.castSuccDart word

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.storedWord {α : Type u_1} (orientation : Bool) (word : List (SurfaceCellComplex.SignedDart α)) : List (SurfaceCellComplex.SignedDart α)

Store a displayed oriented boundary in the presentation's positive orientation.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.retainWord_nil {n : ℕ} : retainWord [] = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.retainWord_append {n : ℕ} (left right : List (SurfaceCellComplex.SignedDart (Fin n))) : retainWord (left ++ right) = retainWord left ++ retainWord right

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.castSuccDart_flip {n : ℕ} (d : SurfaceCellComplex.SignedDart (Fin n)) : P1.castSuccDart d.flip = (P1.castSuccDart d).flip

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.retainWord_inverseWord {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : retainWord (inverseWord word) = inverseWord (retainWord word)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.storedWord_false {α : Type u_1} (word : List (SurfaceCellComplex.SignedDart α)) : storedWord false word = word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.storedWord_true {α : Type u_1} (word : List (SurfaceCellComplex.SignedDart α)) : storedWord true word = inverseWord word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.oriented_storedWord {α : Type u_1} (orientation : Bool) (word : List (SurfaceCellComplex.SignedDart α)) : (if orientation = true then inverseWord (storedWord orientation word) else storedWord orientation word) = word

Reading a stored word in its selected orientation returns the displayed word.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.contractDart_castSuccDart {n : ℕ} (d : SurfaceCellComplex.SignedDart (Fin n)) : P1.contractDart (P1.castSuccDart d) = some d

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.contractWord_retainWord {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : P1.contractWord (retainWord word) = word

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.selectedOrientedBoundary (P : FiniteCyclicPresentation) (cut : P.P2Cut) : List (SurfaceCellComplex.SignedDart (Fin (P.edgeCount + 1)))

The first displayed child boundary.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightOrientedBoundary (P : FiniteCyclicPresentation) (cut : P.P2Cut) : List (SurfaceCellComplex.SignedDart (Fin (P.edgeCount + 1)))

The second displayed child boundary.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.selectedBoundary (P : FiniteCyclicPresentation) (cut : P.P2Cut) : List (SurfaceCellComplex.SignedDart (Fin (P.edgeCount + 1)))

The first child boundary in its stored orientation.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightBoundary (P : FiniteCyclicPresentation) (cut : P.P2Cut) : List (SurfaceCellComplex.SignedDart (Fin (P.edgeCount + 1)))

The second child boundary in its stored orientation.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.faceWord (P : FiniteCyclicPresentation) (cut : P.P2Cut) : Fin (P.faces.length + 1) → List (SurfaceCellComplex.SignedDart (Fin (P.edgeCount + 1)))

The word stored at a target face index.

Equations

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

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.split (P : FiniteCyclicPresentation) (cut : P.P2Cut) : FiniteCyclicPresentation

Canonical presentation-level P2 face split.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.split_edgeCount (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (split P cut).edgeCount = P.edgeCount + 1

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.split_faces_length (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (split P cut).faces.length = P.faces.length + 1

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

Identify the explicit target indexing type with the presentation's face type.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.faceEquiv P cut = finCongr ⋯

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.oldFace (P : FiniteCyclicPresentation) (cut : P.P2Cut) (f : P.Face) : (split P cut).Face

The target face occupying an old source-face position.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.oldFace P cut f = (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.faceEquiv P cut) (Fin.castSucc f)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightFace (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (split P cut).Face

The fresh second child face.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.faceEquiv_apply_val (P : FiniteCyclicPresentation) (cut : P.P2Cut) (f : Fin (P.faces.length + 1)) : ↑((faceEquiv P cut) f) = ↑f

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.face_cases (P : FiniteCyclicPresentation) (cut : P.P2Cut) (q : (split P cut).Face) : (∃ (f : P.Face), q = oldFace P cut f) ∨ q = rightFace P cut

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.split_boundary_index (P : FiniteCyclicPresentation) (cut : P.P2Cut) (q : Fin (P.faces.length + 1)) : (split P cut).boundary ((faceEquiv P cut) q) = faceWord P cut q

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.split_boundary_old (P : FiniteCyclicPresentation) (cut : P.P2Cut) (f : P.Face) : (split P cut).boundary (oldFace P cut f) = if f = cut.face.face then selectedBoundary P cut else retainWord (P.boundary f)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.split_boundary_selected (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (split P cut).boundary (oldFace P cut cut.face.face) = selectedBoundary P cut

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.split_boundary_old_of_ne (P : FiniteCyclicPresentation) (cut : P.P2Cut) {f : P.Face} (h : f ≠ cut.face.face) : (split P cut).boundary (oldFace P cut f) = retainWord (P.boundary f)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.split_boundary_right (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (split P cut).boundary (rightFace P cut) = rightBoundary P cut

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.split_orientedBoundary_selected (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (split P cut).orientedBoundary { face := oldFace P cut cut.face.face, orientation := cut.face.orientation } = selectedOrientedBoundary P cut

The selected child has exactly the displayed oriented boundary left d.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.split_orientedBoundary_right (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (split P cut).orientedBoundary { face := rightFace P cut, orientation := cut.face.orientation } = rightOrientedBoundary P cut

The right child has exactly the displayed oriented boundary d⁻¹ right.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.retainWord_eq_nil_iff {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : retainWord word = [] ↔ word = []

Retaining a word preserves whether it is empty.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.count_retainWord_castSucc {n : ℕ} (e : Fin n) (word : List (SurfaceCellComplex.SignedDart (Fin n))) : List.count e.castSucc (List.map edgeOfDart (retainWord word)) = List.count e (List.map edgeOfDart word)

Retaining a word preserves the multiplicity of every old edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.count_storedWord (orientation : Bool) {α : Type u_1} [DecidableEq α] (word : List (SurfaceCellComplex.SignedDart α)) (e : α) : List.count e (List.map edgeOfDart (storedWord orientation word)) = List.count e (List.map edgeOfDart word)

Reversing the stored traversal does not change unoriented edge multiplicities.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.freshEdge_not_mem_retainWord (P : FiniteCyclicPresentation) (word : List P.Dart) : freshEdge P ∉ List.map edgeOfDart (retainWord word)

The fresh edge does not occur in a retained old word.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.pos_freshEdge_not_mem_retainWord (P : FiniteCyclicPresentation) (word : List P.Dart) : SurfaceCellComplex.SignedDart.pos (freshEdge P) ∉ retainWord word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.neg_freshEdge_not_mem_retainWord (P : FiniteCyclicPresentation) (word : List P.Dart) : SurfaceCellComplex.SignedDart.neg (freshEdge P) ∉ retainWord word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.pos_freshEdge_not_mem_inverse_retainWord (P : FiniteCyclicPresentation) (word : List P.Dart) : SurfaceCellComplex.SignedDart.pos (freshEdge P) ∉ inverseWord (retainWord word)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.neg_freshEdge_not_mem_inverse_retainWord (P : FiniteCyclicPresentation) (word : List P.Dart) : SurfaceCellComplex.SignedDart.neg (freshEdge P) ∉ inverseWord (retainWord word)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.selectedFreshDart (P : FiniteCyclicPresentation) (cut : P.P2Cut) : SurfaceCellComplex.SignedDart (Fin (P.edgeCount + 1))

The signed fresh dart occurring in the selected child.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightFreshDart (P : FiniteCyclicPresentation) (cut : P.P2Cut) : SurfaceCellComplex.SignedDart (Fin (P.edgeCount + 1))

The opposite signed fresh dart occurring in the right child.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightFreshDart P cut = (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.selectedFreshDart P cut).flip

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.edgeOfDart_selectedFreshDart (P : FiniteCyclicPresentation) (cut : P.P2Cut) : edgeOfDart (selectedFreshDart P cut) = freshEdge P

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.edgeOfDart_rightFreshDart (P : FiniteCyclicPresentation) (cut : P.P2Cut) : edgeOfDart (rightFreshDart P cut) = freshEdge P

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.selectedBoundary_of_orientation_false (P : FiniteCyclicPresentation) (cut : P.P2Cut) (h : cut.face.orientation = false) : selectedBoundary P cut = retainWord cut.left ++ [SurfaceCellComplex.SignedDart.pos (freshEdge P)]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.selectedBoundary_of_orientation_true (P : FiniteCyclicPresentation) (cut : P.P2Cut) (h : cut.face.orientation = true) : selectedBoundary P cut = SurfaceCellComplex.SignedDart.neg (freshEdge P) :: inverseWord (retainWord cut.left)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightBoundary_of_orientation_false (P : FiniteCyclicPresentation) (cut : P.P2Cut) (h : cut.face.orientation = false) : rightBoundary P cut = SurfaceCellComplex.SignedDart.neg (freshEdge P) :: retainWord cut.right

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightBoundary_of_orientation_true (P : FiniteCyclicPresentation) (cut : P.P2Cut) (h : cut.face.orientation = true) : rightBoundary P cut = inverseWord (retainWord cut.right) ++ [SurfaceCellComplex.SignedDart.pos (freshEdge P)]

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.selectedBoundary_flip (P : FiniteCyclicPresentation) (cut : P.P2Cut) : selectedBoundary P cut.flip = rightBoundary P cut

Reversing the cut exchanges its selected child with the original right child.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightBoundary_flip (P : FiniteCyclicPresentation) (cut : P.P2Cut) : rightBoundary P cut.flip = selectedBoundary P cut

Reversing the cut exchanges its right child with the original selected child.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.selectedFreshDart_mem_selectedBoundary (P : FiniteCyclicPresentation) (cut : P.P2Cut) : selectedFreshDart P cut ∈ selectedBoundary P cut

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.selectedFreshDart_not_mem_rightBoundary (P : FiniteCyclicPresentation) (cut : P.P2Cut) : selectedFreshDart P cut ∉ rightBoundary P cut

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightFreshDart_mem_rightBoundary (P : FiniteCyclicPresentation) (cut : P.P2Cut) : rightFreshDart P cut ∈ rightBoundary P cut

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightFreshDart_not_mem_selectedBoundary (P : FiniteCyclicPresentation) (cut : P.P2Cut) : rightFreshDart P cut ∉ selectedBoundary P cut

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.selectedFreshDart_not_mem_retainWord (P : FiniteCyclicPresentation) (cut : P.P2Cut) (word : List P.Dart) : selectedFreshDart P cut ∉ retainWord word

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.rightFreshDart_not_mem_retainWord (P : FiniteCyclicPresentation) (cut : P.P2Cut) (word : List P.Dart) : rightFreshDart P cut ∉ retainWord word

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.faceEdgeMultiplicity_split_selected_castSucc (P : FiniteCyclicPresentation) (cut : P.P2Cut) (e : P.Edge) : (split P cut).faceEdgeMultiplicity (oldFace P cut cut.face.face) (Fin.castSucc e) = List.count e (List.map edgeOfDart cut.left)

The selected child receives the old-edge occurrences in the left cut piece.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.faceEdgeMultiplicity_split_right_castSucc (P : FiniteCyclicPresentation) (cut : P.P2Cut) (e : P.Edge) : (split P cut).faceEdgeMultiplicity (rightFace P cut) (Fin.castSucc e) = List.count e (List.map edgeOfDart cut.right)

The right child receives the old-edge occurrences in the right cut piece.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.faceEdgeMultiplicity_split_old_of_ne (P : FiniteCyclicPresentation) (cut : P.P2Cut) {f : P.Face} (h : f ≠ cut.face.face) (e : P.Edge) : (split P cut).faceEdgeMultiplicity (oldFace P cut f) (Fin.castSucc e) = P.faceEdgeMultiplicity f e

Every unselected face retains its old-edge multiplicities.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.faceEdgeMultiplicity_split_selected_freshEdge (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (split P cut).faceEdgeMultiplicity (oldFace P cut cut.face.face) (freshEdge P) = 1

The selected child contains the fresh edge exactly once.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.faceEdgeMultiplicity_split_right_freshEdge (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (split P cut).faceEdgeMultiplicity (rightFace P cut) (freshEdge P) = 1

The right child contains the fresh edge exactly once.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.faceEdgeMultiplicity_split_old_freshEdge_of_ne (P : FiniteCyclicPresentation) (cut : P.P2Cut) {f : P.Face} (h : f ≠ cut.face.face) : (split P cut).faceEdgeMultiplicity (oldFace P cut f) (freshEdge P) = 0

An unselected face contains no occurrence of the fresh edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.faceEdgeMultiplicity_cut_eq_add (P : FiniteCyclicPresentation) (cut : P.P2Cut) (e : P.Edge) : P.faceEdgeMultiplicity cut.face.face e = List.count e (List.map edgeOfDart cut.left) + List.count e (List.map edgeOfDart cut.right)

The selected source face's multiplicity is the sum of the two cut-piece counts.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.edgeMultiplicity_split_castSucc (P : FiniteCyclicPresentation) (cut : P.P2Cut) (e : P.Edge) : P.edgeMultiplicity e = (split P cut).edgeMultiplicity (Fin.castSucc e)

P2 preserves the total multiplicity of every retained old edge.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.edgeMultiplicity_split_freshEdge (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (split P cut).edgeMultiplicity (freshEdge P) = 2

The fresh cutting edge occurs exactly once in each child and nowhere else.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.retainWord_isRotated_iff {n : ℕ} (left right : List (SurfaceCellComplex.SignedDart (Fin n))) : retainWord left ~r retainWord right ↔ left ~r right

Retaining old edge names preserves and reflects cyclic rotation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.split_isSurfaceValid (P : FiniteCyclicPresentation) (cut : P.P2Cut) (h : P.IsSurfaceValid) : (split P cut).IsSurfaceValid

P2 preserves ordinary finite-presentation incidence validity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.edge_mem_orientedBoundary_iff (P : FiniteCyclicPresentation) (face : P.OrientedFace) (e : P.Edge) : e ∈ List.map edgeOfDart (P.orientedBoundary face) ↔ e ∈ List.map edgeOfDart (P.boundary face.face)

Edge membership is independent of the chosen traversal orientation of a face.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.edge_mem_cut_pieces_iff (P : FiniteCyclicPresentation) (cut : P.P2Cut) (e : P.Edge) : e ∈ List.map edgeOfDart cut.left ∨ e ∈ List.map edgeOfDart cut.right ↔ e ∈ List.map edgeOfDart (P.boundary cut.face.face)

An edge of the selected face occurs in one of the two cut pieces.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.castSucc_edge_mem_retainWord {n : ℕ} {e : Fin n} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (h : e ∈ List.map edgeOfDart word) : e.castSucc ∈ List.map edgeOfDart (retainWord word)

Membership of an old edge is retained after enlarging the edge type.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.edge_mem_storedWord_iff {α : Type u_1} (orientation : Bool) (word : List (SurfaceCellComplex.SignedDart α)) (e : α) : e ∈ List.map edgeOfDart (storedWord orientation word) ↔ e ∈ List.map edgeOfDart word

Storing a word in the opposite traversal preserves unoriented edge membership.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.castSucc_edge_mem_selectedBoundary (P : FiniteCyclicPresentation) (cut : P.P2Cut) {e : P.Edge} (h : e ∈ List.map edgeOfDart cut.left) : Fin.castSucc e ∈ List.map edgeOfDart (selectedBoundary P cut)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.castSucc_edge_mem_rightBoundary (P : FiniteCyclicPresentation) (cut : P.P2Cut) {e : P.Edge} (h : e ∈ List.map edgeOfDart cut.right) : Fin.castSucc e ∈ List.map edgeOfDart (rightBoundary P cut)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.split_children_faceAdjacent (P : FiniteCyclicPresentation) (cut : P.P2Cut) : (split P cut).FaceAdjacent (oldFace P cut cut.face.face) (rightFace P cut)

The two child faces are adjacent through the fresh cutting edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.exists_child_edge (P : FiniteCyclicPresentation) (cut : P.P2Cut) (f : P.Face) (e : P.Edge) (h : e ∈ List.map edgeOfDart (P.boundary f)) : ∃ (q : (split P cut).Face), Relation.ReflTransGen (split P cut).FaceAdjacent (oldFace P cut f) q ∧ Fin.castSucc e ∈ List.map edgeOfDart ((split P cut).boundary q)

A source-face edge occurs in a child reachable from the retained face position.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.map_faceAdjacent_chain (P : FiniteCyclicPresentation) (cut : P.P2Cut) {f g : P.Face} (h : P.FaceAdjacent f g) : Relation.ReflTransGen (split P cut).FaceAdjacent (oldFace P cut f) (oldFace P cut g)

A source adjacency lifts to a target path between the retained face positions.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.map_faceChain (P : FiniteCyclicPresentation) (cut : P.P2Cut) {f g : P.Face} (h : Relation.ReflTransGen P.FaceAdjacent f g) : Relation.ReflTransGen (split P cut).FaceAdjacent (oldFace P cut f) (oldFace P cut g)

A source face-adjacency path lifts to a target path.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.split_isConnected (P : FiniteCyclicPresentation) (cut : P.P2Cut) (h : P.IsConnected) : (split P cut).IsConnected

P2 preserves connectivity of the face-edge incidence graph.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.collapseFace (P : FiniteCyclicPresentation) (cut : P.P2Cut) (q : (split P cut).Face) : P.Face

Collapse both child faces of a P2 split back to their source face.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.collapseFace P cut q = if h : ↑q < P.faces.length then ⟨↑q, h⟩ else cut.face.face

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.collapseFace_oldFace (P : FiniteCyclicPresentation) (cut : P.P2Cut) (f : P.Face) : collapseFace P cut (oldFace P cut f) = f

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.collapseFace_rightFace (P : FiniteCyclicPresentation) (cut : P.P2Cut) : collapseFace P cut (rightFace P cut) = cut.face.face

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.collapse_faceAdjacent_chain (P : FiniteCyclicPresentation) (cut : P.P2Cut) {q r : (split P cut).Face} (h : (split P cut).FaceAdjacent q r) : Relation.ReflTransGen P.FaceAdjacent (collapseFace P cut q) (collapseFace P cut r)

Collapsing the child faces sends target adjacency to a source adjacency path.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.collapse_faceChain (P : FiniteCyclicPresentation) (cut : P.P2Cut) {q r : (split P cut).Face} (h : Relation.ReflTransGen (split P cut).FaceAdjacent q r) : Relation.ReflTransGen P.FaceAdjacent (collapseFace P cut q) (collapseFace P cut r)

Collapsing the child faces sends target adjacency paths to source adjacency paths.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.isConnected_of_split (P : FiniteCyclicPresentation) (cut : P.P2Cut) (h : (split P cut).IsConnected) : P.IsConnected

A P2 split is connected only if its source presentation is connected.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.split_isSurfaceValid_of_isEmptyWordSphere (P : FiniteCyclicPresentation) (cut : P.P2Cut) (h : P.IsEmptyWordSphere) : (split P cut).IsSurfaceValid

Every P2 split of an exceptional empty-word presentation is ordinarily valid.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.split_isGallierValid (P : FiniteCyclicPresentation) (cut : P.P2Cut) (h : P.IsGallierValid) : (split P cut).IsGallierValid

P2 preserves Gallier validity, including the exceptional empty-word branch.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.emptyWordSphereCut : emptyWordSphere.P2Cut

The zero-position P2 cut of Gallier--Xu's exceptional sphere presentation.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.emptyWordSphereLastCut : emptyWordSphere.P2Cut

The last-position spelling of the same empty boundary cut.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.emptyWordSphereLastCut_eq : emptyWordSphereLastCut = emptyWordSphereCut

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.split_emptyWordSphere : split emptyWordSphere emptyWordSphereCut = twoMonogonSphere

P2 turns the exceptional empty-word sphere presentation into the two-monogon presentation.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.split_emptyWordSphere_last : split emptyWordSphere emptyWordSphereLastCut = twoMonogonSphere

The endpoint-at-the-right spelling gives the same exact regression.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Subdivision (P Q : FiniteCyclicPresentation) : Prop

A Gallier--Xu P2 face subdivision, up to signed presentation isomorphism of the target.

An ordinary P2 move cuts between two distinct places of a nonempty cyclic boundary, so both old boundary pieces are nonempty. The sole degenerate case admitted here is Gallier--Xu's exceptional empty-word sphere, whose conversion to the ordinary-valid two-monogon presentation is also represented by the raw P2.split construction. This is a syntactic move relation and deliberately does not bundle source validity.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Subdivision.canonical (P : FiniteCyclicPresentation) (cut : P.P2Cut) (hcut : cut.IsNondegenerate) : P.P2Subdivision (P2.split P cut)

A canonical nondegenerate split is a P2 subdivision.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Subdivision.canonicalEmptyWordSphere (P : FiniteCyclicPresentation) (cut : P.P2Cut) (hP : P.IsEmptyWordSphere) : P.P2Subdivision (P2.split P cut)

The raw split of an exceptional empty-word sphere is an allowed exceptional P2 step.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Subdivision.isSurfaceValid {P Q : FiniteCyclicPresentation} (hPQ : P.P2Subdivision Q) (h : P.IsSurfaceValid) : Q.IsSurfaceValid

P2 subdivisions preserve ordinary incidence validity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Subdivision.isConnected {P Q : FiniteCyclicPresentation} (hPQ : P.P2Subdivision Q) (h : P.IsConnected) : Q.IsConnected

P2 subdivisions preserve face-incidence connectivity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Subdivision.isGallierValid {P Q : FiniteCyclicPresentation} (hPQ : P.P2Subdivision Q) (h : P.IsGallierValid) : Q.IsGallierValid

P2 subdivisions preserve Gallier validity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2Subdivision.emptyWordSphere_twoMonogonSphere : emptyWordSphere.P2Subdivision twoMonogonSphere

The exceptional sphere presentation subdivides to the two-monogon sphere presentation.