Derived Gallier--Xu word rewrites

This file builds the repeated word transformations used after the primitive P1/P2 phase of the normalization proof. It starts with proof-producing infrastructure for one-face cyclic words:

• cyclic rotation is a signed presentation isomorphism;
• validity transports across any permutation of the underlying unoriented edge occurrences;
• the Dyck rewrite is available with either orientation of its distinguished edge.

These lemmas keep intermediate validity witnesses out of the public derived-chain APIs.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.inverseWord_singleton {α : Type u_1} (d : SurfaceCellComplex.SignedDart α) : inverseWord [d] = [d.flip]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.oneFace_face_eq_zero {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (f : (oneFace word).Face) : f = 0

The unique face of an explicitly indexed one-face presentation.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.oneFace_boundary {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (f : (oneFace word).Face) : (oneFace word).boundary f = word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.oneFace_edgeMultiplicity {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (e : Fin n) : (oneFace word).edgeMultiplicity e = List.count e (List.map edgeOfDart word)

The edge multiplicity of a one-face presentation is the count in its displayed word.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.oneFace_isSurfaceValid_of_edgePerm {n : ℕ} {sourceWord targetWord : List (SurfaceCellComplex.SignedDart (Fin n))} (hperm : (List.map edgeOfDart sourceWord).Perm (List.map edgeOfDart targetWord)) (validSource : (oneFace sourceWord).IsSurfaceValid) : (oneFace targetWord).IsSurfaceValid

A permutation of the unoriented edge occurrences preserves one-face surface validity. Orientation signs and cyclic positions are intentionally irrelevant here.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.oneFaceSignedIsoOfIsRotated {n : ℕ} {sourceWord targetWord : List (SurfaceCellComplex.SignedDart (Fin n))} (hrotated : sourceWord ~r targetWord) : (oneFace sourceWord).SignedPresentationIso (oneFace targetWord)

A cyclic rotation of one displayed face word is a signed presentation isomorphism.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.normalizationEquivalentOfIsRotated {n : ℕ} {sourceWord targetWord : List (SurfaceCellComplex.SignedDart (Fin n))} (hrotated : sourceWord ~r targetWord) (validSource : (oneFace sourceWord).IsSurfaceValid) (validTarget : (oneFace targetWord).IsSurfaceValid) : NormalizationEquivalent { presentation := oneFace sourceWord, valid := validSource } { presentation := oneFace targetWord, valid := validTarget }

A cyclic rotation of ordinary-valid one-face words is a normalization equivalence.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.target_isSurfaceValid {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) (validSource : (source a U V X).IsSurfaceValid) : (target a U V X).IsSurfaceValid

The Dyck rewrite preserves the unoriented edge-occurrence multiset, hence ordinary validity.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.reverseEdgeRelabeling {n : ℕ} (a : Fin n) : EdgeRelabeling (Fin n) (Fin n)

Reverse exactly one named edge orientation.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.reverseEdgeRelabeling a = { edgeEquiv := Equiv.refl (Fin n), reverse := fun (e : Fin n) => decide (e = a) }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.reverseEdgeRelabeling_pos {n : ℕ} (a : Fin n) : (reverseEdgeRelabeling a).mapDart (SurfaceCellComplex.SignedDart.pos a) = SurfaceCellComplex.SignedDart.neg a

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.reverseEdgeRelabeling_neg {n : ℕ} (a : Fin n) : (reverseEdgeRelabeling a).mapDart (SurfaceCellComplex.SignedDart.neg a) = SurfaceCellComplex.SignedDart.pos a

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.reverseEdgeRelabeling_of_ne {n : ℕ} (a e : Fin n) (h : e ≠ a) (orientation : Bool) : (reverseEdgeRelabeling a).mapDart (if orientation = true then SurfaceCellComplex.SignedDart.neg e else SurfaceCellComplex.SignedDart.pos e) = if orientation = true then SurfaceCellComplex.SignedDart.neg e else SurfaceCellComplex.SignedDart.pos e

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.reverseEdgeRelabeling_word {n : ℕ} (a : Fin n) (word : List (SurfaceCellComplex.SignedDart (Fin n))) (ha : a ∉ List.map edgeOfDart word) : List.map (reverseEdgeRelabeling a).mapDart word = word

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.negativeSource {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The negatively oriented spelling of the Dyck source.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.negativeTarget {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The corresponding negatively oriented target spelling.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.negativeSourceSignedIso {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) (haU : a ∉ List.map edgeOfDart U) (haV : a ∉ List.map edgeOfDart V) (haX : a ∉ List.map edgeOfDart X) : (negativeSource a U V X).SignedPresentationIso (source a U V X)

Reversing a identifies the negative source spelling with the positive source spelling.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.negativeTargetSignedIso {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) (haU : a ∉ List.map edgeOfDart U) (haV : a ∉ List.map edgeOfDart V) (haX : a ∉ List.map edgeOfDart X) : (negativeTarget a U V X).SignedPresentationIso (target a U V X)

Reversing a identifies the negative target spelling with the positive target spelling.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.negativeTarget_isSurfaceValid {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) (validSource : (negativeSource a U V X).IsSurfaceValid) : (negativeTarget a U V X).IsSurfaceValid

The negatively spelled Dyck rewrite also preserves ordinary validity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.negativeNormalizationEquivalent {n : ℕ} (a : Fin n) (U V X : List (SurfaceCellComplex.SignedDart (Fin n))) (haU : a ∉ List.map edgeOfDart U) (haV : a ∉ List.map edgeOfDart V) (haX : a ∉ List.map edgeOfDart X) (validSource : (negativeSource a U V X).IsSurfaceValid) (validTarget : (negativeTarget a U V X).IsSurfaceValid) : NormalizationEquivalent { presentation := negativeSource a U V X, valid := validSource } { presentation := negativeTarget a U V X, valid := validTarget }

The generic Dyck rewrite with the distinguished edge displayed negative first.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.target_isSurfaceValid {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) (validSource : (source a X Y).IsSurfaceValid) : (target a X Y).IsSurfaceValid

The cross-cap rewrite preserves the unoriented edge-occurrence multiset, hence validity.

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.negativeSource {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The cross-cap source with the distinguished edge displayed negative.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.negativeTarget {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The corresponding negatively oriented target.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.negativeTarget_isSurfaceValid {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) (validSource : (negativeSource a X Y).IsSurfaceValid) : (negativeTarget a X Y).IsSurfaceValid

The negatively oriented cross-cap rewrite preserves ordinary validity.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.negativeSourceSignedIso {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) (haX : a ∉ List.map edgeOfDart X) (haY : a ∉ List.map edgeOfDart Y) : (negativeSource a X Y).SignedPresentationIso (source a X Y)

The negativeSourceSignedIso declaration.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.negativeTargetSignedIso {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) (haX : a ∉ List.map edgeOfDart X) (haY : a ∉ List.map edgeOfDart Y) : (negativeTarget a X Y).SignedPresentationIso (target a X Y)

The negativeTargetSignedIso declaration.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.negativeNormalizationEquivalent {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) (haX : a ∉ List.map edgeOfDart X) (haY : a ∉ List.map edgeOfDart Y) (validSource : (negativeSource a X Y).IsSurfaceValid) (validTarget : (negativeTarget a X Y).IsSurfaceValid) : NormalizationEquivalent { presentation := negativeSource a X Y, valid := validSource } { presentation := negativeTarget a X Y, valid := validTarget }

The cross-cap rewrite with both distinguished occurrences displayed negative.

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.adjacentSource {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The adjacent-crosscap source a a X Y.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.adjacentTarget {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The alternate cross-cap target a Y a X⁻¹.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.adjacentTarget_isSurfaceValid {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) (validSource : (adjacentSource a X Y).IsSurfaceValid) : (adjacentTarget a X Y).IsSurfaceValid

The alternate adjacent-crosscap rewrite preserves ordinary validity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.adjacentSource_isRotated_target {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : (adjacentSource a X Y).boundary 0 ~r (target a Y (inverseWord X)).boundary 0

a a X Y is a rotation of the ordinary cross-cap target obtained from a Y a X⁻¹.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Crosscap.adjacentNormalizationEquivalent {n : ℕ} (a : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) (haX : a ∉ List.map edgeOfDart X) (haY : a ∉ List.map edgeOfDart Y) (validSource : (adjacentSource a X Y).IsSurfaceValid) (validTarget : (adjacentTarget a X Y).IsSurfaceValid) : NormalizationEquivalent { presentation := adjacentSource a X Y, valid := validSource } { presentation := adjacentTarget a X Y, valid := validTarget }

Gallier--Xu's alternate rule a a X Y ~ a Y a X⁻¹.

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Handle.source {n : ℕ} (a b : Fin n) (U V X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The source spelling for Gallier--Xu handle extraction.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Handle.afterFirst {n : ℕ} (a b : Fin n) (U V X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The result of the first Dyck rewrite.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Handle.secondSource {n : ℕ} (a b : Fin n) (U V X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

A cyclic spelling of afterFirst exposing the two occurrences of b.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Handle.afterSecond {n : ℕ} (a b : Fin n) (U V X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The result of the second Dyck rewrite.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Handle.thirdSource {n : ℕ} (a b : Fin n) (U V X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

A cyclic spelling of afterSecond exposing a⁻¹ before a.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Handle.target {n : ℕ} (a b : Fin n) (U V X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The target spelling contains the handle a b a⁻¹ b⁻¹, followed cyclically by Y X V U.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Handle.target_isSurfaceValid {n : ℕ} (a b : Fin n) (U V X Y : List (SurfaceCellComplex.SignedDart (Fin n))) (validSource : (source a b U V X Y).IsSurfaceValid) : (target a b U V X Y).IsSurfaceValid

Handle extraction preserves the unoriented edge-occurrence multiset, hence ordinary validity.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Handle.target_boundary_isRotated_handle {n : ℕ} (a b : Fin n) (U V X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : (target a b U V X Y).boundary 0 ~r [SurfaceCellComplex.SignedDart.pos a, SurfaceCellComplex.SignedDart.pos b, SurfaceCellComplex.SignedDart.neg a, SurfaceCellComplex.SignedDart.neg b] ++ Y ++ X ++ V ++ U

The chosen target spelling is cyclically the handle a b a⁻¹ b⁻¹, followed by Y X V U.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Handle.afterFirst_isRotated_secondSource {n : ℕ} (a b : Fin n) (U V X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : (afterFirst a b U V X Y).boundary 0 ~r (secondSource a b U V X Y).boundary 0

Rotate the first Dyck target to expose the second distinguished edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Handle.afterSecond_isRotated_thirdSource {n : ℕ} (a b : Fin n) (U V X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : (afterSecond a b U V X Y).boundary 0 ~r (thirdSource a b U V X Y).boundary 0

Rotate the second Dyck target to expose a in the opposite orientation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Handle.normalizationEquivalent {n : ℕ} (a b : Fin n) (U V X Y : List (SurfaceCellComplex.SignedDart (Fin n))) (hab : a ≠ b) (haU : a ∉ List.map edgeOfDart U) (haV : a ∉ List.map edgeOfDart V) (haX : a ∉ List.map edgeOfDart X) (haY : a ∉ List.map edgeOfDart Y) (hbU : b ∉ List.map edgeOfDart U) (hbV : b ∉ List.map edgeOfDart V) (hbX : b ∉ List.map edgeOfDart X) (hbY : b ∉ List.map edgeOfDart Y) (validSource : (source a b U V X Y).IsSurfaceValid) (validTarget : (target a b U V X Y).IsSurfaceValid) : NormalizationEquivalent { presentation := source a b U V X Y, valid := validSource } { presentation := target a b U V X Y, valid := validTarget }

Gallier--Xu's three-Dyck chain extracts the interleaved opposite pairs as a handle.

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HandleToCrosscaps.source {n : ℕ} (a b c : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

A crosscap followed by a handle, with arbitrary intervening words X and Y.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HandleToCrosscaps.afterFirst {n : ℕ} (a b c : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The first alternate cross-cap rewrite.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HandleToCrosscaps.secondSource {n : ℕ} (a b c : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

Rotate the first target to expose the two negative occurrences of b.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HandleToCrosscaps.afterSecond {n : ℕ} (a b c : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The result of rewriting the two negative occurrences of b.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HandleToCrosscaps.thirdSource {n : ℕ} (a b c : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

Expose the two negative occurrences of c.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HandleToCrosscaps.afterThird {n : ℕ} (a b c : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The result of rewriting the two negative occurrences of c.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HandleToCrosscaps.fourthSource {n : ℕ} (a b c : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

Expose the remaining two occurrences of a.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HandleToCrosscaps.target {n : ℕ} (a b c : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The final spelling is cyclically a a X c c b b Y: three crosscaps.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HandleToCrosscaps.afterFirst_isRotated_secondSource {n : ℕ} (a b c : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : (afterFirst a b c X Y).boundary 0 ~r (secondSource a b c X Y).boundary 0

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HandleToCrosscaps.afterSecond_isRotated_thirdSource {n : ℕ} (a b c : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : (afterSecond a b c X Y).boundary 0 ~r (thirdSource a b c X Y).boundary 0

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HandleToCrosscaps.afterThird_isRotated_fourthSource {n : ℕ} (a b c : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : (afterThird a b c X Y).boundary 0 ~r (fourthSource a b c X Y).boundary 0

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HandleToCrosscaps.target_boundary_isRotated_crosscaps {n : ℕ} (a b c : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) : (target a b c X Y).boundary 0 ~r [SurfaceCellComplex.SignedDart.pos a, SurfaceCellComplex.SignedDart.pos a] ++ X ++ [SurfaceCellComplex.SignedDart.pos c, SurfaceCellComplex.SignedDart.pos c, SurfaceCellComplex.SignedDart.pos b, SurfaceCellComplex.SignedDart.pos b] ++ Y

Check the exact final cyclic order of the three crosscaps.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HandleToCrosscaps.normalizationEquivalent {n : ℕ} (a b c : Fin n) (X Y : List (SurfaceCellComplex.SignedDart (Fin n))) (hab : a ≠ b) (hac : a ≠ c) (hbc : b ≠ c) (haX : a ∉ List.map edgeOfDart X) (haY : a ∉ List.map edgeOfDart Y) (hbX : b ∉ List.map edgeOfDart X) (hbY : b ∉ List.map edgeOfDart Y) (hcX : c ∉ List.map edgeOfDart X) (hcY : c ∉ List.map edgeOfDart Y) (validSource : (source a b c X Y).IsSurfaceValid) (validTarget : (target a b c X Y).IsSurfaceValid) : NormalizationEquivalent { presentation := source a b c X Y, valid := validSource } { presentation := target a b c X Y, valid := validTarget }

Gallier--Xu Step 5: a crosscap and a handle are equivalent to three crosscaps.

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.LoopGrouping.source {n : ℕ} (a : Fin n) (H X V : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

A cyclic word with the loop block a H a⁻¹, a separating word X, and a block V to move next to the loop.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.LoopGrouping.rotatedSource {n : ℕ} (a : Fin n) (H X V : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

Rotate the source to expose the negative occurrence of a first.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.LoopGrouping.target {n : ℕ} (a : Fin n) (H X V : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The target is cyclically a H a⁻¹ V X, so V has crossed the separating word X.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.LoopGrouping.target a H X V = LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Dyck.negativeTarget a X V H

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.LoopGrouping.source_isRotated_rotatedSource {n : ℕ} (a : Fin n) (H X V : List (SurfaceCellComplex.SignedDart (Fin n))) : (source a H X V).boundary 0 ~r (rotatedSource a H X V).boundary 0

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.LoopGrouping.target_boundary_isRotated_grouped {n : ℕ} (a : Fin n) (H X V : List (SurfaceCellComplex.SignedDart (Fin n))) : (target a H X V).boundary 0 ~r [SurfaceCellComplex.SignedDart.pos a] ++ H ++ [SurfaceCellComplex.SignedDart.neg a] ++ V ++ X

The target spelling displays the moved block immediately after the loop.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.LoopGrouping.normalizationEquivalent {n : ℕ} (a : Fin n) (H X V : List (SurfaceCellComplex.SignedDart (Fin n))) (haH : a ∉ List.map edgeOfDart H) (haX : a ∉ List.map edgeOfDart X) (haV : a ∉ List.map edgeOfDart V) (validSource : (source a H X V).IsSurfaceValid) (validTarget : (target a H X V).IsSurfaceValid) : NormalizationEquivalent { presentation := source a H X V, valid := validSource } { presentation := target a H X V, valid := validTarget }

Gallier--Xu loop grouping is one negative Dyck rewrite after a cyclic rotation.