Finite cyclic surface presentations

This file packages the purely combinatorial data used by polygon-word moves. Edge names and faces are finite by construction, and a face boundary is a cyclic list of signed edge names. Unlike SurfaceCellComplex, this presentation has no arbitrary vertex labels or placeholder realization.

PresentationIso records orientation-preserving changes of names: an equivalence of edge names, an equivalence of faces, and a rotation witness for every renamed face boundary. Allowing an independent orientation reversal for each edge is a separate extension needed before the most general polygon-word moves. EdgeRelabeling records an equivalence of edge names together with an independent orientation reversal for each source edge. SignedPresentationIso combines such a relabeling with an equivalence of faces and a rotation witness for every renamed face boundary. The original orientation-preserving PresentationIso remains available as a compatible special case.

OrientedFace gives each stored face a positive and negative traversal view without mutating the presentation. The negative boundary word is the reversed list with every dart orientation flipped, as required by the oriented polygon conventions used in Gallier--Xu moves.

Gallier--Xu Definition 6.1 has one exceptional cell complex: one face, no edges, and the empty boundary word. The ordinary IsSurfaceValid predicate continues to require nonempty face boundaries. At the end of the file, IsEmptyWordSphere recognizes the exceptional signed isomorphism class and IsGallierValid adds it as an explicit disjunct. The presentation twoMonogonSphere is the nonexceptional two-face model obtained by the book's P2 refinement.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation : Type

A finite list of cyclic signed boundary words with edge names in Fin edgeCount.

• edgeCount : ℕ

  The edgeCount declaration.

• faces : List (List (SurfaceCellComplex.SignedDart (Fin self.edgeCount)))

  The faces declaration.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Edge (P : FiniteCyclicPresentation) : Type

The finite type of unoriented edge names.

Equations

• P.Edge = Fin P.edgeCount

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dart (P : FiniteCyclicPresentation) : Type

Signed occurrences of unoriented edge names.

Equations

• P.Dart = LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart P.Edge

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Face (P : FiniteCyclicPresentation) : Type

Faces are positions in the stored list of boundary words.

Equations

• P.Face = Fin P.faces.length

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.boundary (P : FiniteCyclicPresentation) (f : P.Face) : List P.Dart

The stored cyclic boundary word of a face.

Equations

• P.boundary f = P.faces.get f

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.edgeOfDart {α : Type u_1} : SurfaceCellComplex.SignedDart α → α

Forget the orientation of a signed edge occurrence.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.edgeOfDart (LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.pos e) = e
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.edgeOfDart (LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.neg e) = e

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.edgeOfDart_flip {α : Type u_1} (d : SurfaceCellComplex.SignedDart α) : edgeOfDart d.flip = edgeOfDart d

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.inverseWord {α : Type u_1} (word : List (SurfaceCellComplex.SignedDart α)) : List (SurfaceCellComplex.SignedDart α)

Reverse the traversal direction of a signed boundary word.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.inverseWord word = List.map LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.flip word.reverse

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.inverseWord_nil {α : Type u_1} : inverseWord [] = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.inverseWord_length {α : Type u_1} (word : List (SurfaceCellComplex.SignedDart α)) : (inverseWord word).length = word.length

@[simp]

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.inverseWord_involutive {α : Type u_1} : Function.Involutive inverseWord

Reversing signed words is an involution.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.inverseWord_append {α : Type u_1} (left right : List (SurfaceCellComplex.SignedDart α)) : inverseWord (left ++ right) = inverseWord right ++ inverseWord left

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.inverseWord_isRotated {α : Type u_1} {left right : List (SurfaceCellComplex.SignedDart α)} (h : left ~r right) : inverseWord left ~r inverseWord right

Reversing traversal direction preserves cyclic equivalence.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.inverseWord_isRotated_iff {α : Type u_1} (left right : List (SurfaceCellComplex.SignedDart α)) : inverseWord left ~r inverseWord right ↔ left ~r right

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.map_edgeOfDart_inverseWord {α : Type u_1} (word : List (SurfaceCellComplex.SignedDart α)) : List.map edgeOfDart (inverseWord word) = (List.map edgeOfDart word).reverse

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling (α : Type u_1) (β : Type u_2) : Type (max u_1 u_2)

A relabeling of unoriented edges with an independent orientation reversal for each source edge.

• edgeEquiv : α ≃ β

  The edgeEquiv declaration.

• reverse : α → Bool

  The reverse declaration.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.mapDart {α : Type u_1} {β : Type u_2} (e : EdgeRelabeling α β) : SurfaceCellComplex.SignedDart α → SurfaceCellComplex.SignedDart β

Apply an edge relabeling to a signed dart.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.refl (α : Type u_1) : EdgeRelabeling α α

The identity signed-edge relabeling.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.refl α = { edgeEquiv := Equiv.refl α, reverse := fun (x : α) => false }

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.symm {α : Type u_1} {β : Type u_2} (e : EdgeRelabeling α β) : EdgeRelabeling β α

Reverse a signed-edge relabeling.

Equations

• e.symm = { edgeEquiv := e.edgeEquiv.symm, reverse := fun (b : β) => e.reverse (e.edgeEquiv.symm b) }

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : EdgeRelabeling α β) (f : EdgeRelabeling β γ) : EdgeRelabeling α γ

Compose signed-edge relabelings. Reversing twice cancels, so the reversal bits compose by exclusive-or.

Equations

• e.trans f = { edgeEquiv := e.edgeEquiv.trans f.edgeEquiv, reverse := fun (a : α) => e.reverse a ^^ f.reverse (e.edgeEquiv a) }

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.ofEquiv {α : Type u_1} {β : Type u_2} (e : α ≃ β) : EdgeRelabeling α β

An ordinary edge equivalence, viewed as a relabeling that preserves every chosen orientation.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.ofEquiv e = { edgeEquiv := e, reverse := fun (x : α) => false }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.mapDart_refl {α : Type u_1} (d : SurfaceCellComplex.SignedDart α) : (refl α).mapDart d = d

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.mapDart_symm_apply {α : Type u_1} {β : Type u_2} (e : EdgeRelabeling α β) (d : SurfaceCellComplex.SignedDart α) : e.symm.mapDart (e.mapDart d) = d

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.mapDart_apply_symm {α : Type u_1} {β : Type u_2} (e : EdgeRelabeling α β) (d : SurfaceCellComplex.SignedDart β) : e.mapDart (e.symm.mapDart d) = d

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.dartEquiv {α : Type u_1} {β : Type u_2} (e : EdgeRelabeling α β) : SurfaceCellComplex.SignedDart α ≃ SurfaceCellComplex.SignedDart β

A signed-edge relabeling is an equivalence on darts.

Equations

• e.dartEquiv = { toFun := e.mapDart, invFun := e.symm.mapDart, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.dartEquiv_apply {α : Type u_1} {β : Type u_2} (e : EdgeRelabeling α β) (d : SurfaceCellComplex.SignedDart α) : e.dartEquiv d = e.mapDart d

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.edgeOfDart_mapDart {α : Type u_1} {β : Type u_2} (e : EdgeRelabeling α β) (d : SurfaceCellComplex.SignedDart α) : edgeOfDart (e.mapDart d) = e.edgeEquiv (edgeOfDart d)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.edgeOfDart_dartEquiv {α : Type u_1} {β : Type u_2} (e : EdgeRelabeling α β) (d : SurfaceCellComplex.SignedDart α) : edgeOfDart (e.dartEquiv d) = e.edgeEquiv (edgeOfDart d)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.mapDart_flip {α : Type u_1} {β : Type u_2} (e : EdgeRelabeling α β) (d : SurfaceCellComplex.SignedDart α) : e.mapDart d.flip = (e.mapDart d).flip

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.dartEquiv_flip {α : Type u_1} {β : Type u_2} (e : EdgeRelabeling α β) (d : SurfaceCellComplex.SignedDart α) : e.dartEquiv d.flip = (e.dartEquiv d).flip

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.mapDart_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : EdgeRelabeling α β) (f : EdgeRelabeling β γ) (d : SurfaceCellComplex.SignedDart α) : (e.trans f).mapDart d = f.mapDart (e.mapDart d)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.mapDart_ofEquiv {α : Type u_1} {β : Type u_2} (e : α ≃ β) (d : SurfaceCellComplex.SignedDart α) : (ofEquiv e).mapDart d = (SurfaceCellComplex.SignedDart.mapEquiv e) d

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.map_mapDart_ofEquiv {α : Type u_1} {β : Type u_2} (e : α ≃ β) (l : List (SurfaceCellComplex.SignedDart α)) : List.map (ofEquiv e).mapDart l = List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv e)) l

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.map_mapDart_refl {α : Type u_1} (l : List (SurfaceCellComplex.SignedDart α)) : List.map (refl α).mapDart l = l

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.map_mapDart_symm {α : Type u_1} {β : Type u_2} (e : EdgeRelabeling α β) (l : List (SurfaceCellComplex.SignedDart α)) : List.map e.symm.mapDart (List.map e.mapDart l) = l

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.map_mapDart_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : EdgeRelabeling α β) (f : EdgeRelabeling β γ) (l : List (SurfaceCellComplex.SignedDart α)) : List.map (e.trans f).mapDart l = List.map f.mapDart (List.map e.mapDart l)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.EdgeRelabeling.inverseWord_map_mapDart {α : Type u_1} {β : Type u_2} (e : EdgeRelabeling α β) (word : List (SurfaceCellComplex.SignedDart α)) : inverseWord (List.map e.mapDart word) = List.map e.mapDart (inverseWord word)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.edgeOfDart_mapEquiv {α : Type u_1} {β : Type u_2} (e : α ≃ β) (d : SurfaceCellComplex.SignedDart α) : edgeOfDart ((SurfaceCellComplex.SignedDart.mapEquiv e) d) = e (edgeOfDart d)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.mapEquiv_refl {α : Type u_1} (d : SurfaceCellComplex.SignedDart α) : (SurfaceCellComplex.SignedDart.mapEquiv (Equiv.refl α)) d = d

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.mapEquiv_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f : β ≃ γ) (d : SurfaceCellComplex.SignedDart α) : (SurfaceCellComplex.SignedDart.mapEquiv (e.trans f)) d = (SurfaceCellComplex.SignedDart.mapEquiv f) ((SurfaceCellComplex.SignedDart.mapEquiv e) d)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.mapEquiv_symm_apply {α : Type u_1} {β : Type u_2} (e : α ≃ β) (d : SurfaceCellComplex.SignedDart α) : (SurfaceCellComplex.SignedDart.mapEquiv e.symm) ((SurfaceCellComplex.SignedDart.mapEquiv e) d) = d

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.map_mapEquiv_refl {α : Type u_1} (l : List (SurfaceCellComplex.SignedDart α)) : List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv (Equiv.refl α))) l = l

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.map_mapEquiv_symm {α : Type u_1} {β : Type u_2} (e : α ≃ β) (l : List (SurfaceCellComplex.SignedDart α)) : List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv e.symm)) (List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv e)) l) = l

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.map_mapEquiv_trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : α ≃ β) (f : β ≃ γ) (l : List (SurfaceCellComplex.SignedDart α)) : List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv (e.trans f))) l = List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv f)) (List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv e)) l)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.inverseWord_map_mapEquiv {α : Type u_1} {β : Type u_2} (e : α ≃ β) (word : List (SurfaceCellComplex.SignedDart α)) : inverseWord (List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv e)) word) = List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv e)) (inverseWord word)

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

A face together with one of its two traversal orientations. false selects the stored orientation and true selects its reverse.

• face : P.Face

  The face declaration.

• orientation : Bool

  The orientation declaration.

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.instDecidableEqOrientedFace {P✝ : FiniteCyclicPresentation} : DecidableEq P✝.OrientedFace

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.instDecidableEqOrientedFace.decEq {P✝ : FiniteCyclicPresentation} (x✝ x✝¹ : P✝.OrientedFace) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.instFintypeOrientedFace {P✝ : FiniteCyclicPresentation} : Fintype P✝.OrientedFace

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.OrientedFace.pos {P : FiniteCyclicPresentation} (f : P.Face) : P.OrientedFace

A face with its stored traversal orientation.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.OrientedFace.pos f = { face := f, orientation := false }

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.OrientedFace.neg {P : FiniteCyclicPresentation} (f : P.Face) : P.OrientedFace

A face with the traversal orientation opposite to the stored one.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.OrientedFace.neg f = { face := f, orientation := true }

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.OrientedFace.flip {P : FiniteCyclicPresentation} (f : P.OrientedFace) : P.OrientedFace

Reverse the traversal orientation of a face.

Equations

• f.flip = { face := f.face, orientation := !f.orientation }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.OrientedFace.pos_face {P : FiniteCyclicPresentation} (f : P.Face) : (pos f).face = f

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.OrientedFace.neg_face {P : FiniteCyclicPresentation} (f : P.Face) : (neg f).face = f

@[simp]

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.OrientedFace.flip_pos {P : FiniteCyclicPresentation} (f : P.Face) : (pos f).flip = neg f

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.OrientedFace.flip_neg {P : FiniteCyclicPresentation} (f : P.Face) : (neg f).flip = pos f

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.OrientedFace.flip_flip {P : FiniteCyclicPresentation} (f : P.OrientedFace) : f.flip.flip = f

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.orientedBoundary (P : FiniteCyclicPresentation) (f : P.OrientedFace) : List P.Dart

The boundary of an oriented face, read in its chosen traversal direction.

Equations

• P.orientedBoundary f = if f.orientation = true then LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.inverseWord (P.boundary f.face) else P.boundary f.face

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.orientedBoundary_pos (P : FiniteCyclicPresentation) (f : P.Face) : P.orientedBoundary (OrientedFace.pos f) = P.boundary f

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.orientedBoundary_neg (P : FiniteCyclicPresentation) (f : P.Face) : P.orientedBoundary (OrientedFace.neg f) = inverseWord (P.boundary f)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.orientedBoundary_flip (P : FiniteCyclicPresentation) (f : P.OrientedFace) : P.orientedBoundary f.flip = inverseWord (P.orientedBoundary f)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.orientedBoundary_length (P : FiniteCyclicPresentation) (f : P.OrientedFace) : (P.orientedBoundary f).length = (P.boundary f.face).length

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.faceEdgeMultiplicity (P : FiniteCyclicPresentation) (f : P.Face) (e : P.Edge) : ℕ

Multiplicity of an edge in one face boundary.

Equations

• P.faceEdgeMultiplicity f e = List.count e (List.map LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.edgeOfDart (P.boundary f))

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.orientedBoundary_edgeMultiplicity (P : FiniteCyclicPresentation) (f : P.OrientedFace) (e : P.Edge) : List.count e (List.map edgeOfDart (P.orientedBoundary f)) = P.faceEdgeMultiplicity f.face e

Reading a face boundary in the opposite direction does not change edge multiplicities.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.edgeMultiplicity (P : FiniteCyclicPresentation) (e : P.Edge) : ℕ

Total number of boundary occurrences of an unoriented edge.

Equations

• P.edgeMultiplicity e = ∑ f : P.Face, P.faceEdgeMultiplicity f e

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.IsBoundaryEdge (P : FiniteCyclicPresentation) (e : P.Edge) : Prop

An edge is a boundary edge when it occurs in exactly one face boundary position.

Equations

• P.IsBoundaryEdge e = (P.edgeMultiplicity e = 1)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.IsSurfaceValid (P : FiniteCyclicPresentation) : Prop

Incidence validity for a finite cyclic presentation.

There is at least one face, every face has a nonempty boundary, different faces have different cyclic boundary words, and every edge occurs either once or twice.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.FaceAdjacent (P : FiniteCyclicPresentation) (f g : P.Face) : Prop

Two faces are adjacent when their boundary words contain a common unoriented edge.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.IsConnected (P : FiniteCyclicPresentation) : Prop

Connectivity of the face-edge incidence graph.

Equations

• P.IsConnected = (Nonempty P.Face ∧ ∀ (f g : P.Face), Relation.ReflTransGen P.FaceAdjacent f g)

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.emptyWordSphere : FiniteCyclicPresentation

The exceptional Gallier--Xu presentation with one face, no edges, and an empty boundary.

Definition 6.1 explicitly allows this case. Its geometric realization is assigned to the sphere on page 86.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.emptyWordSphere = { edgeCount := 0, faces := [[]] }

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonSphere : FiniteCyclicPresentation

The two-monogon presentation with boundaries d and d⁻¹.

Gallier--Xu page 86 obtains this presentation from emptyWordSphere by the P2 face split. Unlike the exceptional presentation, it satisfies the ordinary nonempty-boundary validity predicate.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.emptyWordSphere_boundary (f : emptyWordSphere.Face) : emptyWordSphere.boundary f = []

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.emptyWordSphere_isConnected : emptyWordSphere.IsConnected

The exceptional empty-word presentation is connected because it has exactly one face.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.emptyWordSphere_not_isSurfaceValid : ¬emptyWordSphere.IsSurfaceValid

The exceptional presentation is deliberately excluded from ordinary validity.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonSphere_boundary_zero : twoMonogonSphere.boundary 0 = [SurfaceCellComplex.SignedDart.pos 0]

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonSphere_boundary_one : twoMonogonSphere.boundary 1 = [SurfaceCellComplex.SignedDart.neg 0]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonSphere_boundary_nonempty (f : twoMonogonSphere.Face) : twoMonogonSphere.boundary f ≠ []

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonSphere_boundary_injective (f g : twoMonogonSphere.Face) (h : twoMonogonSphere.boundary f ~r twoMonogonSphere.boundary g) : f = g

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonSphere_edgeMultiplicity (e : twoMonogonSphere.Edge) : twoMonogonSphere.edgeMultiplicity e = 2

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonSphere_isSurfaceValid : twoMonogonSphere.IsSurfaceValid

The P2-expanded two-monogon sphere satisfies ordinary incidence validity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonSphere_faceAdjacent (f g : twoMonogonSphere.Face) : twoMonogonSphere.FaceAdjacent f g

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonSphere_isConnected : twoMonogonSphere.IsConnected

The two monogons are adjacent through their common unoriented edge.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PresentationIso (P Q : FiniteCyclicPresentation) : Type

An orientation-preserving isomorphism of finite cyclic presentations, allowing a cyclic rotation of each face. The sign of every dart is retained under edgeEquiv.

• edgeEquiv : P.Edge ≃ Q.Edge

  The edgeEquiv declaration.

• faceEquiv : P.Face ≃ Q.Face

  The faceEquiv declaration.

• boundary_rotated (f : P.Face) : List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv self.edgeEquiv)) (P.boundary f) ~r Q.boundary (self.faceEquiv f)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PresentationIso.refl (P : FiniteCyclicPresentation) : P.PresentationIso P

The identity isomorphism of a finite cyclic presentation.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PresentationIso.refl P = { edgeEquiv := Equiv.refl P.Edge, faceEquiv := Equiv.refl P.Face, boundary_rotated := ⋯ }

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PresentationIso.symm {P Q : FiniteCyclicPresentation} (e : P.PresentationIso Q) : Q.PresentationIso P

Reverse an isomorphism of finite cyclic presentations.

Equations

• e.symm = { edgeEquiv := e.edgeEquiv.symm, faceEquiv := e.faceEquiv.symm, boundary_rotated := ⋯ }

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PresentationIso.trans {P Q R : FiniteCyclicPresentation} (e : P.PresentationIso Q) (f : Q.PresentationIso R) : P.PresentationIso R

Compose isomorphisms of finite cyclic presentations.

Equations

• e.trans f = { edgeEquiv := e.edgeEquiv.trans f.edgeEquiv, faceEquiv := e.faceEquiv.trans f.faceEquiv, boundary_rotated := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PresentationIso.faceEdgeMultiplicity_eq {P Q : FiniteCyclicPresentation} (e : P.PresentationIso Q) (f : P.Face) (a : P.Edge) : P.faceEdgeMultiplicity f a = Q.faceEdgeMultiplicity (e.faceEquiv f) (e.edgeEquiv a)

A presentation isomorphism preserves the multiplicity of an edge in each corresponding face.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PresentationIso.edgeMultiplicity_eq {P Q : FiniteCyclicPresentation} (e : P.PresentationIso Q) (a : P.Edge) : P.edgeMultiplicity a = Q.edgeMultiplicity (e.edgeEquiv a)

A presentation isomorphism preserves total edge multiplicities.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PresentationIso.boundary_length_eq {P Q : FiniteCyclicPresentation} (e : P.PresentationIso Q) (f : P.Face) : (P.boundary f).length = (Q.boundary (e.faceEquiv f)).length

Corresponding face boundaries have the same length.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PresentationIso.map_isRotated {P Q : FiniteCyclicPresentation} (e : P.PresentationIso Q) {f g : P.Face} (h : P.boundary f ~r P.boundary g) : Q.boundary (e.faceEquiv f) ~r Q.boundary (e.faceEquiv g)

Cyclic equivalence of face boundaries is preserved by a presentation isomorphism.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PresentationIso.isRotated_iff {P Q : FiniteCyclicPresentation} (e : P.PresentationIso Q) (f g : P.Face) : P.boundary f ~r P.boundary g ↔ Q.boundary (e.faceEquiv f) ~r Q.boundary (e.faceEquiv g)

Two source boundaries are cyclically equivalent exactly when the corresponding target boundaries are.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PresentationIso.map_faceAdjacent {P Q : FiniteCyclicPresentation} (e : P.PresentationIso Q) {f g : P.Face} (h : P.FaceAdjacent f g) : Q.FaceAdjacent (e.faceEquiv f) (e.faceEquiv g)

Face adjacency is preserved by a presentation isomorphism.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PresentationIso.faceAdjacent_iff {P Q : FiniteCyclicPresentation} (e : P.PresentationIso Q) (f g : P.Face) : P.FaceAdjacent f g ↔ Q.FaceAdjacent (e.faceEquiv f) (e.faceEquiv g)

Face adjacency corresponds exactly under a presentation isomorphism.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PresentationIso.isBoundaryEdge_iff {P Q : FiniteCyclicPresentation} (e : P.PresentationIso Q) (a : P.Edge) : P.IsBoundaryEdge a ↔ Q.IsBoundaryEdge (e.edgeEquiv a)

Boundary-edge status is preserved by a presentation isomorphism.

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

Incidence validity is preserved by a presentation isomorphism.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PresentationIso.isSurfaceValid_iff {P Q : FiniteCyclicPresentation} (e : P.PresentationIso Q) : P.IsSurfaceValid ↔ Q.IsSurfaceValid

Incidence validity corresponds exactly under a presentation isomorphism.

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

Face-incidence connectivity is preserved by a presentation isomorphism.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.PresentationIso.isConnected_iff {P Q : FiniteCyclicPresentation} (e : P.PresentationIso Q) : P.IsConnected ↔ Q.IsConnected

Face-incidence connectivity corresponds exactly under a presentation isomorphism.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso (P Q : FiniteCyclicPresentation) : Type

A signed isomorphism of finite cyclic presentations. Each edge may be independently reoriented while it is renamed; face boundary order is preserved up to cyclic rotation.

• edgeRelabeling : EdgeRelabeling P.Edge Q.Edge

  The edgeRelabeling declaration.

• faceEquiv : P.Face ≃ Q.Face

  The faceEquiv declaration.

• boundary_rotated (f : P.Face) : List.map self.edgeRelabeling.mapDart (P.boundary f) ~r Q.boundary (self.faceEquiv f)

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.edgeEquiv {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) : P.Edge ≃ Q.Edge

The underlying equivalence of unoriented edge names.

Equations

• e.edgeEquiv = e.edgeRelabeling.edgeEquiv

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.reverse {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) : P.Edge → Bool

The orientation-reversal bit attached to a source edge.

Equations

• e.reverse = e.edgeRelabeling.reverse

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.ofPresentationIso {P Q : FiniteCyclicPresentation} (e : P.PresentationIso Q) : P.SignedPresentationIso Q

Regard an orientation-preserving presentation isomorphism as a general signed isomorphism.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.refl (P : FiniteCyclicPresentation) : P.SignedPresentationIso P

The identity signed isomorphism of a finite cyclic presentation.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.symm {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) : Q.SignedPresentationIso P

Reverse a signed isomorphism of finite cyclic presentations.

Equations

• e.symm = { edgeRelabeling := e.edgeRelabeling.symm, faceEquiv := e.faceEquiv.symm, boundary_rotated := ⋯ }

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.trans {P Q R : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (f : Q.SignedPresentationIso R) : P.SignedPresentationIso R

Compose signed isomorphisms of finite cyclic presentations.

Equations

• e.trans f = { edgeRelabeling := e.edgeRelabeling.trans f.edgeRelabeling, faceEquiv := e.faceEquiv.trans f.faceEquiv, boundary_rotated := ⋯ }

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.orientedFaceEquiv {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) : P.OrientedFace ≃ Q.OrientedFace

A signed presentation isomorphism transports the two orientations of every face.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.orientedFaceEquiv_face {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (f : P.OrientedFace) : (e.orientedFaceEquiv f).face = e.faceEquiv f.face

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.orientedFaceEquiv_orientation {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (f : P.OrientedFace) : (e.orientedFaceEquiv f).orientation = f.orientation

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.orientedFaceEquiv_pos {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (f : P.Face) : e.orientedFaceEquiv (OrientedFace.pos f) = OrientedFace.pos (e.faceEquiv f)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.orientedFaceEquiv_neg {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (f : P.Face) : e.orientedFaceEquiv (OrientedFace.neg f) = OrientedFace.neg (e.faceEquiv f)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.orientedFaceEquiv_flip {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (f : P.OrientedFace) : e.orientedFaceEquiv f.flip = (e.orientedFaceEquiv f).flip

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.orientedBoundary_rotated {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (f : P.OrientedFace) : List.map e.edgeRelabeling.mapDart (P.orientedBoundary f) ~r Q.orientedBoundary (e.orientedFaceEquiv f)

A signed presentation isomorphism transports either traversal orientation of every face boundary up to cyclic rotation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.faceEdgeMultiplicity_eq {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (f : P.Face) (a : P.Edge) : P.faceEdgeMultiplicity f a = Q.faceEdgeMultiplicity (e.faceEquiv f) (e.edgeEquiv a)

A signed presentation isomorphism preserves edge multiplicity in each corresponding face.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.edgeMultiplicity_eq {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (a : P.Edge) : P.edgeMultiplicity a = Q.edgeMultiplicity (e.edgeEquiv a)

A signed presentation isomorphism preserves total edge multiplicities.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.boundary_length_eq {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (f : P.Face) : (P.boundary f).length = (Q.boundary (e.faceEquiv f)).length

Corresponding face boundaries have the same length under a signed isomorphism.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.map_isRotated {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) {f g : P.Face} (h : P.boundary f ~r P.boundary g) : Q.boundary (e.faceEquiv f) ~r Q.boundary (e.faceEquiv g)

Cyclic equivalence of face boundaries is preserved by a signed presentation isomorphism.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.isRotated_iff {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (f g : P.Face) : P.boundary f ~r P.boundary g ↔ Q.boundary (e.faceEquiv f) ~r Q.boundary (e.faceEquiv g)

Two source boundaries are cyclically equivalent exactly when the corresponding target boundaries are.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.map_faceAdjacent {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) {f g : P.Face} (h : P.FaceAdjacent f g) : Q.FaceAdjacent (e.faceEquiv f) (e.faceEquiv g)

Face adjacency is preserved by a signed presentation isomorphism.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.faceAdjacent_iff {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (f g : P.Face) : P.FaceAdjacent f g ↔ Q.FaceAdjacent (e.faceEquiv f) (e.faceEquiv g)

Face adjacency corresponds exactly under a signed presentation isomorphism.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.isBoundaryEdge_iff {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (a : P.Edge) : P.IsBoundaryEdge a ↔ Q.IsBoundaryEdge (e.edgeEquiv a)

Boundary-edge status is preserved by a signed presentation isomorphism.

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

Incidence validity is preserved by a signed presentation isomorphism.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.isSurfaceValid_iff {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) : P.IsSurfaceValid ↔ Q.IsSurfaceValid

Incidence validity corresponds exactly under a signed presentation isomorphism.

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

Face-incidence connectivity is preserved by a signed presentation isomorphism.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.isConnected_iff {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) : P.IsConnected ↔ Q.IsConnected

Face-incidence connectivity corresponds exactly under a signed presentation isomorphism.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.IsEmptyWordSphere (P : FiniteCyclicPresentation) : Prop

The signed-isomorphism class of Gallier--Xu's exceptional one-face empty-word sphere.

Equations

• P.IsEmptyWordSphere = Nonempty (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.emptyWordSphere.SignedPresentationIso P)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.IsGallierValid (P : FiniteCyclicPresentation) : Prop

Gallier--Xu validity for the packed presentation layer.

The first disjunct is the ordinary nonempty-boundary case. The second is precisely the exceptional one-face, zero-edge, empty-boundary presentation allowed by Definition 6.1.

Equations

• P.IsGallierValid = (P.IsSurfaceValid ∧ P.IsConnected ∨ P.IsEmptyWordSphere)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.IsEmptyWordSphere.edgeCount_eq_zero {P : FiniteCyclicPresentation} (h : P.IsEmptyWordSphere) : P.edgeCount = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.IsEmptyWordSphere.faces_length_eq_one {P : FiniteCyclicPresentation} (h : P.IsEmptyWordSphere) : P.faces.length = 1

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.IsEmptyWordSphere.boundary_eq_nil {P : FiniteCyclicPresentation} (h : P.IsEmptyWordSphere) (f : P.Face) : P.boundary f = []

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.isEmptyWordSphere_iff (P : FiniteCyclicPresentation) : P.IsEmptyWordSphere ↔ P.edgeCount = 0 ∧ P.faces = [[]]

Intrinsic characterization of the exceptional signed-isomorphism class.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.emptyWordSphere_isEmptyWordSphere : emptyWordSphere.IsEmptyWordSphere

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.IsEmptyWordSphere.isConnected {P : FiniteCyclicPresentation} (h : P.IsEmptyWordSphere) : P.IsConnected

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.IsEmptyWordSphere.not_isSurfaceValid {P : FiniteCyclicPresentation} (h : P.IsEmptyWordSphere) : ¬P.IsSurfaceValid

Empty-word spheres are exactly the exceptional, non-ordinary branch of Gallier validity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.IsEmptyWordSphere.isGallierValid {P : FiniteCyclicPresentation} (h : P.IsEmptyWordSphere) : P.IsGallierValid

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.isGallierValid_of_isSurfaceValid_of_isConnected {P : FiniteCyclicPresentation} (hvalid : P.IsSurfaceValid) (hconnected : P.IsConnected) : P.IsGallierValid

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.emptyWordSphere_isGallierValid : emptyWordSphere.IsGallierValid

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.twoMonogonSphere_isGallierValid : twoMonogonSphere.IsGallierValid

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.IsGallierValid.isConnected {P : FiniteCyclicPresentation} (h : P.IsGallierValid) : P.IsConnected

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.isEmptyWordSphere {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) (h : P.IsEmptyWordSphere) : Q.IsEmptyWordSphere

A signed presentation isomorphism preserves the exceptional empty-word sphere class.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.isEmptyWordSphere_iff {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) : P.IsEmptyWordSphere ↔ Q.IsEmptyWordSphere

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

Gallier--Xu validity is preserved by signed edge and face relabeling.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.SignedPresentationIso.isGallierValid_iff {P Q : FiniteCyclicPresentation} (e : P.SignedPresentationIso Q) : P.IsGallierValid ↔ Q.IsGallierValid