Recursive reduction of finite cyclic one-face words

The face-merging recursion deliberately retains each deleted separator as a cyclically adjacent inverse pair. This file supplies the next normalization phase: repeatedly cancel every such pair while preserving a validity-bundled normalization chain. If the final pair is the whole word, the result is the agreed ordinary-valid two-monogon sphere presentation.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.onlyFace (P : FiniteCyclicPresentation) (hfaces : P.faces.length = 1) : P.Face

The unique face of a presentation whose stored face list has length one.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.onlyFace P hfaces = ⟨0, ⋯⟩

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.explicitOneFace (P : FiniteCyclicPresentation) (hfaces : P.faces.length = 1) : FiniteCyclicPresentation

Rewrite an arbitrary one-face presentation using its unique stored boundary word.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.explicitOneFaceSignedIso (P : FiniteCyclicPresentation) (hfaces : P.faces.length = 1) : P.SignedPresentationIso (explicitOneFace P hfaces)

Every presentation with one stored face is signed-isomorphic to its explicit one-word spelling.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.oneFaceSignedIsoToOfOneFaceWord {n : ℕ} {Edge : Type} [Fintype Edge] (sourceWord : List (SurfaceCellComplex.SignedDart (Fin n))) (typedWord : List (SurfaceCellComplex.SignedDart Edge)) (edgeEquiv : Fin n ≃ Edge) (rotated : List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv edgeEquiv)) sourceWord ~r typedWord) : (Dyck.oneFace sourceWord).SignedPresentationIso (ofOneFaceWord typedWord)

Relabel a finished Fin-indexed one-face word directly to the existing typed one-face adapter. This is the final bridge used by canonical normalization; it does not introduce a second spelling of any Lean-Eval representative.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.oneFaceSignedIsoToOfOneFaceWordRelabeling {n : ℕ} {Edge : Type} [Fintype Edge] (sourceWord : List (SurfaceCellComplex.SignedDart (Fin n))) (typedWord : List (SurfaceCellComplex.SignedDart Edge)) (edgeRelabeling : EdgeRelabeling (Fin n) Edge) (rotated : List.map edgeRelabeling.mapDart sourceWord ~r typedWord) : (Dyck.oneFace sourceWord).SignedPresentationIso (ofOneFaceWord typedWord)

Signed version of the finished one-face adapter. In addition to renaming edge names, this allows each finished block edge to be reversed independently before landing at the single project-owned canonical word.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.orientableNormalizationResultOfRotated {k p n : ℕ} (sourceWord : List (SurfaceCellComplex.SignedDart (Fin k))) (edgeEquiv : Fin k ≃ NormalForm.OrientableEdge p n) (rotated : List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv edgeEquiv)) sourceWord ~r NormalForm.orientableBoundaryWord p n) (valid : (Dyck.oneFace sourceWord).IsSurfaceValid) (admissible : (NormalForm.orientable p n).IsEvalAdmissible) : NormalizationResult { presentation := Dyck.oneFace sourceWord, valid := valid }

A finished orientable word, up to its explicit edge relabeling and cyclic rotation, gives a normalization result at the exact existing orientable canonical presentation.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.nonOrientableNormalizationResultOfRotated {k p n : ℕ} (sourceWord : List (SurfaceCellComplex.SignedDart (Fin k))) (edgeEquiv : Fin k ≃ NormalForm.NonOrientableEdge p n) (rotated : List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv edgeEquiv)) sourceWord ~r NormalForm.nonOrientableBoundaryWord p n) (valid : (Dyck.oneFace sourceWord).IsSurfaceValid) (admissible : (NormalForm.nonOrientable p n).IsEvalAdmissible) : NormalizationResult { presentation := Dyck.oneFace sourceWord, valid := valid }

A finished nonorientable word, up to its explicit edge relabeling and cyclic rotation, gives a normalization result at the exact existing nonorientable canonical presentation.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.orientableNormalizationResultOfSignedRotated {k p n : ℕ} (sourceWord : List (SurfaceCellComplex.SignedDart (Fin k))) (edgeRelabeling : EdgeRelabeling (Fin k) (NormalForm.OrientableEdge p n)) (rotated : List.map edgeRelabeling.mapDart sourceWord ~r NormalForm.orientableBoundaryWord p n) (valid : (Dyck.oneFace sourceWord).IsSurfaceValid) (admissible : (NormalForm.orientable p n).IsEvalAdmissible) : NormalizationResult { presentation := Dyck.oneFace sourceWord, valid := valid }

Signed finished orientable word adapter, permitting independent orientation normalization of every handle and boundary-loop edge.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.nonOrientableNormalizationResultOfSignedRotated {k p n : ℕ} (sourceWord : List (SurfaceCellComplex.SignedDart (Fin k))) (edgeRelabeling : EdgeRelabeling (Fin k) (NormalForm.NonOrientableEdge p n)) (rotated : List.map edgeRelabeling.mapDart sourceWord ~r NormalForm.nonOrientableBoundaryWord p n) (valid : (Dyck.oneFace sourceWord).IsSurfaceValid) (admissible : (NormalForm.nonOrientable p n).IsEvalAdmissible) : NormalizationResult { presentation := Dyck.oneFace sourceWord, valid := valid }

Signed finished nonorientable word adapter, permitting independent orientation normalization of every crosscap and boundary-loop edge.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.inversePair {Edge : Type} (a : Edge) : Bool → List (SurfaceCellComplex.SignedDart Edge)

The two possible signed spellings of an adjacent inverse pair.

Equations

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

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.CancellablePair {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : Type

Data exposing a cyclically adjacent inverse pair in a one-face word.

• edge : Fin n

  The edge declaration.

• tail : List (SurfaceCellComplex.SignedDart (Fin n))

  The tail declaration.

• negativeFirst : Bool

  The negativeFirst declaration.

• rotated : word ~r inversePair self.edge self.negativeFirst ++ self.tail

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.IsPairReduced {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : Prop

A one-face word has no cyclically adjacent inverse pair.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.isPairReduced_of_length_lt_two {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (hshort : word.length < 2) : IsPairReduced word

A word with fewer than two darts cannot contain a cyclically adjacent inverse pair.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.CancellablePair.edge_not_mem_tail {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (pair : CancellablePair word) (valid : (Dyck.oneFace word).IsSurfaceValid) : pair.edge ∉ List.map edgeOfDart pair.tail

Validity forces the displayed inverse pair's edge to be absent from its remaining tail.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.predecessor_eq_zero_of_lowerTail_eq_nil {n : ℕ} (a : Fin (n + 1)) (X : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (ha : a ∉ List.map edgeOfDart X) (hlower : Cancellation.lowerTail a X = []) (valid : (Cancellation.namedSource a X).IsSurfaceValid) : n = 0

If deleting a displayed pair leaves the empty word, there were no other edge names.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.ReducedWordResult (P : ValidPresentation) : Type

A reduced non-spherical endpoint reached after inverse-pair cancellation.

• edgeCount : ℕ

  The edgeCount declaration.

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

  The word declaration.

• valid : (Dyck.oneFace self.word).IsSurfaceValid
• reduced : IsPairReduced self.word
• equivalent : NormalizationEquivalent P { presentation := Dyck.oneFace self.word, valid := ⋯ }

inductive LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.CancellationResult (P : ValidPresentation) : Type

Cancellation either reaches the canonical sphere presentation or a pair-reduced one-face word.

• sphere {P : ValidPresentation} (equivalent : NormalizationEquivalent P { presentation := twoMonogonSphere, valid := twoMonogonSphere_isSurfaceValid }) : CancellationResult P
• reduced {P : ValidPresentation} (result : ReducedWordResult P) : CancellationResult P

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.CancellationResult.ofEquivalent {P Q : ValidPresentation} (hPQ : NormalizationEquivalent P Q) : CancellationResult Q → CancellationResult P

Transport a cancellation result backward through a normalization equivalence.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.CancellationResult.finish {P : ValidPresentation} (normalizeReduced : (result : ReducedWordResult P) → NormalizationResult { presentation := Dyck.oneFace result.word, valid := ⋯ }) : CancellationResult P → NormalizationResult P

Finish a cancellation result once pair-reduced one-face words have a canonical normalizer.

Equations

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

@[irreducible]

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.cancelInversePairsFuel (fuel : ℕ) {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (valid : (Dyck.oneFace word).IsSurfaceValid) : word.length ≤ fuel → CancellationResult { presentation := Dyck.oneFace word, valid := valid }

Fuel-bounded implementation of repeated inverse-pair cancellation.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.cancelInversePairs {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (valid : (Dyck.oneFace word).IsSurfaceValid) : CancellationResult { presentation := Dyck.oneFace word, valid := valid }

Repeatedly cancel cyclically adjacent inverse pairs in an ordinary-valid one-face word.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.reduceAndCancel (P : ValidPresentation) (connectedP : P.presentation.IsConnected) : CancellationResult P

Merge a connected valid presentation to one face, rewrite that face explicitly as a cyclic word, and cancel every adjacent inverse pair.

Equations

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

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.PairReducedNormalizer : Type

The remaining proof obligation after face merging and inverse-pair cancellation: normalize an arbitrary pair-reduced valid one-face word.

• normalize {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (valid : (Dyck.oneFace word).IsSurfaceValid) : IsPairReduced word → NormalizationResult { presentation := Dyck.oneFace word, valid := valid }

  The normalize declaration.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.normalizeConnected (normalizer : PairReducedNormalizer) (P : ValidPresentation) (connectedP : P.presentation.IsConnected) : NormalizationResult P

A normalizer for pair-reduced words completes the faithful finite-cyclic Gallier--Xu normalization theorem for every connected valid presentation.

Equations

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

Certified occurrence decompositions for the remaining pairing reduction

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.dart {α : Type u_1} (a : α) : Bool → SurfaceCellComplex.SignedDart α

A signed dart with its orientation represented by a Boolean.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.dart a false = LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.pos a
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.dart a true = LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.neg a

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.dartNegative {α : Type u_1} : SurfaceCellComplex.SignedDart α → Bool

Boolean orientation of a signed dart.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.dartNegative (LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.pos a) = false
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.dartNegative (LeanEval.Topology.ClassificationOfSurfaces.SurfaceCellComplex.SignedDart.neg a) = true

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.signedRelabeling {α : Type u_1} {β : Type u_2} (edgeEquiv : α ≃ β) (reverse : α → Bool) : EdgeRelabeling α β

An edge equivalence equipped with an explicit source-orientation normalization function.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.signedRelabeling edgeEquiv reverse = { edgeEquiv := edgeEquiv, reverse := reverse }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.signedRelabeling_edgeEquiv {α : Type u_1} {β : Type u_2} (edgeEquiv : α ≃ β) (reverse : α → Bool) : (signedRelabeling edgeEquiv reverse).edgeEquiv = edgeEquiv

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.signedRelabeling_reverse {α : Type u_1} {β : Type u_2} (edgeEquiv : α ≃ β) (reverse : α → Bool) (a : α) : (signedRelabeling edgeEquiv reverse).reverse a = reverse a

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.edgeOfDart_dart {α : Type u_1} (a : α) (negative : Bool) : edgeOfDart (dart a negative) = a

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.edgeOfDart_pos {α : Type u_1} (a : α) : edgeOfDart (SurfaceCellComplex.SignedDart.pos a) = a

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.edgeOfDart_neg {α : Type u_1} (a : α) : edgeOfDart (SurfaceCellComplex.SignedDart.neg a) = a

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.dart_edgeOfDart_dartNegative {α : Type u_1} (d : SurfaceCellComplex.SignedDart α) : dart (edgeOfDart d) (dartNegative d) = d

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.signedRelabeling_mapDart_dart_self {α : Type u_1} {β : Type u_2} (edgeEquiv : α ≃ β) (reverse : α → Bool) (a : α) : (signedRelabeling edgeEquiv reverse).mapDart (dart a (reverse a)) = SurfaceCellComplex.SignedDart.pos (edgeEquiv a)

A signed relabeling whose reversal bit is the displayed dart orientation sends that dart to the positive orientation of its renamed edge.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.signedRelabeling_mapDart_dart_not_self {α : Type u_1} {β : Type u_2} (edgeEquiv : α ≃ β) (reverse : α → Bool) (a : α) : (signedRelabeling edgeEquiv reverse).mapDart (dart a !reverse a) = SurfaceCellComplex.SignedDart.neg (edgeEquiv a)

The opposite displayed orientation is normalized to the negative renamed dart.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.boundaryLoopWord {α : Type u_1} (carrier hole : α) (carrierNegative holeNegative : Bool) : List (SurfaceCellComplex.SignedDart α)

Exact signed spelling of one boundary loop before final edge-name and sign normalization.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.map_boundaryLoopWord_normalized {α : Type u_1} {β : Type u_2} (edgeEquiv : α ≃ β) (reverse : α → Bool) (carrier hole : α) (carrierNegative holeNegative : Bool) (hcarrier : reverse carrier = carrierNegative) (hhole : reverse hole = holeNegative) : List.map (signedRelabeling edgeEquiv reverse).mapDart (boundaryLoopWord carrier hole carrierNegative holeNegative) = [SurfaceCellComplex.SignedDart.pos (edgeEquiv carrier), SurfaceCellComplex.SignedDart.pos (edgeEquiv hole), SurfaceCellComplex.SignedDart.neg (edgeEquiv carrier)]

Independent sign normalization sends an arbitrary boundary-loop spelling to the positive carrier, positive hole, negative carrier convention used by the canonical representatives.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.isSurfaceValid_of_p1Expand (P : FiniteCyclicPresentation) (a : P.Edge) (validExpand : (P1.expand P a).IsSurfaceValid) : P.IsSurfaceValid

Ordinary surface validity reflects through a P1 expansion.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.count_edgeOfDart_eq_pos_add_neg {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (a : Fin n) : List.count a (List.map edgeOfDart word) = List.count (SurfaceCellComplex.SignedDart.pos a) word + List.count (SurfaceCellComplex.SignedDart.neg a) word

Unoriented edge count is the sum of its positive and negative dart counts.

inductive LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.EdgePattern {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (a : Fin n) : Type

The four occurrence patterns allowed for one edge of a valid one-face word.

• boundary {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a : Fin n} (total : List.count a (List.map edgeOfDart word) = 1) : EdgePattern word a
• positiveCrosscap {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a : Fin n} (positive : List.count (SurfaceCellComplex.SignedDart.pos a) word = 2) (negative : List.count (SurfaceCellComplex.SignedDart.neg a) word = 0) : EdgePattern word a
• negativeCrosscap {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a : Fin n} (positive : List.count (SurfaceCellComplex.SignedDart.pos a) word = 0) (negative : List.count (SurfaceCellComplex.SignedDart.neg a) word = 2) : EdgePattern word a
• opposite {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a : Fin n} (positive : List.count (SurfaceCellComplex.SignedDart.pos a) word = 1) (negative : List.count (SurfaceCellComplex.SignedDart.neg a) word = 1) : EdgePattern word a

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.HasValidUsedMultiplicities {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : Prop

Every edge name actually used by a residual word still has a surface multiplicity. Unlike IsSurfaceValid, this predicate permits the ambient Fin type to contain already-grouped edge names which no longer occur in the residual word.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.hasValidUsedMultiplicities_of_isSurfaceValid {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (valid : (Dyck.oneFace word).IsSurfaceValid) : HasValidUsedMultiplicities word

Ordinary one-face validity implies valid multiplicity for every used edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.cancellablePair_edge_not_mem_tail_of_usedMultiplicities {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (pair : CancellablePair word) (multiplicities : HasValidUsedMultiplicities word) : pair.edge ∉ List.map edgeOfDart pair.tail

Residual surface multiplicities force the edge of a displayed inverse pair to occur nowhere else in its tail.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.cancellablePair_count_tail_of_mem {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (pair : CancellablePair word) (multiplicities : HasValidUsedMultiplicities word) (e : Fin n) (he : e ∈ List.map edgeOfDart pair.tail) : List.count e (List.map edgeOfDart word) = List.count e (List.map edgeOfDart pair.tail)

Deleting a displayed inverse pair preserves the count of every edge which remains in the tail.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.cancellablePair_hasValidUsedMultiplicities_tail {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (pair : CancellablePair word) (multiplicities : HasValidUsedMultiplicities word) : HasValidUsedMultiplicities pair.tail

Residual surface multiplicities survive deletion of a displayed inverse pair.

inductive LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ResidualPairReductionTrace {n : ℕ} : List (SurfaceCellComplex.SignedDart (Fin n)) → List (SurfaceCellComplex.SignedDart (Fin n)) → Type

Proof-relevant trace of the residual inverse-pair recursion. Keeping the selected pair at each step is essential when the same reduction is later lifted through an ambient marked word: the erased residual endpoint alone does not say which protected token interval the pair crossed.

• done {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (reduced : IsPairReduced word) : ResidualPairReductionTrace word word
• cancel {n : ℕ} {word target : List (SurfaceCellComplex.SignedDart (Fin n))} (pair : CancellablePair word) (tail : ResidualPairReductionTrace pair.tail target) : ResidualPairReductionTrace word target

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ResidualPairReduction {n : ℕ} (sourceWord : List (SurfaceCellComplex.SignedDart (Fin n))) : Type

Certified result of repeatedly deleting adjacent inverse pairs from a residual word. The ambient edge type is intentionally retained: names belonging to already-extracted blocks may be absent from both the input and output residual words. Its trace records the exact recursion choices for subsequent marked execution.

• reducedWord : List (SurfaceCellComplex.SignedDart (Fin n))

  The reducedWord declaration.

• trace : ResidualPairReductionTrace sourceWord self.reducedWord

  The trace declaration.

• multiplicities : HasValidUsedMultiplicities self.reducedWord
• reduced : IsPairReduced self.reducedWord
• count_eq_of_mem (e : Fin n) : e ∈ List.map edgeOfDart self.reducedWord → List.count e (List.map edgeOfDart sourceWord) = List.count e (List.map edgeOfDart self.reducedWord)
• length_le : self.reducedWord.length ≤ sourceWord.length

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ResidualPairReductionTrace.target_isPairReduced {n : ℕ} {source target : List (SurfaceCellComplex.SignedDart (Fin n))} (trace : ResidualPairReductionTrace source target) : IsPairReduced target

The endpoint recorded by a residual cancellation trace is pair-reduced.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ResidualPairReductionTrace.target_length_le {n : ℕ} {source target : List (SurfaceCellComplex.SignedDart (Fin n))} (trace : ResidualPairReductionTrace source target) : target.length ≤ source.length

Residual cancellation never increases word length.

@[irreducible]

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.reduceResidualPairsFuel (fuel : ℕ) {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (multiplicities : HasValidUsedMultiplicities word) : word.length ≤ fuel → ResidualPairReduction word

Fuel-bounded residual inverse-pair cancellation.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.reduceResidualPairs {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (multiplicities : HasValidUsedMultiplicities word) : ResidualPairReduction word

Repeatedly delete every adjacent inverse pair from a residual word while retaining its ambient edge namespace and the surface multiplicities of all surviving names.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ResidualPairReduction.mem_source_of_mem {n : ℕ} {sourceWord : List (SurfaceCellComplex.SignedDart (Fin n))} (result : ResidualPairReduction sourceWord) (e : Fin n) (he : e ∈ List.map edgeOfDart result.reducedWord) : e ∈ List.map edgeOfDart sourceWord

Every name surviving residual cancellation occurred in the input residual word.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.exists_edgePattern_of_multiplicity {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (a : Fin n) (hmultiplicity : List.count a (List.map edgeOfDart word) = 1 ∨ List.count a (List.map edgeOfDart word) = 2) : Nonempty (EdgePattern word a)

A known surface multiplicity classifies the two signed counts of an edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.exists_edgePattern {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (valid : (Dyck.oneFace word).IsSurfaceValid) (a : Fin n) : Nonempty (EdgePattern word a)

Surface validity classifies every edge as boundary, equally oriented, or oppositely oriented.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.exists_decomposition_of_count_eq_one {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (a : Fin n) (hcount : List.count a (List.map edgeOfDart word) = 1) : ∃ (negative : Bool) (left : List (SurfaceCellComplex.SignedDart (Fin n))) (right : List (SurfaceCellComplex.SignedDart (Fin n))), word = left ++ dart a negative :: right ∧ a ∉ List.map edgeOfDart left ∧ a ∉ List.map edgeOfDart right

A list in which a occurs exactly once can be split at that occurrence, with certified absence on both sides.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.DoubleOccurrenceForm {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (a : Fin n) : Type

Cyclic data exposing the two occurrences of a twice-used edge.

• firstNegative : Bool

  The firstNegative declaration.

• secondNegative : Bool

  The secondNegative declaration.

• between : List (SurfaceCellComplex.SignedDart (Fin n))

  The between declaration.

• remainder : List (SurfaceCellComplex.SignedDart (Fin n))

  The remainder declaration.

• rotated : word ~r dart a self.firstNegative :: self.between ++ dart a self.secondNegative :: self.remainder
• edge_not_mem_between : a ∉ List.map edgeOfDart self.between
• edge_not_mem_remainder : a ∉ List.map edgeOfDart self.remainder

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.exists_doubleOccurrenceForm_of_count_eq_two {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (a : Fin n) (hcount : List.count a (List.map edgeOfDart word) = 2) : Nonempty (DoubleOccurrenceForm word a)

Every edge of multiplicity two in a one-face word has a certified cyclic two-occurrence decomposition.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.doubleOccurrenceFormOfMultiplicityTwo {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (_valid : (Dyck.oneFace word).IsSurfaceValid) (a : Fin n) (htwo : (Dyck.oneFace word).edgeMultiplicity a = 2) : DoubleOccurrenceForm word a

Surface validity supplies a double-occurrence form for every twice-used edge.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.doubleOccurrenceFormOfMultiplicityTwo word _valid a htwo = Classical.choice ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.DoubleOccurrenceForm.between_ne_nil_of_opposite {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a : Fin n} (form : DoubleOccurrenceForm word a) (reduced : IsPairReduced word) (hopposite : form.firstNegative ≠ form.secondNegative) : form.between ≠ []

In a pair-reduced word, oppositely oriented occurrences cannot be cyclically adjacent.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CrosscapOccurrenceForm {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (a : Fin n) : Type

A twice-used edge displayed with equal orientations.

• negative : Bool

  The negative declaration.

• between : List (SurfaceCellComplex.SignedDart (Fin n))

  The between declaration.

• remainder : List (SurfaceCellComplex.SignedDart (Fin n))

  The remainder declaration.

• rotated : word ~r dart a self.negative :: self.between ++ dart a self.negative :: self.remainder
• edge_not_mem_between : a ∉ List.map edgeOfDart self.between
• edge_not_mem_remainder : a ∉ List.map edgeOfDart self.remainder

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.OppositeOccurrenceForm {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (a : Fin n) : Type

An oppositely used edge displayed positive first and negative second.

• between : List (SurfaceCellComplex.SignedDart (Fin n))

  The between declaration.

• remainder : List (SurfaceCellComplex.SignedDart (Fin n))

  The remainder declaration.

• rotated : word ~r SurfaceCellComplex.SignedDart.pos a :: self.between ++ SurfaceCellComplex.SignedDart.neg a :: self.remainder
• edge_not_mem_between : a ∉ List.map edgeOfDart self.between
• edge_not_mem_remainder : a ∉ List.map edgeOfDart self.remainder

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.OppositeArcForm {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (a : Fin n) : Type

An orientation-symmetric directed arc between the two opposite occurrences of an edge. Unlike OppositeOccurrenceForm, this form permits either sign at the beginning, which is the right induction invariant when descending to a shorter nested pair.

• firstNegative : Bool

  The firstNegative declaration.

• between : List (SurfaceCellComplex.SignedDart (Fin n))

  The between declaration.

• remainder : List (SurfaceCellComplex.SignedDart (Fin n))

  The remainder declaration.

• rotated : word ~r dart a self.firstNegative :: self.between ++ (dart a !self.firstNegative) :: self.remainder
• edge_not_mem_between : a ∉ List.map edgeOfDart self.between
• edge_not_mem_remainder : a ∉ List.map edgeOfDart self.remainder

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.OppositeOccurrenceForm.toArc {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a : Fin n} (form : OppositeOccurrenceForm word a) : OppositeArcForm word a

Forget the positive-first convention of an opposite occurrence form.

Equations

• form.toArc = { firstNegative := false, between := form.between, remainder := form.remainder, rotated := ⋯, edge_not_mem_between := ⋯, edge_not_mem_remainder := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.OppositeArcForm.between_ne_nil {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a : Fin n} (form : OppositeArcForm word a) (reduced : IsPairReduced word) : form.between ≠ []

Pair reduction makes the directed interval of every opposite arc nonempty.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.InterleavedOccurrenceForm {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (a b : Fin n) : Type

Two oppositely oriented edge pairs whose endpoints interleave cyclically. The first distinguished pair is displayed positive then negative. The Boolean records whether the occurrence of b inside that pair is negative; a signed relabeling will reverse b when necessary before applying handle extraction.

• bNegativeInside : Bool

  The bNegativeInside declaration.

• beforeB : List (SurfaceCellComplex.SignedDart (Fin n))

  The beforeB declaration.

• beforeNegA : List (SurfaceCellComplex.SignedDart (Fin n))

  The beforeNegA declaration.

• beforeOutsideB : List (SurfaceCellComplex.SignedDart (Fin n))

  The beforeOutsideB declaration.

• remainder : List (SurfaceCellComplex.SignedDart (Fin n))

  The remainder declaration.

• rotated : word ~r SurfaceCellComplex.SignedDart.pos a :: self.beforeB ++ dart b self.bNegativeInside :: self.beforeNegA ++ SurfaceCellComplex.SignedDart.neg a :: self.beforeOutsideB ++ (dart b !self.bNegativeInside) :: self.remainder
• edge_ne : a ≠ b
• a_not_mem_beforeB : a ∉ List.map edgeOfDart self.beforeB
• a_not_mem_beforeNegA : a ∉ List.map edgeOfDart self.beforeNegA
• a_not_mem_beforeOutsideB : a ∉ List.map edgeOfDart self.beforeOutsideB
• a_not_mem_remainder : a ∉ List.map edgeOfDart self.remainder
• b_not_mem_beforeB : b ∉ List.map edgeOfDart self.beforeB
• b_not_mem_beforeNegA : b ∉ List.map edgeOfDart self.beforeNegA
• b_not_mem_beforeOutsideB : b ∉ List.map edgeOfDart self.beforeOutsideB
• b_not_mem_remainder : b ∉ List.map edgeOfDart self.remainder

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.exists_positiveCrosscapOccurrenceForm {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (a : Fin n) (hpositive : List.count (SurfaceCellComplex.SignedDart.pos a) word = 2) (hnegative : List.count (SurfaceCellComplex.SignedDart.neg a) word = 0) : Nonempty (CrosscapOccurrenceForm word a)

A positive crosscap edge has an equally oriented occurrence form.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.exists_negativeCrosscapOccurrenceForm {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (a : Fin n) (hpositive : List.count (SurfaceCellComplex.SignedDart.pos a) word = 0) (hnegative : List.count (SurfaceCellComplex.SignedDart.neg a) word = 2) : Nonempty (CrosscapOccurrenceForm word a)

A negative crosscap edge has an equally oriented occurrence form.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.exists_oppositeOccurrenceForm {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (a : Fin n) (hpositive : List.count (SurfaceCellComplex.SignedDart.pos a) word = 1) (hnegative : List.count (SurfaceCellComplex.SignedDart.neg a) word = 1) : Nonempty (OppositeOccurrenceForm word a)

An opposite edge has a cyclic spelling with its positive occurrence first.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryOccurrenceForm {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (a : Fin n) : Type

A once-used boundary edge displayed at the cyclic head.

• negative : Bool

  The negative declaration.

• remainder : List (SurfaceCellComplex.SignedDart (Fin n))

  The remainder declaration.

• rotated : word ~r dart a self.negative :: self.remainder
• edge_not_mem_remainder : a ∉ List.map edgeOfDart self.remainder

inductive LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionFeature {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : Type

A pairing feature on which the normalization recursion can immediately act.

• boundary {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (a : Fin n) (form : BoundaryOccurrenceForm word a) : ActionablePairReductionFeature word
• crosscap {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (a : Fin n) (form : CrosscapOccurrenceForm word a) : ActionablePairReductionFeature word
• handle {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (a b : Fin n) (form : InterleavedOccurrenceForm word a b) : ActionablePairReductionFeature word

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionFeature.residualWord {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} : ActionablePairReductionFeature word → List (SurfaceCellComplex.SignedDart (Fin n))

Delete the darts of the extracted block, retaining the exact residual order produced by the proof-generating rewrite endpoint.

Equations

• One or more equations did not get rendered due to their size.
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionFeature.boundary a form).residualWord = form.remainder

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionFeature.residualWord_length_lt {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (feature : ActionablePairReductionFeature word) : feature.residualWord.length < word.length

Every actionable extraction strictly shortens its residual word.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionFeature.count_residualWord_of_mem {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (feature : ActionablePairReductionFeature word) (e : Fin n) (he : e ∈ List.map edgeOfDart feature.residualWord) : List.count e (List.map edgeOfDart word) = List.count e (List.map edgeOfDart feature.residualWord)

Counts of every edge still used by the residual word agree with their counts in the source word.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionFeature.mem_source_of_mem_residualWord {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (feature : ActionablePairReductionFeature word) (e : Fin n) (he : e ∈ List.map edgeOfDart feature.residualWord) : e ∈ List.map edgeOfDart word

Every edge name retained by an actionable feature occurred in its source word.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionFeature.hasValidUsedMultiplicities_residualWord {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (feature : ActionablePairReductionFeature word) (multiplicities : HasValidUsedMultiplicities word) : HasValidUsedMultiplicities feature.residualWord

Used-edge surface multiplicities survive deletion of an extracted block.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.Cancellation.lowerEdge {n : ℕ} (a e : Fin (n + 1)) (hne : e ≠ a) : Fin n

Lower an edge name after moving a distinguished, unused name to the last position.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.Cancellation.castSucc_lowerEdge {n : ℕ} (a e : Fin (n + 1)) (hne : e ≠ a) : (lowerEdge a e hne).castSucc = (Cancellation.moveToLast a) e

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.Cancellation.restoreEdge {n : ℕ} (a : Fin (n + 1)) (e : Fin n) : Fin (n + 1)

Re-embed a lowered edge into the old namespace, undoing the move-to-last relabeling.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.Cancellation.restoreEdge_lowerEdge {n : ℕ} (a e : Fin (n + 1)) (hne : e ≠ a) : restoreEdge a (lowerEdge a e hne) = e

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.Cancellation.lowerDart {n : ℕ} (a : Fin (n + 1)) (d : SurfaceCellComplex.SignedDart (Fin (n + 1))) (hne : edgeOfDart d ≠ a) : SurfaceCellComplex.SignedDart (Fin n)

The lowerDart declaration.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.Cancellation.restoreDart {n : ℕ} (a : Fin (n + 1)) : SurfaceCellComplex.SignedDart (Fin n) → SurfaceCellComplex.SignedDart (Fin (n + 1))

Re-embed a lowered dart into the old namespace.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.Cancellation.restoreDart_lowerDart {n : ℕ} (a : Fin (n + 1)) (d : SurfaceCellComplex.SignedDart (Fin (n + 1))) (hne : edgeOfDart d ≠ a) : restoreDart a (lowerDart a d hne) = d

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.Cancellation.restoreEdge_edgeOfDart_lowerDart {n : ℕ} (a : Fin (n + 1)) (d : SurfaceCellComplex.SignedDart (Fin (n + 1))) (hne : edgeOfDart d ≠ a) : restoreEdge a (edgeOfDart (lowerDart a d hne)) = edgeOfDart d

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.Cancellation.contractDart_mapEquiv_moveToLast {n : ℕ} (a : Fin (n + 1)) (d : SurfaceCellComplex.SignedDart (Fin (n + 1))) (hne : edgeOfDart d ≠ a) : P1.contractDart ((SurfaceCellComplex.SignedDart.mapEquiv (Cancellation.moveToLast a)) d) = some (lowerDart a d hne)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.Cancellation.lowerWordAvoiding {n : ℕ} (a : Fin (n + 1)) (word : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) : a ∉ List.map edgeOfDart word → List (SurfaceCellComplex.SignedDart (Fin n))

Lower a word which avoids a distinguished edge, preserving its exact dart order.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.Cancellation.lowerWordAvoiding a [] x_2 = []

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.Cancellation.lowerWordAvoiding_eq_lowerTail {n : ℕ} (a : Fin (n + 1)) (word : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (ha : a ∉ List.map edgeOfDart word) : lowerWordAvoiding a word ha = Cancellation.lowerTail a word

Lowering a word explicitly agrees with moving the removed name last and applying P1 contraction.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.Cancellation.lowerTail_ne_nil_of_ne_nil {n : ℕ} (a : Fin (n + 1)) (word : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (ha : a ∉ List.map edgeOfDart word) (hne : word ≠ []) : Cancellation.lowerTail a word ≠ []

Removing an absent ambient edge name does not turn a nonempty word into the empty word.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.Cancellation.restoreEdges_lowerTail {n : ℕ} (a : Fin (n + 1)) (word : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (ha : a ∉ List.map edgeOfDart word) : List.map (restoreEdge a) (List.map edgeOfDart (Cancellation.lowerTail a word)) = List.map edgeOfDart word

Re-embedding all names in a lowered word recovers the source edge-name list exactly.

inductive LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock (n : ℕ) : Type

The combinatorial block contributed by one actionable extraction. Orientations on boundary and crosscap blocks are retained until the final signed relabeling; handle extraction has already normalized both distinguished edge orientations.

• boundary {n : ℕ} (a : Fin n) (negative : Bool) : ExtractedBlock n
• crosscap {n : ℕ} (a : Fin n) (negative : Bool) : ExtractedBlock n
• handle {n : ℕ} (a b : Fin n) : ExtractedBlock n

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.edges {n : ℕ} : ExtractedBlock n → List (Fin n)

Ambient edge names consumed by an extracted block.

Equations

• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.boundary a negative).edges = [a]
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.crosscap a negative).edges = [a]
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.handle a b).edges = [a, b]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.word {n : ℕ} : ExtractedBlock n → List (SurfaceCellComplex.SignedDart (Fin n))

Exact signed word contributed by an extracted block.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.inverse {n : ℕ} : ExtractedBlock n → ExtractedBlock n

Block obtained by reading an extracted block backwards with every dart reversed.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.mapEquiv {n m : ℕ} (e : Fin n ≃ Fin m) : ExtractedBlock n → ExtractedBlock m

Relabel every ambient edge name in an extracted block.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.lowerAvoiding {n : ℕ} (a : Fin (n + 1)) (block : ExtractedBlock (n + 1)) (ha : a ∉ block.edges) : ExtractedBlock n

Remove an ambient edge name known not to occur in an extracted block.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.word_inverse {n : ℕ} (block : ExtractedBlock n) : block.inverse.word = inverseWord block.word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.inverse_inverse {n : ℕ} (block : ExtractedBlock n) : block.inverse.inverse = block

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.edges_inverse {n : ℕ} (block : ExtractedBlock n) : block.inverse.edges = block.edges.reverse

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.word_mapEquiv {n m : ℕ} (e : Fin n ≃ Fin m) (block : ExtractedBlock n) : (mapEquiv e block).word = List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv e)) block.word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.edges_mapEquiv {n m : ℕ} (e : Fin n ≃ Fin m) (block : ExtractedBlock n) : (mapEquiv e block).edges = List.map (⇑e) block.edges

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.mem_map_edgeOfDart_word_iff {n : ℕ} (block : ExtractedBlock n) (a : Fin n) : a ∈ List.map edgeOfDart block.word ↔ a ∈ block.edges

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.inverse_mapEquiv {n m : ℕ} (e : Fin n ≃ Fin m) (block : ExtractedBlock n) : (mapEquiv e block).inverse = mapEquiv e block.inverse

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.map_word_boundary_normalized {n : ℕ} {Edge : Type u_1} (edgeEquiv : Fin n ≃ Edge) (reverse : Fin n → Bool) (a : Fin n) (negative : Bool) (horientation : reverse a = negative) : List.map (signedRelabeling edgeEquiv reverse).mapDart (boundary a negative).word = [SurfaceCellComplex.SignedDart.pos (edgeEquiv a)]

A boundary singleton is positive after reversing precisely its recorded input orientation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.map_word_crosscap_normalized {n : ℕ} {Edge : Type u_1} (edgeEquiv : Fin n ≃ Edge) (reverse : Fin n → Bool) (a : Fin n) (negative : Bool) (horientation : reverse a = negative) : List.map (signedRelabeling edgeEquiv reverse).mapDart (crosscap a negative).word = [SurfaceCellComplex.SignedDart.pos (edgeEquiv a), SurfaceCellComplex.SignedDart.pos (edgeEquiv a)]

A crosscap square is positive after reversing precisely its recorded input orientation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.map_word_handle_normalized {n : ℕ} {Edge : Type u_1} (edgeEquiv : Fin n ≃ Edge) (reverse : Fin n → Bool) (a b : Fin n) (ha : reverse a = false) (hb : reverse b = false) : List.map (signedRelabeling edgeEquiv reverse).mapDart (handle a b).word = [SurfaceCellComplex.SignedDart.pos (edgeEquiv a), SurfaceCellComplex.SignedDart.pos (edgeEquiv b), SurfaceCellComplex.SignedDart.neg (edgeEquiv a), SurfaceCellComplex.SignedDart.neg (edgeEquiv b)]

An extracted handle already has the canonical commutator orientation whenever neither of its two edge names is reversed by the final signed relabeling.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.word_lowerAvoiding {n : ℕ} (a : Fin (n + 1)) (block : ExtractedBlock (n + 1)) (ha : a ∉ block.edges) : (lowerAvoiding a block ha).word = Cancellation.lowerTail a block.word

Expanding a lowered block agrees with renaming its old spelling and contracting the unused last edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.edges_lowerAvoiding_map_restoreEdge {n : ℕ} (a : Fin (n + 1)) (block : ExtractedBlock (n + 1)) (ha : a ∉ block.edges) : List.map (Cancellation.restoreEdge a) (lowerAvoiding a block ha).edges = block.edges

Re-embedding the edge names of a lowered block recovers its original edge list.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.sequenceWord {n : ℕ} (blocks : List (ExtractedBlock n)) : List (SurfaceCellComplex.SignedDart (Fin n))

Concatenate a sequence of extracted blocks into its exact signed boundary word.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.inverseSequence {n : ℕ} (blocks : List (ExtractedBlock n)) : List (ExtractedBlock n)

Reverse a block sequence in the order induced by reversing its full signed word.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.sequenceWord_nil {n : ℕ} : sequenceWord [] = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.sequenceWord_cons {n : ℕ} (block : ExtractedBlock n) (blocks : List (ExtractedBlock n)) : sequenceWord (block :: blocks) = block.word ++ sequenceWord blocks

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.sequenceWord_append {n : ℕ} (left right : List (ExtractedBlock n)) : sequenceWord (left ++ right) = sequenceWord left ++ sequenceWord right

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ExtractedBlock.sequenceWord_inverseSequence {n : ℕ} (blocks : List (ExtractedBlock n)) : sequenceWord (inverseSequence blocks) = inverseWord (sequenceWord blocks)

inductive LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock (n : ℕ) : Type

A completed normalization block. Boundary singletons are absent: a boundary block enters this type only after a residual carrier pair has closed it into the three-dart loop required by the canonical representatives.

• crosscap {n : ℕ} (a : Fin n) (negative : Bool) : CompletedBlock n
• handle {n : ℕ} (a b : Fin n) : CompletedBlock n
• boundary {n : ℕ} (carrier hole : Fin n) (carrierNegative holeNegative : Bool) : CompletedBlock n

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.word {n : ℕ} : CompletedBlock n → List (SurfaceCellComplex.SignedDart (Fin n))

Exact signed word represented by a completed block.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.edges {n : ℕ} : CompletedBlock n → List (Fin n)

Ambient edge names used by a completed block.

Equations

• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.crosscap a negative).edges = [a]
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.handle a b).edges = [a, b]
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.boundary carrier hole carrierNegative holeNegative).edges = [carrier, hole, carrier]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.names {n : ℕ} : CompletedBlock n → List (Fin n)

Distinct-name spine of a completed block. Unlike edges, this records a boundary carrier once rather than once per dart occurrence.

Equations

• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.crosscap a negative).names = [a]
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.handle a b).names = [a, b]
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.boundary carrier hole carrierNegative holeNegative).names = [carrier, hole]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.inverse {n : ℕ} : CompletedBlock n → CompletedBlock n

Reverse a completed block as one atomic cyclic-word segment.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.mapEquiv {n m : ℕ} (e : Fin n ≃ Fin m) : CompletedBlock n → CompletedBlock m

Relabel every edge of a completed block.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.lowerAvoiding {n : ℕ} (a : Fin (n + 1)) (block : CompletedBlock (n + 1)) (ha : a ∉ block.edges) : CompletedBlock n

Remove an ambient edge name known not to occur in a completed block.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.word_inverse {n : ℕ} (block : CompletedBlock n) : block.inverse.word = inverseWord block.word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.inverse_inverse {n : ℕ} (block : CompletedBlock n) : block.inverse.inverse = block

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.edges_inverse {n : ℕ} (block : CompletedBlock n) : block.inverse.edges = block.edges.reverse

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.names_inverse_perm {n : ℕ} (block : CompletedBlock n) : block.inverse.names.Perm block.names

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.word_mapEquiv {n m : ℕ} (e : Fin n ≃ Fin m) (block : CompletedBlock n) : (mapEquiv e block).word = List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv e)) block.word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.edges_mapEquiv {n m : ℕ} (e : Fin n ≃ Fin m) (block : CompletedBlock n) : (mapEquiv e block).edges = List.map (⇑e) block.edges

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.inverse_mapEquiv {n m : ℕ} (e : Fin n ≃ Fin m) (block : CompletedBlock n) : (mapEquiv e block).inverse = mapEquiv e block.inverse

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.mem_map_edgeOfDart_word_iff {n : ℕ} (block : CompletedBlock n) (a : Fin n) : a ∈ List.map edgeOfDart block.word ↔ a ∈ block.edges

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.mem_names_iff_mem_edges {n : ℕ} (block : CompletedBlock n) (a : Fin n) : a ∈ block.names ↔ a ∈ block.edges

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.word_lowerAvoiding {n : ℕ} (a : Fin (n + 1)) (block : CompletedBlock (n + 1)) (ha : a ∉ block.edges) : (lowerAvoiding a block ha).word = Cancellation.lowerTail a block.word

Expanding a lowered completed block agrees with word-level cancellation lowering.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.edges_lowerAvoiding_map_restoreEdge {n : ℕ} (a : Fin (n + 1)) (block : CompletedBlock (n + 1)) (ha : a ∉ block.edges) : List.map (Cancellation.restoreEdge a) (lowerAvoiding a block ha).edges = block.edges

Re-embedding the edge names of a lowered completed block recovers the old edge list.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.names_lowerAvoiding_map_restoreEdge {n : ℕ} (a : Fin (n + 1)) (block : CompletedBlock (n + 1)) (ha : a ∉ block.edges) : List.map (Cancellation.restoreEdge a) (lowerAvoiding a block ha).names = block.names

Re-embedding the distinct names of a lowered block recovers its old name spine.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.sequenceWord {n : ℕ} (blocks : List (CompletedBlock n)) : List (SurfaceCellComplex.SignedDart (Fin n))

Concatenate a completed block sequence into its exact signed one-face word.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.sequenceWord_nil {n : ℕ} : sequenceWord [] = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.sequenceWord_cons {n : ℕ} (block : CompletedBlock n) (blocks : List (CompletedBlock n)) : sequenceWord (block :: blocks) = block.word ++ sequenceWord blocks

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.sequenceWord_append {n : ℕ} (left right : List (CompletedBlock n)) : sequenceWord (left ++ right) = sequenceWord left ++ sequenceWord right

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.sequenceNames {n : ℕ} (blocks : List (CompletedBlock n)) : List (Fin n)

Concatenate the distinct-name spines owned by a completed block sequence.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.sequenceNames_nil {n : ℕ} : sequenceNames [] = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.sequenceNames_cons {n : ℕ} (block : CompletedBlock n) (blocks : List (CompletedBlock n)) : sequenceNames (block :: blocks) = block.names ++ sequenceNames blocks

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.crosscapCount {n : ℕ} : List (CompletedBlock n) → ℕ

Number of completed crosscap blocks.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.crosscapCount [] = 0

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.handleCount {n : ℕ} : List (CompletedBlock n) → ℕ

Number of completed handle blocks.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.handleCount [] = 0

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.boundaryCount {n : ℕ} : List (CompletedBlock n) → ℕ

Number of completed boundary-loop blocks.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.boundaryCount [] = 0

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.normalForm {n : ℕ} (blocks : List (CompletedBlock n)) : NormalForm

Normal-form parameters selected by a completed block sequence.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.count_sum_eq_length {n : ℕ} (blocks : List (CompletedBlock n)) : boundaryCount blocks + crosscapCount blocks + handleCount blocks = blocks.length

Every completed block belongs to exactly one normal-form block class.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.normalForm_isEvalAdmissible_of_ne_nil {n : ℕ} (blocks : List (CompletedBlock n)) (hne : blocks ≠ []) : (normalForm blocks).IsEvalAdmissible

A nonempty completed block sequence selects an Eval-admissible normal form.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryBlockCommute.sourceWord {n : ℕ} (outer carrier hole : Fin n) (outerNegative holeNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin n))

A completed positive-carrier boundary loop lying inside an opposite residual pair.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryBlockCommute.targetWord {n : ℕ} (outer carrier hole : Fin n) (outerNegative holeNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin n))

Move the completed loop outside the residual pair, leaving the residual pair around the strictly shorter protected interval.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryBlockCommute.negativeSourceWord {n : ℕ} (outer carrier hole : Fin n) (outerNegative holeNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin n))

The same contextual loop with its carrier displayed negative first.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryBlockCommute.negativeTargetWord {n : ℕ} (outer carrier hole : Fin n) (outerNegative holeNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin n))

Negative-carrier target spelling.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryBlockCommute.exists_positiveNormalizationEquivalent {n : ℕ} (outer carrier hole : Fin n) (outerNegative holeNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) (hcarrierHole : carrier ≠ hole) (hcarrierOuter : carrier ≠ outer) (hcarrierInside : carrier ∉ List.map edgeOfDart insideTail) (hcarrierOutside : carrier ∉ List.map edgeOfDart outsideTail) (validSource : (Dyck.oneFace (sourceWord outer carrier hole outerNegative holeNegative insideTail outsideTail)).IsSurfaceValid) : ∃ (validTarget : (Dyck.oneFace (targetWord outer carrier hole outerNegative holeNegative insideTail outsideTail)).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace (sourceWord outer carrier hole outerNegative holeNegative insideTail outsideTail), valid := validSource } { presentation := Dyck.oneFace (targetWord outer carrier hole outerNegative holeNegative insideTail outsideTail), valid := validTarget }

Positive-carrier boundary-loop commuting is exactly one LoopGrouping rewrite between two cyclic rotations.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryBlockCommute.negativeSourceSignedIso {n : ℕ} (outer carrier hole : Fin n) (outerNegative holeNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) (hcarrierHole : carrier ≠ hole) (hcarrierOuter : carrier ≠ outer) (hcarrierInside : carrier ∉ List.map edgeOfDart insideTail) (hcarrierOutside : carrier ∉ List.map edgeOfDart outsideTail) : (Dyck.oneFace (negativeSourceWord outer carrier hole outerNegative holeNegative insideTail outsideTail)).SignedPresentationIso (Dyck.oneFace (sourceWord outer carrier hole outerNegative holeNegative insideTail outsideTail))

Reversing only the loop carrier identifies the negative and positive source spellings.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryBlockCommute.negativeTargetSignedIso {n : ℕ} (outer carrier hole : Fin n) (outerNegative holeNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) (hcarrierHole : carrier ≠ hole) (hcarrierOuter : carrier ≠ outer) (hcarrierInside : carrier ∉ List.map edgeOfDart insideTail) (hcarrierOutside : carrier ∉ List.map edgeOfDart outsideTail) : (Dyck.oneFace (negativeTargetWord outer carrier hole outerNegative holeNegative insideTail outsideTail)).SignedPresentationIso (Dyck.oneFace (targetWord outer carrier hole outerNegative holeNegative insideTail outsideTail))

Reversing only the loop carrier identifies the negative and positive target spellings.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryBlockCommute.exists_negativeNormalizationEquivalent {n : ℕ} (outer carrier hole : Fin n) (outerNegative holeNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) (hcarrierHole : carrier ≠ hole) (hcarrierOuter : carrier ≠ outer) (hcarrierInside : carrier ∉ List.map edgeOfDart insideTail) (hcarrierOutside : carrier ∉ List.map edgeOfDart outsideTail) (validSource : (Dyck.oneFace (negativeSourceWord outer carrier hole outerNegative holeNegative insideTail outsideTail)).IsSurfaceValid) : ∃ (validTarget : (Dyck.oneFace (negativeTargetWord outer carrier hole outerNegative holeNegative insideTail outsideTail)).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace (negativeSourceWord outer carrier hole outerNegative holeNegative insideTail outsideTail), valid := validSource } { presentation := Dyck.oneFace (negativeTargetWord outer carrier hole outerNegative holeNegative insideTail outsideTail), valid := validTarget }

Negative-carrier boundary-loop commuting reduces to the positive theorem by a signed presentation isomorphism at each endpoint.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundarySingletonClosure.sourceWord {n : ℕ} (carrier hole : Fin n) (carrierNegative holeNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin n))

A raw boundary dart already lying between adjacent opposite carrier occurrences, followed by two contextual tails.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundarySingletonClosure.targetWord {n : ℕ} (carrier hole : Fin n) (carrierNegative holeNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin n))

Close the raw boundary dart into a completed loop and move the remaining protected interval past that loop.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundarySingletonClosure.exists_positiveNormalizationEquivalent {n : ℕ} (carrier hole : Fin n) (holeNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) (hcarrierHole : carrier ≠ hole) (hcarrierInside : carrier ∉ List.map edgeOfDart insideTail) (hcarrierOutside : carrier ∉ List.map edgeOfDart outsideTail) (validSource : (Dyck.oneFace (sourceWord carrier hole false holeNegative insideTail outsideTail)).IsSurfaceValid) : ∃ (validTarget : (Dyck.oneFace (targetWord carrier hole false holeNegative insideTail outsideTail)).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace (sourceWord carrier hole false holeNegative insideTail outsideTail), valid := validSource } { presentation := Dyck.oneFace (targetWord carrier hole false holeNegative insideTail outsideTail), valid := validTarget }

Positive-carrier contextual boundary closure is exactly one LoopGrouping rewrite.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundarySingletonClosure.negativeSourceSignedIso {n : ℕ} (carrier hole : Fin n) (holeNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) (hcarrierHole : carrier ≠ hole) (hcarrierInside : carrier ∉ List.map edgeOfDart insideTail) (hcarrierOutside : carrier ∉ List.map edgeOfDart outsideTail) : (Dyck.oneFace (sourceWord carrier hole true holeNegative insideTail outsideTail)).SignedPresentationIso (Dyck.oneFace (sourceWord carrier hole false holeNegative insideTail outsideTail))

Reversing the carrier identifies negative- and positive-carrier contextual sources.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundarySingletonClosure.negativeTargetSignedIso {n : ℕ} (carrier hole : Fin n) (holeNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) (hcarrierHole : carrier ≠ hole) (hcarrierInside : carrier ∉ List.map edgeOfDart insideTail) (hcarrierOutside : carrier ∉ List.map edgeOfDart outsideTail) : (Dyck.oneFace (targetWord carrier hole true holeNegative insideTail outsideTail)).SignedPresentationIso (Dyck.oneFace (targetWord carrier hole false holeNegative insideTail outsideTail))

Reversing the carrier identifies negative- and positive-carrier contextual targets.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundarySingletonClosure.exists_negativeNormalizationEquivalent {n : ℕ} (carrier hole : Fin n) (holeNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) (hcarrierHole : carrier ≠ hole) (hcarrierInside : carrier ∉ List.map edgeOfDart insideTail) (hcarrierOutside : carrier ∉ List.map edgeOfDart outsideTail) (validSource : (Dyck.oneFace (sourceWord carrier hole true holeNegative insideTail outsideTail)).IsSurfaceValid) : ∃ (validTarget : (Dyck.oneFace (targetWord carrier hole true holeNegative insideTail outsideTail)).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace (sourceWord carrier hole true holeNegative insideTail outsideTail), valid := validSource } { presentation := Dyck.oneFace (targetWord carrier hole true holeNegative insideTail outsideTail), valid := validTarget }

Negative-carrier contextual boundary closure reduces to the positive theorem through signed presentation isomorphisms at both endpoints.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryAtomRotate.sourceWord {n : ℕ} (carrier hole : Fin n) (carrierNegative holeNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin n))

A raw boundary atom followed by a nonempty protected interval inside an opposite pair.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryAtomRotate.targetWord {n : ℕ} (carrier hole : Fin n) (carrierNegative holeNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin n))

Move the raw boundary atom to the end of the protected interval, exposing its next atom.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryAtomRotate.exists_normalizationEquivalent {n : ℕ} (carrier hole : Fin n) (carrierNegative holeNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) (hcarrierHole : carrier ≠ hole) (hcarrierInside : carrier ∉ List.map edgeOfDart insideTail) (hcarrierOutside : carrier ∉ List.map edgeOfDart outsideTail) (validSource : (Dyck.oneFace (sourceWord carrier hole carrierNegative holeNegative insideTail outsideTail)).IsSurfaceValid) : ∃ (validTarget : (Dyck.oneFace (targetWord carrier hole carrierNegative holeNegative insideTail outsideTail)).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace (sourceWord carrier hole carrierNegative holeNegative insideTail outsideTail), valid := validSource } { presentation := Dyck.oneFace (targetWord carrier hole carrierNegative holeNegative insideTail outsideTail), valid := validTarget }

Rotating a raw boundary atom through a protected interval is one signed Dyck rewrite.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CrosscapBlockCommute.positiveSourceWord {n : ℕ} (outer carrier : Fin n) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin n))

A positive completed crosscap lying at the head of a positive/negative residual pair.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CrosscapBlockCommute.positiveTargetWord {n : ℕ} (outer carrier : Fin n) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin n))

Commute the completed crosscap through the residual pair. The old residual carrier becomes the completed crosscap, while the old crosscap carrier becomes the residual pair around the strictly shorter protected interval.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CrosscapBlockCommute.sourceWord {n : ℕ} (outer carrier : Fin n) (outerNegative carrierNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin n))

Contextual crosscap source with arbitrary orientations on both distinguished edges.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CrosscapBlockCommute.targetWord {n : ℕ} (outer carrier : Fin n) (outerNegative carrierNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin n))

Arbitrarily oriented contextual crosscap target.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CrosscapBlockCommute.orientationRelabeling {n : ℕ} (outer carrier : Fin n) (outerNegative carrierNegative : Bool) : EdgeRelabeling (Fin n) (Fin n)

Reverse exactly the displayed orientations of the two distinguished edges.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CrosscapBlockCommute.orientationRelabeling_mapDart_outer {n : ℕ} (outer carrier : Fin n) (outerNegative carrierNegative : Bool) : (orientationRelabeling outer carrier outerNegative carrierNegative).mapDart (dart outer outerNegative) = SurfaceCellComplex.SignedDart.pos outer

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CrosscapBlockCommute.orientationRelabeling_mapDart_outer_opposite {n : ℕ} (outer carrier : Fin n) (outerNegative carrierNegative : Bool) : (orientationRelabeling outer carrier outerNegative carrierNegative).mapDart (dart outer !outerNegative) = SurfaceCellComplex.SignedDart.neg outer

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CrosscapBlockCommute.orientationRelabeling_mapDart_carrier {n : ℕ} (outer carrier : Fin n) (outerNegative carrierNegative : Bool) (hcarrierOuter : carrier ≠ outer) : (orientationRelabeling outer carrier outerNegative carrierNegative).mapDart (dart carrier carrierNegative) = SurfaceCellComplex.SignedDart.pos carrier

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CrosscapBlockCommute.orientationRelabeling_mapDart_carrier_opposite {n : ℕ} (outer carrier : Fin n) (outerNegative carrierNegative : Bool) (hcarrierOuter : carrier ≠ outer) : (orientationRelabeling outer carrier outerNegative carrierNegative).mapDart (dart carrier !carrierNegative) = SurfaceCellComplex.SignedDart.neg carrier

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CrosscapBlockCommute.orientationRelabeling_word {n : ℕ} (outer carrier : Fin n) (outerNegative carrierNegative : Bool) (word : List (SurfaceCellComplex.SignedDart (Fin n))) (houter : outer ∉ List.map edgeOfDart word) (hcarrier : carrier ∉ List.map edgeOfDart word) : List.map (orientationRelabeling outer carrier outerNegative carrierNegative).mapDart word = word

The two-edge orientation normalization fixes every word avoiding both distinguished names.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CrosscapBlockCommute.sourceSignedIso {n : ℕ} (outer carrier : Fin n) (outerNegative carrierNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) (hcarrierOuter : carrier ≠ outer) (hcarrierInside : carrier ∉ List.map edgeOfDart insideTail) (hcarrierOutside : carrier ∉ List.map edgeOfDart outsideTail) (houterInside : outer ∉ List.map edgeOfDart insideTail) (houterOutside : outer ∉ List.map edgeOfDart outsideTail) : (Dyck.oneFace (sourceWord outer carrier outerNegative carrierNegative insideTail outsideTail)).SignedPresentationIso (Dyck.oneFace (positiveSourceWord outer carrier insideTail outsideTail))

Independent sign normalization identifies the generic and positive source spellings.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CrosscapBlockCommute.targetSignedIso {n : ℕ} (outer carrier : Fin n) (outerNegative carrierNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) (hcarrierOuter : carrier ≠ outer) (hcarrierInside : carrier ∉ List.map edgeOfDart insideTail) (hcarrierOutside : carrier ∉ List.map edgeOfDart outsideTail) (houterInside : outer ∉ List.map edgeOfDart insideTail) (houterOutside : outer ∉ List.map edgeOfDart outsideTail) : (Dyck.oneFace (targetWord outer carrier outerNegative carrierNegative insideTail outsideTail)).SignedPresentationIso (Dyck.oneFace (positiveTargetWord outer carrier insideTail outsideTail))

Independent sign normalization identifies the generic and positive target spellings.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CrosscapBlockCommute.exists_positiveNormalizationEquivalent {n : ℕ} (outer carrier : Fin n) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) (hcarrierOuter : carrier ≠ outer) (hcarrierInside : carrier ∉ List.map edgeOfDart insideTail) (hcarrierOutside : carrier ∉ List.map edgeOfDart outsideTail) (houterInside : outer ∉ List.map edgeOfDart insideTail) (houterOutside : outer ∉ List.map edgeOfDart outsideTail) (validSource : (Dyck.oneFace (positiveSourceWord outer carrier insideTail outsideTail)).IsSurfaceValid) : ∃ (validTarget : (Dyck.oneFace (positiveTargetWord outer carrier insideTail outsideTail)).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace (positiveSourceWord outer carrier insideTail outsideTail), valid := validSource } { presentation := Dyck.oneFace (positiveTargetWord outer carrier insideTail outsideTail), valid := validTarget }

The positive contextual crosscap commute is an adjacent-crosscap rewrite followed by an ordinary crosscap grouping, with cyclic rotations between the displayed spellings.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CrosscapBlockCommute.exists_normalizationEquivalent {n : ℕ} (outer carrier : Fin n) (outerNegative carrierNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) (hcarrierOuter : carrier ≠ outer) (hcarrierInside : carrier ∉ List.map edgeOfDart insideTail) (hcarrierOutside : carrier ∉ List.map edgeOfDart outsideTail) (houterInside : outer ∉ List.map edgeOfDart insideTail) (houterOutside : outer ∉ List.map edgeOfDart outsideTail) (validSource : (Dyck.oneFace (sourceWord outer carrier outerNegative carrierNegative insideTail outsideTail)).IsSurfaceValid) : ∃ (validTarget : (Dyck.oneFace (targetWord outer carrier outerNegative carrierNegative insideTail outsideTail)).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace (sourceWord outer carrier outerNegative carrierNegative insideTail outsideTail), valid := validSource } { presentation := Dyck.oneFace (targetWord outer carrier outerNegative carrierNegative insideTail outsideTail), valid := validTarget }

Contextual crosscap commuting supports arbitrary orientations on both distinguished edges.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.HandleBlockCommute.positiveSourceWord {n : ℕ} (outer first second : Fin n) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin n))

A completed handle at the head of a positive/negative residual pair.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.HandleBlockCommute.positiveTargetWord {n : ℕ} (outer first second : Fin n) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin n))

The same completed handle commuted outside the residual pair.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.HandleBlockCommute.negativeSourceWord {n : ℕ} (outer first second : Fin n) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin n))

The contextual handle source with its residual carrier displayed negative first.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.HandleBlockCommute.negativeTargetWord {n : ℕ} (outer first second : Fin n) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin n))

Negative-residual-carrier target spelling.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.HandleBlockCommute.sourceWord {n : ℕ} (outer first second : Fin n) (outerNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin n))

Contextual handle source with arbitrary residual-carrier orientation.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.HandleBlockCommute.targetWord {n : ℕ} (outer first second : Fin n) (outerNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin n))

Contextual handle target with arbitrary residual-carrier orientation.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.HandleBlockCommute.negativeSourceSignedIso {n : ℕ} (outer first second : Fin n) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) (hfirstOuter : first ≠ outer) (hsecondOuter : second ≠ outer) (houterInside : outer ∉ List.map edgeOfDart insideTail) (houterOutside : outer ∉ List.map edgeOfDart outsideTail) : (Dyck.oneFace (negativeSourceWord outer first second insideTail outsideTail)).SignedPresentationIso (Dyck.oneFace (positiveSourceWord outer first second insideTail outsideTail))

Reversing only the residual carrier identifies negative and positive handle sources.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.HandleBlockCommute.negativeTargetSignedIso {n : ℕ} (outer first second : Fin n) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) (hfirstOuter : first ≠ outer) (hsecondOuter : second ≠ outer) (houterInside : outer ∉ List.map edgeOfDart insideTail) (houterOutside : outer ∉ List.map edgeOfDart outsideTail) : (Dyck.oneFace (negativeTargetWord outer first second insideTail outsideTail)).SignedPresentationIso (Dyck.oneFace (positiveTargetWord outer first second insideTail outsideTail))

Reversing only the residual carrier identifies negative and positive handle targets.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.HandleBlockCommute.exists_positiveNormalizationEquivalent {n : ℕ} (outer first second : Fin n) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) (hfirstSecond : first ≠ second) (hfirstOuter : first ≠ outer) (hsecondOuter : second ≠ outer) (hfirstInside : first ∉ List.map edgeOfDart insideTail) (hfirstOutside : first ∉ List.map edgeOfDart outsideTail) (hsecondInside : second ∉ List.map edgeOfDart insideTail) (hsecondOutside : second ∉ List.map edgeOfDart outsideTail) (validSource : (Dyck.oneFace (positiveSourceWord outer first second insideTail outsideTail)).IsSurfaceValid) : ∃ (validTarget : (Dyck.oneFace (positiveTargetWord outer first second insideTail outsideTail)).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace (positiveSourceWord outer first second insideTail outsideTail), valid := validSource } { presentation := Dyck.oneFace (positiveTargetWord outer first second insideTail outsideTail), valid := validTarget }

Commuting a completed handle through a residual pair is a four-Dyck chain.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.HandleBlockCommute.exists_normalizationEquivalent {n : ℕ} (outer first second : Fin n) (outerNegative : Bool) (insideTail outsideTail : List (SurfaceCellComplex.SignedDart (Fin n))) (hfirstSecond : first ≠ second) (hfirstOuter : first ≠ outer) (hsecondOuter : second ≠ outer) (hfirstInside : first ∉ List.map edgeOfDart insideTail) (hfirstOutside : first ∉ List.map edgeOfDart outsideTail) (hsecondInside : second ∉ List.map edgeOfDart insideTail) (hsecondOutside : second ∉ List.map edgeOfDart outsideTail) (houterInside : outer ∉ List.map edgeOfDart insideTail) (houterOutside : outer ∉ List.map edgeOfDart outsideTail) (validSource : (Dyck.oneFace (sourceWord outer first second outerNegative insideTail outsideTail)).IsSurfaceValid) : ∃ (validTarget : (Dyck.oneFace (targetWord outer first second outerNegative insideTail outsideTail)).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace (sourceWord outer first second outerNegative insideTail outsideTail), valid := validSource } { presentation := Dyck.oneFace (targetWord outer first second outerNegative insideTail outsideTail), valid := validTarget }

Contextual handle commuting supports either orientation of the residual carrier.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryPairContraction.sourceWord {n : ℕ} (first second : Fin (n + 1)) (firstNegative secondNegative : Bool) (tail : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))

Two consecutive extracted boundary darts with arbitrary independent orientations.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryPairContraction.targetWord {n : ℕ} (first second : Fin (n + 1)) (hfirstSecond : first ≠ second) (tail : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) : List (SurfaceCellComplex.SignedDart (Fin n))

Contract the second boundary edge and retain one positively normalized boundary dart.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryPairContraction.expandWord_avoiding {n : ℕ} (edge : Fin n) (word : List (SurfaceCellComplex.SignedDart (Fin n))) (hedge : edge ∉ List.map edgeOfDart word) : P1.expandWord edge word = P2.retainWord word

P1 expansion is just edge-name retention on a word avoiding the subdivided edge.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryPairContraction.sourceSignSignedIso {n : ℕ} (first second : Fin (n + 1)) (firstNegative secondNegative : Bool) (tail : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (hfirstSecond : first ≠ second) (hfirstTail : first ∉ List.map edgeOfDart tail) (hsecondTail : second ∉ List.map edgeOfDart tail) : (Dyck.oneFace (sourceWord first second firstNegative secondNegative tail)).SignedPresentationIso (Dyck.oneFace (sourceWord first second false false tail))

Independent sign normalization identifies the generic and positive adjacent-boundary spellings.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryPairContraction.positiveSourceSignedIso {n : ℕ} (first second : Fin (n + 1)) (tail : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (hfirstSecond : first ≠ second) (hfirstTail : first ∉ List.map edgeOfDart tail) (hsecondTail : second ∉ List.map edgeOfDart tail) : (Dyck.oneFace (sourceWord first second false false tail)).SignedPresentationIso (P1.expand (Dyck.oneFace (targetWord first second hfirstSecond tail)) (Cancellation.lowerEdge second first hfirstSecond))

The positive adjacent-boundary spelling is exactly a P1 expansion after moving the second edge to the fresh-last name.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryPairContraction.exists_normalizationEquivalent {n : ℕ} (first second : Fin (n + 1)) (firstNegative secondNegative : Bool) (tail : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) (hfirstSecond : first ≠ second) (hfirstTail : first ∉ List.map edgeOfDart tail) (hsecondTail : second ∉ List.map edgeOfDart tail) (validSource : (Dyck.oneFace (sourceWord first second firstNegative secondNegative tail)).IsSurfaceValid) : ∃ (validTarget : (Dyck.oneFace (targetWord first second hfirstSecond tail)).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace (sourceWord first second firstNegative secondNegative tail), valid := validSource } { presentation := Dyck.oneFace (targetWord first second hfirstSecond tail), valid := validTarget }

Contracting two adjacent once-used boundary darts is a signed isomorphism followed by one inverse P1 move.

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryEnvelope.source {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

A one-face word before a fresh opposite carrier pair is introduced.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryEnvelope.carrier (n : ℕ) : Fin (n + 1)

The fresh carrier name in the enlarged edge type.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryEnvelope.targetWord {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))

Enclose a retained word in a fresh positively oriented carrier pair.

Equations

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

@[reducible]

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryEnvelope.target {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : FiniteCyclicPresentation

The target declaration.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryEnvelope.sourceCut {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : (source word).P2Cut

The one-sided source split creates the carrier as a face separator.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryEnvelope.targetCut {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : (target word).P2Cut

Split the enveloped target between its two carrier occurrences.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryEnvelope.expandedCarrier {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : (P2.split (source word) (sourceCut word)).Edge

The separator edge selected for P1 expansion in the source split.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryEnvelope.subdivisionCarrier {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : (P1.expand (P2.split (source word) (sourceCut word)) (expandedCarrier word)).Edge

The retained half of the expanded source separator.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryEnvelope.subdivisionRelabeling {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : EdgeRelabeling (P1.expand (P2.split (source word) (sourceCut word)) (expandedCarrier word)).Edge (P2.split (target word) (targetCut word)).Edge

Reverse the retained separator when identifying the two common subdivisions.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryEnvelope.subdivisionFaceEquiv {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : (P1.expand (P2.split (source word) (sourceCut word)) (expandedCarrier word)).Face ≃ (P2.split (target word) (targetCut word)).Face

The subdivisionFaceEquiv declaration.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryEnvelope.subdivisionSignedIso {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : (P1.expand (P2.split (source word) (sourceCut word)) (expandedCarrier word)).SignedPresentationIso (P2.split (target word) (targetCut word))

Expanding the source separator and splitting the enveloped target give signed-isomorphic two-face presentations.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryEnvelope.target_isSurfaceValid {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (validSource : (source word).IsSurfaceValid) : (target word).IsSurfaceValid

The enveloping carrier adds one twice-used name and retains all old multiplicities.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryEnvelope.sourceCut_isOneSided {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (hne : word ≠ []) : (sourceCut word).left = [] ∧ 0 < (sourceCut word).right.length ∨ 0 < (sourceCut word).left.length ∧ (sourceCut word).right = []

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryEnvelope.targetCut_isNondegenerate {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : (targetCut word).IsNondegenerate

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryEnvelope.normalizationEquivalent {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (hne : word ≠ []) (validSource : (source word).IsSurfaceValid) : NormalizationEquivalent { presentation := source word, valid := validSource } { presentation := target word, valid := ⋯ }

Add a fresh opposite carrier pair around a nonempty one-face word. A one-sided P2 split followed by P1 has the same subdivision as a genuine split of the enveloped target.

inductive LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom (n : ℕ) : Type

One non-residual atom allowed in a classified marked execution state.

• boundary {n : ℕ} (hole : Fin n) (negative : Bool) : ProtectedAtom n
• completed {n : ℕ} (block : CompletedBlock n) : ProtectedAtom n

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.word {n : ℕ} : ProtectedAtom n → List (SurfaceCellComplex.SignedDart (Fin n))

Exact signed word represented by one classified protected atom.

Equations

• One or more equations did not get rendered due to their size.
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.completed block).word = block.word

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.edges {n : ℕ} : ProtectedAtom n → List (Fin n)

Edge names protected by one classified atom.

Equations

• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.boundary hole negative).edges = [hole]
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.completed block).edges = block.edges

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.names {n : ℕ} : ProtectedAtom n → List (Fin n)

Distinct protected names owned by one classified atom.

Equations

• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.boundary hole negative).names = [hole]
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.completed block).names = block.names

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.retainCompleted {n : ℕ} : CompletedBlock n → CompletedBlock (n + 1)

Retain a completed block when one fresh ambient carrier name is added.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.retain {n : ℕ} : ProtectedAtom n → ProtectedAtom (n + 1)

Retain a protected atom when one fresh ambient carrier name is added.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.inverse {n : ℕ} : ProtectedAtom n → ProtectedAtom n

Reverse one protected atom.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.sequenceWord {n : ℕ} (atoms : List (ProtectedAtom n)) : List (SurfaceCellComplex.SignedDart (Fin n))

Concatenate a protected atom sequence into its exact signed word.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.sequenceNames {n : ℕ} (atoms : List (ProtectedAtom n)) : List (Fin n)

Concatenate the distinct-name spines owned by a protected atom sequence.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.sequenceNames_cons {n : ℕ} (head : ProtectedAtom n) (tail : List (ProtectedAtom n)) : sequenceNames (head :: tail) = head.names ++ sequenceNames tail

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.inverseSequence {n : ℕ} (atoms : List (ProtectedAtom n)) : List (ProtectedAtom n)

Reverse a protected atom sequence at atom granularity.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.word_inverse {n : ℕ} (atom : ProtectedAtom n) : atom.inverse.word = inverseWord atom.word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.sequenceWord_nil {n : ℕ} : sequenceWord [] = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.sequenceWord_cons {n : ℕ} (atom : ProtectedAtom n) (atoms : List (ProtectedAtom n)) : sequenceWord (atom :: atoms) = atom.word ++ sequenceWord atoms

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.sequenceWord_append {n : ℕ} (left right : List (ProtectedAtom n)) : sequenceWord (left ++ right) = sequenceWord left ++ sequenceWord right

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.sequenceWord_inverseSequence {n : ℕ} (atoms : List (ProtectedAtom n)) : sequenceWord (inverseSequence atoms) = inverseWord (sequenceWord atoms)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.word_retainCompleted {n : ℕ} (block : CompletedBlock n) : (retainCompleted block).word = P2.retainWord block.word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.names_retainCompleted {n : ℕ} (block : CompletedBlock n) : (retainCompleted block).names = List.map Fin.castSucc block.names

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.word_retain {n : ℕ} (atom : ProtectedAtom n) : atom.retain.word = P2.retainWord atom.word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.names_retain {n : ℕ} (atom : ProtectedAtom n) : atom.retain.names = List.map Fin.castSucc atom.names

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.sequenceWord_map_retain {n : ℕ} (atoms : List (ProtectedAtom n)) : sequenceWord (List.map retain atoms) = P2.retainWord (sequenceWord atoms)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.sequenceNames_map_retain {n : ℕ} (atoms : List (ProtectedAtom n)) : sequenceNames (List.map retain atoms) = List.map Fin.castSucc (sequenceNames atoms)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.rawBoundaryCount {n : ℕ} : List (ProtectedAtom n) → ℕ

Number of raw once-used boundary darts. Terminal normalization groups and contracts every such dart to one representative of the remaining outer boundary component.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.rawBoundaryCount [] = 0

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.completedBoundaryCount {n : ℕ} : List (ProtectedAtom n) → ℕ

Number of boundary components already displayed as completed carrier loops.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.completedBoundaryCount [] = 0

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.boundaryCount {n : ℕ} (atoms : List (ProtectedAtom n)) : ℕ

Number of boundary components selected by a terminal atom sequence. Completed loops are already distinct boundary components. All remaining raw boundary darts lie on the one outer boundary component and therefore contribute one component collectively, rather than one each.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.crosscapCount {n : ℕ} : List (ProtectedAtom n) → ℕ

Number of completed crosscap blocks.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.crosscapCount [] = 0

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.handleCount {n : ℕ} : List (ProtectedAtom n) → ℕ

Number of completed handle blocks.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.handleCount [] = 0

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.normalForm {n : ℕ} (atoms : List (ProtectedAtom n)) : NormalForm

Normal-form parameters selected by a terminal protected-atom sequence. Completed boundary loops contribute individually; any remaining raw boundary darts collectively contribute the one outer boundary component and will be grouped during terminal normalization.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.raw_completed_count_sum_eq_length {n : ℕ} (atoms : List (ProtectedAtom n)) : rawBoundaryCount atoms + completedBoundaryCount atoms + crosscapCount atoms + handleCount atoms = atoms.length

Every protected atom is raw boundary data or belongs to exactly one completed block class.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.normalForm_isEvalAdmissible_of_ne_nil {n : ℕ} (atoms : List (ProtectedAtom n)) (hne : atoms ≠ []) : (normalForm atoms).IsEvalAdmissible

A nonempty terminal protected-atom sequence selects an Eval-admissible normal form.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.exists_eq_map_completed_of_rawBoundaryCount_eq_zero {n : ℕ} (atoms : List (ProtectedAtom n)) (hraw : rawBoundaryCount atoms = 0) : ∃ (blocks : List (CompletedBlock n)), atoms = List.map completed blocks

A protected atom sequence with no raw boundary singleton consists entirely of completed blocks.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.sequenceWord_map_completed {n : ℕ} (blocks : List (CompletedBlock n)) : sequenceWord (List.map completed blocks) = CompletedBlock.sequenceWord blocks

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.sequenceNames_map_completed {n : ℕ} (blocks : List (CompletedBlock n)) : sequenceNames (List.map completed blocks) = CompletedBlock.sequenceNames blocks

inductive LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken (n : ℕ) : Type

A marked normalization word. Residual darts are still available to subsequent pairing reductions; extracted blocks are atomic tokens whose exact dart succession must be preserved.

• residual {n : ℕ} (dart : SurfaceCellComplex.SignedDart (Fin n)) : ReductionToken n
• extracted {n : ℕ} (block : ExtractedBlock n) : ReductionToken n
• completed {n : ℕ} (block : CompletedBlock n) : ReductionToken n

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.ofProtectedAtom {n : ℕ} : ProtectedAtom n → ReductionToken n

Embed a classified protected atom as one marked token.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.rawBoundaryCount {n : ℕ} : List (ReductionToken n) → ℕ

Number of still-raw boundary singleton tokens in a marked word.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.rawBoundaryCount [] = 0

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.rawBoundaryCount_append {n : ℕ} (left right : List (ReductionToken n)) : rawBoundaryCount (left ++ right) = rawBoundaryCount left + rawBoundaryCount right

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.rawBoundaryCount_map_ofProtectedAtom {n : ℕ} (atoms : List (ProtectedAtom n)) : rawBoundaryCount (List.map ofProtectedAtom atoms) = ProtectedAtom.rawBoundaryCount atoms

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.word {n : ℕ} : ReductionToken n → List (SurfaceCellComplex.SignedDart (Fin n))

Exact signed word represented by one marked token.

Equations

• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residual dart).word = [dart]
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extracted block).word = block.word
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.completed block).word = block.word

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualWord {n : ℕ} : ReductionToken n → List (SurfaceCellComplex.SignedDart (Fin n))

Residual contribution of one marked token.

Equations

• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residual dart).residualWord = [dart]
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extracted block).residualWord = []
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.completed block).residualWord = []

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extractedEdges {n : ℕ} : ReductionToken n → List (Fin n)

Edge names protected inside one extracted-block token.

Equations

• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residual dart).extractedEdges = []
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extracted block).extractedEdges = block.edges
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.completed block).extractedEdges = block.edges

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extractedNames {n : ℕ} : ReductionToken n → List (Fin n)

One occurrence of every protected edge name represented by a token.

Equations

• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residual dart).extractedNames = []
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extracted block).extractedNames = block.edges
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.completed block).extractedNames = block.names

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.word_residual {n : ℕ} (dart : SurfaceCellComplex.SignedDart (Fin n)) : (residual dart).word = [dart]

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.word_extracted {n : ℕ} (block : ExtractedBlock n) : (extracted block).word = block.word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.word_completed {n : ℕ} (block : CompletedBlock n) : (completed block).word = block.word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualWord_residual {n : ℕ} (dart : SurfaceCellComplex.SignedDart (Fin n)) : (residual dart).residualWord = [dart]

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualWord_extracted {n : ℕ} (block : ExtractedBlock n) : (extracted block).residualWord = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualWord_completed {n : ℕ} (block : CompletedBlock n) : (completed block).residualWord = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extractedEdges_residual {n : ℕ} (dart : SurfaceCellComplex.SignedDart (Fin n)) : (residual dart).extractedEdges = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extractedEdges_extracted {n : ℕ} (block : ExtractedBlock n) : (extracted block).extractedEdges = block.edges

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extractedEdges_completed {n : ℕ} (block : CompletedBlock n) : (completed block).extractedEdges = block.edges

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extractedNames_residual {n : ℕ} (dart : SurfaceCellComplex.SignedDart (Fin n)) : (residual dart).extractedNames = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extractedNames_extracted {n : ℕ} (block : ExtractedBlock n) : (extracted block).extractedNames = block.edges

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extractedNames_completed {n : ℕ} (block : CompletedBlock n) : (completed block).extractedNames = block.names

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.mem_extractedNames_iff_mem_extractedEdges {n : ℕ} (token : ReductionToken n) (a : Fin n) : a ∈ token.extractedNames ↔ a ∈ token.extractedEdges

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.IsClassified {n : ℕ} : ReductionToken n → Prop

Structural grammar of marked execution states. Extracted crosscaps and handles are promoted immediately to completed blocks; only a boundary singleton may remain in the intermediate extracted constructor.

Equations

• One or more equations did not get rendered due to their size.
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residual dart).IsClassified = True
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extracted block).IsClassified = False
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.completed block).IsClassified = True

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.AllClassified {n : ℕ} (tokens : List (ReductionToken n)) : Prop

Every token in a marked execution state obeys the classified-token grammar.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.AllClassified tokens = ∀ token ∈ tokens, token.IsClassified

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.isClassified_residual {n : ℕ} (d : SurfaceCellComplex.SignedDart (Fin n)) : (residual d).IsClassified

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.isClassified_boundary {n : ℕ} (a : Fin n) (negative : Bool) : (extracted (ExtractedBlock.boundary a negative)).IsClassified

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.isClassified_completed {n : ℕ} (block : CompletedBlock n) : (completed block).IsClassified

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.isClassified_ofProtectedAtom {n : ℕ} (atom : ProtectedAtom n) : (ofProtectedAtom atom).IsClassified

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.word_ofProtectedAtom {n : ℕ} (atom : ProtectedAtom n) : (ofProtectedAtom atom).word = atom.word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualWord_ofProtectedAtom {n : ℕ} (atom : ProtectedAtom n) : (ofProtectedAtom atom).residualWord = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extractedEdges_ofProtectedAtom {n : ℕ} (atom : ProtectedAtom n) : (ofProtectedAtom atom).extractedEdges = atom.edges

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extractedNames_ofProtectedAtom {n : ℕ} (atom : ProtectedAtom n) : (ofProtectedAtom atom).extractedNames = atom.names

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.AllClassified.of_isRotated {n : ℕ} {tokens target : List (ReductionToken n)} (classified : AllClassified tokens) (rotated : tokens ~r target) : AllClassified target

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.AllClassified.of_perm {n : ℕ} {tokens target : List (ReductionToken n)} (classified : AllClassified tokens) (permuted : tokens.Perm target) : AllClassified target

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.AllClassified.of_append_left {n : ℕ} {left right : List (ReductionToken n)} (classified : AllClassified (left ++ right)) : AllClassified left

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.AllClassified.of_append_right {n : ℕ} {left right : List (ReductionToken n)} (classified : AllClassified (left ++ right)) : AllClassified right

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.AllClassified.append {n : ℕ} {left right : List (ReductionToken n)} (leftClassified : AllClassified left) (rightClassified : AllClassified right) : AllClassified (left ++ right)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.allClassified_cons {n : ℕ} (token : ReductionToken n) (tokens : List (ReductionToken n)) : AllClassified (token :: tokens) ↔ token.IsClassified ∧ AllClassified tokens

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.inverse {n : ℕ} : ReductionToken n → ReductionToken n

Reverse a token while preserving an extracted block as one atomic token.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.mapEquiv {n m : ℕ} (e : Fin n ≃ Fin m) : ReductionToken n → ReductionToken m

Relabel every edge name represented by a marked token.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.inverse_ofProtectedAtom {n : ℕ} (atom : ProtectedAtom n) : (ofProtectedAtom atom).inverse = ofProtectedAtom atom.inverse

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.IsClassified.inverse {n : ℕ} {token : ReductionToken n} (classified : token.IsClassified) : token.inverse.IsClassified

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.IsClassified.mapEquiv {n m : ℕ} {token : ReductionToken n} (classified : token.IsClassified) (e : Fin n ≃ Fin m) : (ReductionToken.mapEquiv e token).IsClassified

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.word_inverse {n : ℕ} (token : ReductionToken n) : token.inverse.word = inverseWord token.word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualWord_inverse {n : ℕ} (token : ReductionToken n) : token.inverse.residualWord = inverseWord token.residualWord

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extractedEdges_inverse {n : ℕ} (token : ReductionToken n) : token.inverse.extractedEdges = token.extractedEdges.reverse

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extractedNames_inverse_perm {n : ℕ} (token : ReductionToken n) : token.inverse.extractedNames.Perm token.extractedNames

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.inverse_inverse {n : ℕ} (token : ReductionToken n) : token.inverse.inverse = token

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.word_mapEquiv {n m : ℕ} (e : Fin n ≃ Fin m) (token : ReductionToken n) : (mapEquiv e token).word = List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv e)) token.word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualWord_mapEquiv {n m : ℕ} (e : Fin n ≃ Fin m) (token : ReductionToken n) : (mapEquiv e token).residualWord = List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv e)) token.residualWord

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.inverse_mapEquiv {n m : ℕ} (e : Fin n ≃ Fin m) (token : ReductionToken n) : (mapEquiv e token).inverse = mapEquiv e token.inverse

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.lowerAvoiding {n : ℕ} (a : Fin (n + 1)) (token : ReductionToken (n + 1)) (ha : a ∉ List.map edgeOfDart token.word) : ReductionToken n

Lower a marked token known not to use the removed ambient edge.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.lowerAvoiding_residual_dart {n : ℕ} (a e : Fin (n + 1)) (negative : Bool) (ha : a ∉ List.map edgeOfDart (residual (dart e negative)).word) : lowerAvoiding a (residual (dart e negative)) ha = residual (dart (Cancellation.lowerEdge a e ⋯) negative)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.word_lowerAvoiding {n : ℕ} (a : Fin (n + 1)) (token : ReductionToken (n + 1)) (ha : a ∉ List.map edgeOfDart token.word) : (lowerAvoiding a token ha).word = Cancellation.lowerTail a token.word

Lowering one marked token agrees with word-level cancellation lowering.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.IsClassified.lowerAvoiding {n : ℕ} (a : Fin (n + 1)) {token : ReductionToken (n + 1)} (classified : token.IsClassified) (ha : a ∉ List.map edgeOfDart token.word) : (ReductionToken.lowerAvoiding a token ha).IsClassified

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualEdges_lowerAvoiding_map_restoreEdge {n : ℕ} (a : Fin (n + 1)) (token : ReductionToken (n + 1)) (ha : a ∉ List.map edgeOfDart token.word) : List.map (Cancellation.restoreEdge a) (List.map edgeOfDart (lowerAvoiding a token ha).residualWord) = List.map edgeOfDart token.residualWord

Re-embedding residual edge names after lowering one token recovers the old residual names.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extractedEdges_lowerAvoiding_map_restoreEdge {n : ℕ} (a : Fin (n + 1)) (token : ReductionToken (n + 1)) (ha : a ∉ List.map edgeOfDart token.word) : List.map (Cancellation.restoreEdge a) (lowerAvoiding a token ha).extractedEdges = token.extractedEdges

Re-embedding protected edge names after lowering one token recovers the old protected names.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.extractedNames_lowerAvoiding_map_restoreEdge {n : ℕ} (a : Fin (n + 1)) (token : ReductionToken (n + 1)) (ha : a ∉ List.map edgeOfDart token.word) : List.map (Cancellation.restoreEdge a) (lowerAvoiding a token ha).extractedNames = token.extractedNames

Re-embedding a lowered token's distinct protected names recovers its old name spine.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.expand {n : ℕ} (tokens : List (ReductionToken n)) : List (SurfaceCellComplex.SignedDart (Fin n))

Expand a marked word to the exact signed word on which normalization moves act.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualDarts {n : ℕ} (tokens : List (ReductionToken n)) : List (SurfaceCellComplex.SignedDart (Fin n))

Erase extracted blocks and retain only the darts still available to pairing reduction.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedEdges {n : ℕ} (tokens : List (ReductionToken n)) : List (Fin n)

All edge names protected inside extracted block tokens.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedNames {n : ℕ} (tokens : List (ReductionToken n)) : List (Fin n)

Distinct-name spine of all protected tokens. Each token contributes each of its edge names once, so global Nodup expresses disjoint ownership of protected names.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.IsSeparated {n : ℕ} (tokens : List (ReductionToken n)) : Prop

Residual darts and already-extracted blocks use disjoint ambient edge names.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.inverseSequence {n : ℕ} (tokens : List (ReductionToken n)) : List (ReductionToken n)

Reverse a marked word at token granularity.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.rawBoundaryCount_inverseSequence {n : ℕ} (tokens : List (ReductionToken n)) : rawBoundaryCount (inverseSequence tokens) = rawBoundaryCount tokens

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.ofWord {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : List (ReductionToken n)

Initially every dart is still residual.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.ofBlocks {n : ℕ} (blocks : List (ExtractedBlock n)) : List (ReductionToken n)

A finished marked word contains only extracted block tokens.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.allClassified_ofWord {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : AllClassified (ofWord word)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.AllClassified.inverseSequence {n : ℕ} {tokens : List (ReductionToken n)} (classified : AllClassified tokens) : AllClassified (ReductionToken.inverseSequence tokens)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.expand_nil {n : ℕ} : expand [] = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.expand_cons {n : ℕ} (token : ReductionToken n) (tokens : List (ReductionToken n)) : expand (token :: tokens) = token.word ++ expand tokens

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.expand_append {n : ℕ} (left right : List (ReductionToken n)) : expand (left ++ right) = expand left ++ expand right

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.expand_map_ofProtectedAtom {n : ℕ} (atoms : List (ProtectedAtom n)) : expand (List.map ofProtectedAtom atoms) = ProtectedAtom.sequenceWord atoms

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualDarts_nil {n : ℕ} : residualDarts [] = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualDarts_cons {n : ℕ} (token : ReductionToken n) (tokens : List (ReductionToken n)) : residualDarts (token :: tokens) = token.residualWord ++ residualDarts tokens

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualDarts_append {n : ℕ} (left right : List (ReductionToken n)) : residualDarts (left ++ right) = residualDarts left ++ residualDarts right

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.exists_eq_map_ofProtectedAtom_of_allClassified_of_residualDarts_eq_nil {n : ℕ} (tokens : List (ReductionToken n)) (classified : AllClassified tokens) (residual_nil : residualDarts tokens = []) : ∃ (atoms : List (ProtectedAtom n)), tokens = List.map ofProtectedAtom atoms

A classified token list with no residual darts is exactly a list of typed protected atoms.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.terminalAtoms {n : ℕ} (tokens : List (ReductionToken n)) (classified : AllClassified tokens) (residual_nil : residualDarts tokens = []) : List (ProtectedAtom n)

Canonical atom-level view of a classified marked word whose residual contribution is empty.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.terminalAtoms tokens classified residual_nil = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.eq_map_terminalAtoms {n : ℕ} (tokens : List (ReductionToken n)) (classified : AllClassified tokens) (residual_nil : residualDarts tokens = []) : tokens = List.map ofProtectedAtom (terminalAtoms tokens classified residual_nil)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.expand_eq_sequenceWord_terminalAtoms {n : ℕ} (tokens : List (ReductionToken n)) (classified : AllClassified tokens) (residual_nil : residualDarts tokens = []) : expand tokens = ProtectedAtom.sequenceWord (terminalAtoms tokens classified residual_nil)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.terminalAtoms_ne_nil_of_protectedNames_ne_nil {n : ℕ} (tokens : List (ReductionToken n)) (classified : AllClassified tokens) (residual_nil : residualDarts tokens = []) (protected_nonempty : protectedNames tokens ≠ []) : terminalAtoms tokens classified residual_nil ≠ []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedNames_map_ofProtectedAtom {n : ℕ} (atoms : List (ProtectedAtom n)) : protectedNames (List.map ofProtectedAtom atoms) = ProtectedAtom.sequenceNames atoms

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedEdges_nil {n : ℕ} : protectedEdges [] = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedEdges_cons {n : ℕ} (token : ReductionToken n) (tokens : List (ReductionToken n)) : protectedEdges (token :: tokens) = token.extractedEdges ++ protectedEdges tokens

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedEdges_append {n : ℕ} (left right : List (ReductionToken n)) : protectedEdges (left ++ right) = protectedEdges left ++ protectedEdges right

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedNames_nil {n : ℕ} : protectedNames [] = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedNames_cons {n : ℕ} (token : ReductionToken n) (tokens : List (ReductionToken n)) : protectedNames (token :: tokens) = token.extractedNames ++ protectedNames tokens

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedNames_append {n : ℕ} (left right : List (ReductionToken n)) : protectedNames (left ++ right) = protectedNames left ++ protectedNames right

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.mem_protectedNames_iff_mem_protectedEdges {n : ℕ} (tokens : List (ReductionToken n)) (a : Fin n) : a ∈ protectedNames tokens ↔ a ∈ protectedEdges tokens

The distinct-name spine and occurrence-level protected list have identical membership.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.Cancellation.lowerTail_append {n : ℕ} (a : Fin (n + 1)) (left right : List (SurfaceCellComplex.SignedDart (Fin (n + 1)))) : Cancellation.lowerTail a (left ++ right) = Cancellation.lowerTail a left ++ Cancellation.lowerTail a right

Cancellation lowering distributes over concatenation.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.lowerTokensAvoiding {n : ℕ} (a : Fin (n + 1)) (tokens : List (ReductionToken (n + 1))) : a ∉ List.map edgeOfDart (expand tokens) → List (ReductionToken n)

Lower every token in a marked word which avoids the removed edge.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.lowerTokensAvoiding a [] x_2 = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.rawBoundaryCount_lowerTokensAvoiding {n : ℕ} (a : Fin (n + 1)) (tokens : List (ReductionToken (n + 1))) (ha : a ∉ List.map edgeOfDart (expand tokens)) : rawBoundaryCount (lowerTokensAvoiding a tokens ha) = rawBoundaryCount tokens

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.lowerTokensAvoiding_append {n : ℕ} (a : Fin (n + 1)) (left right : List (ReductionToken (n + 1))) (ha : a ∉ List.map edgeOfDart (expand (left ++ right))) : lowerTokensAvoiding a (left ++ right) ha = lowerTokensAvoiding a left ⋯ ++ lowerTokensAvoiding a right ⋯

Marked cancellation lowering distributes over token concatenation.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.length_lowerTokensAvoiding {n : ℕ} (a : Fin (n + 1)) (tokens : List (ReductionToken (n + 1))) (ha : a ∉ List.map edgeOfDart (expand tokens)) : (lowerTokensAvoiding a tokens ha).length = tokens.length

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.AllClassified.lowerTokensAvoiding {n : ℕ} (a : Fin (n + 1)) (tokens : List (ReductionToken (n + 1))) (classified : AllClassified tokens) (ha : a ∉ List.map edgeOfDart (expand tokens)) : AllClassified (ReductionToken.lowerTokensAvoiding a tokens ha)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.expand_lowerTokensAvoiding {n : ℕ} (a : Fin (n + 1)) (tokens : List (ReductionToken (n + 1))) (ha : a ∉ List.map edgeOfDart (expand tokens)) : expand (lowerTokensAvoiding a tokens ha) = Cancellation.lowerTail a (expand tokens)

Expanding a lowered marked word gives exactly the ordinary cancellation target word.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualEdges_lowerTokensAvoiding_map_restoreEdge {n : ℕ} (a : Fin (n + 1)) (tokens : List (ReductionToken (n + 1))) (ha : a ∉ List.map edgeOfDart (expand tokens)) : List.map (Cancellation.restoreEdge a) (List.map edgeOfDart (residualDarts (lowerTokensAvoiding a tokens ha))) = List.map edgeOfDart (residualDarts tokens)

Re-embedding all residual edge names after lowering a marked word recovers the source residual namespace exactly.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualDarts_length_lowerTokensAvoiding {n : ℕ} (a : Fin (n + 1)) (tokens : List (ReductionToken (n + 1))) (ha : a ∉ List.map edgeOfDart (expand tokens)) : (residualDarts (lowerTokensAvoiding a tokens ha)).length = (residualDarts tokens).length

Lowering an absent ambient edge preserves the number of residual darts.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedEdges_lowerTokensAvoiding_map_restoreEdge {n : ℕ} (a : Fin (n + 1)) (tokens : List (ReductionToken (n + 1))) (ha : a ∉ List.map edgeOfDart (expand tokens)) : List.map (Cancellation.restoreEdge a) (protectedEdges (lowerTokensAvoiding a tokens ha)) = protectedEdges tokens

Re-embedding all protected edge names after lowering a marked word recovers the source protected namespace exactly.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedNames_lowerTokensAvoiding_map_restoreEdge {n : ℕ} (a : Fin (n + 1)) (tokens : List (ReductionToken (n + 1))) (ha : a ∉ List.map edgeOfDart (expand tokens)) : List.map (Cancellation.restoreEdge a) (protectedNames (lowerTokensAvoiding a tokens ha)) = protectedNames tokens

Re-embedding all distinct protected names after lowering recovers the source name spine.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.IsSeparated.lowerTokensAvoiding {n : ℕ} (a : Fin (n + 1)) (tokens : List (ReductionToken (n + 1))) (ha : a ∉ List.map edgeOfDart (expand tokens)) (separated : IsSeparated tokens) : IsSeparated (ReductionToken.lowerTokensAvoiding a tokens ha)

Injective cancellation lowering preserves separation of residual and protected names.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.mem_map_edgeOfDart_expand_iff {n : ℕ} (tokens : List (ReductionToken n)) (a : Fin n) : a ∈ List.map edgeOfDart (expand tokens) ↔ a ∈ List.map edgeOfDart (residualDarts tokens) ∨ a ∈ protectedEdges tokens

An edge occurs in the expanded word exactly when it is residual or protected in an extracted block token.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.count_map_edgeOfDart_word_eq_residualWord_of_not_mem_extractedEdges {n : ℕ} (token : ReductionToken n) (a : Fin n) (ha : a ∉ token.extractedEdges) : List.count a (List.map edgeOfDart token.word) = List.count a (List.map edgeOfDart token.residualWord)

A name absent from a token's protected part has the same multiplicity in its exact word and its residual contribution.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.count_map_edgeOfDart_expand_eq_residualDarts_of_not_mem_protectedEdges {n : ℕ} (tokens : List (ReductionToken n)) (a : Fin n) (ha : a ∉ protectedEdges tokens) : List.count a (List.map edgeOfDart (expand tokens)) = List.count a (List.map edgeOfDart (residualDarts tokens))

A name absent from every protected token has the same multiplicity in the expanded word and the erased residual word.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.isRotated_flatten {α : Type u_1} {lists target : List (List α)} (hrotated : lists ~r target) : lists.flatten ~r target.flatten

Flattening preserves a cyclic rotation of a list of lists.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.expand_isRotated {n : ℕ} {tokens target : List (ReductionToken n)} (hrotated : tokens ~r target) : expand tokens ~r expand target

Expanding atomic marked tokens preserves cyclic rotation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedEdges_isRotated {n : ℕ} {tokens target : List (ReductionToken n)} (hrotated : tokens ~r target) : protectedEdges tokens ~r protectedEdges target

Protected edge names rotate with their atomic marked tokens.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedNames_isRotated {n : ℕ} {tokens target : List (ReductionToken n)} (hrotated : tokens ~r target) : protectedNames tokens ~r protectedNames target

Distinct protected-name spines rotate with their atomic marked tokens.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualEdges_isRotated {n : ℕ} {tokens target : List (ReductionToken n)} (hrotated : tokens ~r target) : List.map edgeOfDart (residualDarts tokens) ~r List.map edgeOfDart (residualDarts target)

Residual edge names rotate with their atomic marked tokens.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.IsSeparated.of_isRotated {n : ℕ} {tokens target : List (ReductionToken n)} (separated : IsSeparated tokens) (hrotated : tokens ~r target) : IsSeparated target

Separation of residual and protected edge names is invariant under cyclic rotation.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.IsSeparated.of_perm {n : ℕ} {tokens target : List (ReductionToken n)} (separated : IsSeparated tokens) (permuted : tokens.Perm target) : IsSeparated target

Separation depends only on the multiset of atomic marked tokens.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedNames_perm {n : ℕ} {tokens target : List (ReductionToken n)} (permuted : tokens.Perm target) : (protectedNames tokens).Perm (protectedNames target)

Permuting atomic marked tokens permutes their distinct protected-name spines.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedNames_nodup_of_perm {n : ℕ} {tokens target : List (ReductionToken n)} (nodup : (protectedNames tokens).Nodup) (permuted : tokens.Perm target) : (protectedNames target).Nodup

Duplicate-freeness of protected names depends only on the multiset of marked tokens.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedNames_ne_nil_of_perm {n : ℕ} {tokens target : List (ReductionToken n)} (hne : protectedNames tokens ≠ []) (permuted : tokens.Perm target) : protectedNames target ≠ []

Permuting marked tokens preserves nonemptiness of the protected-name spine.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualDarts_length_of_perm {n : ℕ} {tokens target : List (ReductionToken n)} (permuted : tokens.Perm target) : (residualDarts target).length = (residualDarts tokens).length

Permuting atomic marked tokens preserves the number of residual darts.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedNames_nodup_lowerTokensAvoiding {n : ℕ} (a : Fin (n + 1)) (tokens : List (ReductionToken (n + 1))) (ha : a ∉ List.map edgeOfDart (expand tokens)) (nodup : (protectedNames tokens).Nodup) : (protectedNames (lowerTokensAvoiding a tokens ha)).Nodup

Lowering an absent ambient edge preserves duplicate-freeness of all protected names.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.IsSeparated.not_mem_protected_of_mem_residual {n : ℕ} {tokens : List (ReductionToken n)} (separated : IsSeparated tokens) (a : Fin n) (ha : a ∈ List.map edgeOfDart (residualDarts tokens)) : a ∉ protectedEdges tokens

A separated marked word cannot protect an edge that still occurs residually.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.expand_ofWord {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : expand (ofWord word) = word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualDarts_ofWord {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : residualDarts (ofWord word) = word

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedEdges_ofWord {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : protectedEdges (ofWord word) = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedNames_ofWord {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) : protectedNames (ofWord word) = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.expand_ofBlocks {n : ℕ} (blocks : List (ExtractedBlock n)) : expand (ofBlocks blocks) = ExtractedBlock.sequenceWord blocks

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualDarts_ofBlocks {n : ℕ} (blocks : List (ExtractedBlock n)) : residualDarts (ofBlocks blocks) = []

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.exists_split_of_residualDarts_eq_append_cons {n : ℕ} (tokens : List (ReductionToken n)) (left right : List (SurfaceCellComplex.SignedDart (Fin n))) (dart : SurfaceCellComplex.SignedDart (Fin n)) (hresidual : residualDarts tokens = left ++ dart :: right) : ∃ (tokenLeft : List (ReductionToken n)) (tokenRight : List (ReductionToken n)), tokens = tokenLeft ++ residual dart :: tokenRight ∧ residualDarts tokenLeft = left ∧ residualDarts tokenRight = right

Lift a displayed residual dart occurrence to an exact split of the marked token list.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.exists_split_of_residualDarts_eq_append {n : ℕ} (tokens : List (ReductionToken n)) (left right : List (SurfaceCellComplex.SignedDart (Fin n))) (hresidual : residualDarts tokens = left ++ right) : ∃ (tokenLeft : List (ReductionToken n)) (tokenRight : List (ReductionToken n)), tokens = tokenLeft ++ tokenRight ∧ residualDarts tokenLeft = left ∧ residualDarts tokenRight = right

Lift an arbitrary residual-word cut to a cut of the marked token list.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.exists_isRotated_of_residualDarts_isRotated {n : ℕ} (tokens : List (ReductionToken n)) {target : List (SurfaceCellComplex.SignedDart (Fin n))} (hrotated : residualDarts tokens ~r target) : ∃ (rotatedTokens : List (ReductionToken n)), tokens ~r rotatedTokens ∧ residualDarts rotatedTokens = target

Every cyclic rotation of the residual darts is induced by a cyclic rotation of the marked tokens.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.exists_isRotated_residual_cons {n : ℕ} (tokens : List (ReductionToken n)) (dart : SurfaceCellComplex.SignedDart (Fin n)) (remainder : List (SurfaceCellComplex.SignedDart (Fin n))) (hrotated : residualDarts tokens ~r dart :: remainder) : ∃ (tokenRemainder : List (ReductionToken n)), tokens ~r residual dart :: tokenRemainder ∧ residualDarts tokenRemainder = remainder

Lift a residual rotation which displays one dart at its head to a marked-token rotation with that exact residual token at its head.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.ResidualSplit {n : ℕ} (tokens : List (ReductionToken n)) (left right : List (SurfaceCellComplex.SignedDart (Fin n))) : Type

Type-valued packaging of a marked split, suitable for recursive normalization data.

• tokenLeft : List (ReductionToken n)

  The tokenLeft declaration.

• tokenRight : List (ReductionToken n)

  The tokenRight declaration.

• tokens_eq : tokens = self.tokenLeft ++ self.tokenRight
• residual_left : residualDarts self.tokenLeft = left
• residual_right : residualDarts self.tokenRight = right

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.ResidualDartSplit {n : ℕ} (tokens : List (ReductionToken n)) (left right : List (SurfaceCellComplex.SignedDart (Fin n))) (dart : SurfaceCellComplex.SignedDart (Fin n)) : Type

Type-valued packaging of a marked split at one displayed residual dart.

• tokenLeft : List (ReductionToken n)

  The tokenLeft declaration.

• tokenRight : List (ReductionToken n)

  The tokenRight declaration.

• tokens_eq : tokens = self.tokenLeft ++ residual dart :: self.tokenRight
• residual_left : residualDarts self.tokenLeft = left
• residual_right : residualDarts self.tokenRight = right

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualSplit {n : ℕ} (tokens : List (ReductionToken n)) (left right : List (SurfaceCellComplex.SignedDart (Fin n))) (hresidual : residualDarts tokens = left ++ right) : ResidualSplit tokens left right

Choose a marked split above a displayed residual-word split.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualDartSplit {n : ℕ} (tokens : List (ReductionToken n)) (left right : List (SurfaceCellComplex.SignedDart (Fin n))) (dart : SurfaceCellComplex.SignedDart (Fin n)) (hresidual : residualDarts tokens = left ++ dart :: right) : ResidualDartSplit tokens left right dart

Choose a marked split at a displayed residual dart.

Equations

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

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.ResidualConsRotation {n : ℕ} (tokens : List (ReductionToken n)) (dart : SurfaceCellComplex.SignedDart (Fin n)) (remainder : List (SurfaceCellComplex.SignedDart (Fin n))) : Type

Type-valued packaging of a marked rotation with one residual dart at its head.

• tokenRemainder : List (ReductionToken n)

  The tokenRemainder declaration.

• rotated : tokens ~r residual dart :: self.tokenRemainder
• residual_remainder : residualDarts self.tokenRemainder = remainder

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualConsRotation {n : ℕ} (tokens : List (ReductionToken n)) (dart : SurfaceCellComplex.SignedDart (Fin n)) (remainder : List (SurfaceCellComplex.SignedDart (Fin n))) (hrotated : residualDarts tokens ~r dart :: remainder) : ResidualConsRotation tokens dart remainder

Choose the marked rotation above a residual rotation with one displayed head dart.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.expand_inverseSequence {n : ℕ} (tokens : List (ReductionToken n)) : expand (inverseSequence tokens) = inverseWord (expand tokens)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualDarts_inverseSequence {n : ℕ} (tokens : List (ReductionToken n)) : residualDarts (inverseSequence tokens) = inverseWord (residualDarts tokens)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedEdges_inverseSequence {n : ℕ} (tokens : List (ReductionToken n)) : protectedEdges (inverseSequence tokens) = (protectedEdges tokens).reverse

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.protectedNames_inverseSequence_perm {n : ℕ} (tokens : List (ReductionToken n)) : (protectedNames (inverseSequence tokens)).Perm (protectedNames tokens)

Reversing a marked token sequence preserves its multiset of distinct protected names.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.expand_mapEquiv {n m : ℕ} (e : Fin n ≃ Fin m) (tokens : List (ReductionToken n)) : expand (List.map (mapEquiv e) tokens) = List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv e)) (expand tokens)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.residualDarts_mapEquiv {n m : ℕ} (e : Fin n ≃ Fin m) (tokens : List (ReductionToken n)) : residualDarts (List.map (mapEquiv e) tokens) = List.map (⇑(SurfaceCellComplex.SignedDart.mapEquiv e)) (residualDarts tokens)