Marked finite cyclic word reduction

This file completes the recursive reduction developed in FiniteCyclicWordReductionCore, carrying the marked normalization state through terminal block normalization and the connected-presentation result.

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

Invariants carried by every marked normalization state. Protected-name uniqueness is stated on name spines rather than dart-occurrence lists, so completed boundary carriers are counted once.

• valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid
• separated : ReductionToken.IsSeparated tokens
• classified : ReductionToken.AllClassified tokens
• protectedNodup : (ReductionToken.protectedNames tokens).Nodup

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

The all-residual marking of a valid word satisfies every execution invariant.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedExecutionState.hasValidUsedMultiplicities_residualDarts {n : ℕ} {tokens : List (ReductionToken n)} (state : MarkedExecutionState tokens) : HasValidUsedMultiplicities (ReductionToken.residualDarts tokens)

Surface multiplicities restrict to the erased residual word because separation rules out any residual name from all protected blocks.

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

Forget an actionable feature's occurrence decomposition while retaining its extracted block.

Equations

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

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

The edge names consumed by an actionable extraction.

Equations

• feature.extractedEdges = feature.block.edges

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionFeature.extractedEdges_ne_nil {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (feature : ActionablePairReductionFeature word) : feature.extractedEdges ≠ []

Every actionable feature consumes at least one edge name.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionFeature.extractedEdges_nodup {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (feature : ActionablePairReductionFeature word) : feature.extractedEdges.Nodup

The edge names inside one extracted block are distinct.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionFeature.extractedEdges_disjoint_residualWord {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (feature : ActionablePairReductionFeature word) : feature.extractedEdges.Disjoint (List.map edgeOfDart feature.residualWord)

No edge consumed by a feature remains in its residual word.

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

Every name consumed by a feature occurs in its source word.

inductive LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedActionablePairReductionFeature {n : ℕ} (tokens : List (ReductionToken n)) : Type

An actionable residual feature lifted to a marked word. Extracted blocks occupy whole token segments between the distinguished residual darts, so later rewrites can reorder or reverse those segments without splitting a protected block.

• boundary {n : ℕ} {tokens : List (ReductionToken n)} (a : Fin n) (form : BoundaryOccurrenceForm (ReductionToken.residualDarts tokens) a) (remainderTokens : List (ReductionToken n)) (rotated : tokens ~r ReductionToken.residual (dart a form.negative) :: remainderTokens) (residual_remainder : ReductionToken.residualDarts remainderTokens = form.remainder) : MarkedActionablePairReductionFeature tokens
• crosscap {n : ℕ} {tokens : List (ReductionToken n)} (a : Fin n) (form : CrosscapOccurrenceForm (ReductionToken.residualDarts tokens) a) (betweenTokens remainderTokens : List (ReductionToken n)) (rotated : tokens ~r ReductionToken.residual (dart a form.negative) :: betweenTokens ++ ReductionToken.residual (dart a form.negative) :: remainderTokens) (residual_between : ReductionToken.residualDarts betweenTokens = form.between) (residual_remainder : ReductionToken.residualDarts remainderTokens = form.remainder) : MarkedActionablePairReductionFeature tokens
• handle {n : ℕ} {tokens : List (ReductionToken n)} (a b : Fin n) (form : InterleavedOccurrenceForm (ReductionToken.residualDarts tokens) a b) (beforeBTokens beforeNegATokens beforeOutsideBTokens remainderTokens : List (ReductionToken n)) (rotated : tokens ~r ReductionToken.residual (SurfaceCellComplex.SignedDart.pos a) :: beforeBTokens ++ ReductionToken.residual (dart b form.bNegativeInside) :: beforeNegATokens ++ ReductionToken.residual (SurfaceCellComplex.SignedDart.neg a) :: beforeOutsideBTokens ++ ReductionToken.residual (dart b !form.bNegativeInside) :: remainderTokens) (residual_beforeB : ReductionToken.residualDarts beforeBTokens = form.beforeB) (residual_beforeNegA : ReductionToken.residualDarts beforeNegATokens = form.beforeNegA) (residual_beforeOutsideB : ReductionToken.residualDarts beforeOutsideBTokens = form.beforeOutsideB) (residual_remainder : ReductionToken.residualDarts remainderTokens = form.remainder) : MarkedActionablePairReductionFeature tokens

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedActionablePairReductionFeature.residualFeature {n : ℕ} {tokens : List (ReductionToken n)} : MarkedActionablePairReductionFeature tokens → ActionablePairReductionFeature (ReductionToken.residualDarts tokens)

Residual feature underlying a marked feature.

Equations

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

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

Marked target: replace the distinguished residual darts by one atomic extracted block while performing the same segment reversal/reordering as the local Gallier--Xu rewrite.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedActionablePairReductionFeature.lift {n : ℕ} {tokens : List (ReductionToken n)} (feature : ActionablePairReductionFeature (ReductionToken.residualDarts tokens)) : MarkedActionablePairReductionFeature tokens

Lift an actionable feature of the erased residual word to the marked token word.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedActionablePairReductionFeature.residualDarts_targetTokens {n : ℕ} {tokens : List (ReductionToken n)} (marked : MarkedActionablePairReductionFeature tokens) : ReductionToken.residualDarts marked.targetTokens = marked.residualFeature.residualWord

Erasing the marked target recovers exactly the residual word of the underlying feature.

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

Marked extraction preserves the classified-token grammar.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedActionablePairReductionFeature.mem_protectedEdges_targetTokens_iff {n : ℕ} {tokens : List (ReductionToken n)} (marked : MarkedActionablePairReductionFeature tokens) (e : Fin n) : e ∈ ReductionToken.protectedEdges marked.targetTokens ↔ e ∈ marked.residualFeature.extractedEdges ∨ e ∈ ReductionToken.protectedEdges tokens

The protected names after one marked extraction are precisely the newly extracted names together with the previously protected names.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedActionablePairReductionFeature.protectedNames_targetTokens_perm {n : ℕ} {tokens : List (ReductionToken n)} (marked : MarkedActionablePairReductionFeature tokens) : (ReductionToken.protectedNames marked.targetTokens).Perm (marked.residualFeature.extractedEdges ++ ReductionToken.protectedNames tokens)

A marked extraction prepends exactly its newly consumed names and otherwise only permutes the existing protected-name spine.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedActionablePairReductionFeature.protectedNames_targetTokens_ne_nil {n : ℕ} {tokens : List (ReductionToken n)} (marked : MarkedActionablePairReductionFeature tokens) : ReductionToken.protectedNames marked.targetTokens ≠ []

Every marked extraction creates at least one protected name.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedActionablePairReductionFeature.targetTokens_protectedNames_nodup {n : ℕ} {tokens : List (ReductionToken n)} (marked : MarkedActionablePairReductionFeature tokens) (separated : ReductionToken.IsSeparated tokens) (nodup : (ReductionToken.protectedNames tokens).Nodup) : (ReductionToken.protectedNames marked.targetTokens).Nodup

Extraction preserves global ownership uniqueness of protected names.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedActionablePairReductionFeature.targetTokens_isSeparated {n : ℕ} {tokens : List (ReductionToken n)} (marked : MarkedActionablePairReductionFeature tokens) (separated : ReductionToken.IsSeparated tokens) : ReductionToken.IsSeparated marked.targetTokens

Marked extraction preserves separation of residual and protected edge namespaces.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedActionablePairReductionFeature.expandedFeature {n : ℕ} {tokens : List (ReductionToken n)} (marked : MarkedActionablePairReductionFeature tokens) (separated : ReductionToken.IsSeparated tokens) : ActionablePairReductionFeature (ReductionToken.expand tokens)

Expanding a separated marked feature gives the genuine feature on the full signed word. The separation invariant is exactly what rules out a selected residual edge from every protected block lying in an intervening token segment.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedActionablePairReductionFeature.expandedFeature_block_word_append_residualWord {n : ℕ} {tokens : List (ReductionToken n)} (marked : MarkedActionablePairReductionFeature tokens) (separated : ReductionToken.IsSeparated tokens) : (marked.expandedFeature separated).block.word ++ (marked.expandedFeature separated).residualWord = ReductionToken.expand marked.targetTokens

The full-word extraction target is exactly the expansion of the marked target.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedCancellablePair {n : ℕ} (tokens : List (ReductionToken (n + 1))) : Type

An inverse pair which is adjacent at marked-token granularity. Unlike adjacency only after erasing protected blocks, this is immediately executable by the ordinary cancellation chain.

• edge : Fin (n + 1)

  The edge declaration.

• negativeFirst : Bool

  The negativeFirst declaration.

• tailTokens : List (ReductionToken (n + 1))

  The tailTokens declaration.

• rotated : tokens ~r ReductionToken.residual (dart self.edge self.negativeFirst) :: ReductionToken.residual (dart self.edge !self.negativeFirst) :: self.tailTokens

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedCancellablePair.expandedPair {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedCancellablePair tokens) : CancellablePair (ReductionToken.expand tokens)

Expanding a token-adjacent pair gives an ordinary cancellable pair on the full word.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedCancellablePair.edge_not_mem_tailTokens {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedCancellablePair tokens) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : pair.edge ∉ List.map edgeOfDart (ReductionToken.expand pair.tailTokens)

Validity ensures that the removed edge is absent from every remaining marked token.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedCancellablePair.tailTokens_isSeparated {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedCancellablePair tokens) (separated : ReductionToken.IsSeparated tokens) : ReductionToken.IsSeparated pair.tailTokens

Separation of residual and protected names passes to the marked tail after deleting the displayed residual pair.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedCancellablePair.tailTokens_protectedNames_nodup {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedCancellablePair tokens) (nodup : (ReductionToken.protectedNames tokens).Nodup) : (ReductionToken.protectedNames pair.tailTokens).Nodup

Removing a displayed residual pair leaves the protected-name spine unchanged up to rotation.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair {n : ℕ} (tokens : List (ReductionToken n)) : Type

A cancellable pair of the erased residual word lifted to its exact marked-token interval. The intervening tokens have empty residual contribution but may contain protected blocks.

• edge : Fin n

  The edge declaration.

• negativeFirst : Bool

  The negativeFirst declaration.

• betweenTokens : List (ReductionToken n)

  The betweenTokens declaration.

• tailTokens : List (ReductionToken n)

  The tailTokens declaration.

• rotated : tokens ~r ReductionToken.residual (dart self.edge self.negativeFirst) :: self.betweenTokens ++ ReductionToken.residual (dart self.edge !self.negativeFirst) :: self.tailTokens
• residual_between : ReductionToken.residualDarts self.betweenTokens = []

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.lift {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : CancellablePair (ReductionToken.residualDarts tokens)) : MarkedResidualCancellablePair tokens

Lift an ordinary cancellable pair of the erased residual word to marked-token data.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.toAdjacent {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (hempty : pair.betweenTokens = []) : MarkedCancellablePair tokens

When no protected token intervenes, a lifted residual pair is directly cancellable.

Equations

• pair.toAdjacent hempty = { edge := pair.edge, negativeFirst := pair.negativeFirst, tailTokens := pair.tailTokens, rotated := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.edge_not_mem_between_and_tail {n : ℕ} {tokens : List (ReductionToken n)} (pair : MarkedResidualCancellablePair tokens) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : pair.edge ∉ List.map edgeOfDart (ReductionToken.expand pair.betweenTokens) ∧ pair.edge ∉ List.map edgeOfDart (ReductionToken.expand pair.tailTokens)

Surface multiplicity ensures that a lifted pair's carrier occurs nowhere in its protected interval or remaining marked tail.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.residualDarts_length_eq {n : ℕ} {tokens : List (ReductionToken n)} (pair : MarkedResidualCancellablePair tokens) : (ReductionToken.residualDarts tokens).length = 2 + (ReductionToken.residualDarts pair.tailTokens).length

A lifted inverse pair contributes exactly two residual darts beyond its marked tail.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryClosure {n : ℕ} (tokens : List (ReductionToken n)) : Type

A residual inverse pair surrounding one extracted boundary singleton. Reclassifying the three-token succession as one completed boundary block closes the singleton into the canonical loop shape without changing the expanded cyclic presentation.

• carrier : Fin n

  The carrier declaration.

• hole : Fin n

  The hole declaration.

• carrierNegative : Bool

  The carrierNegative declaration.

• holeNegative : Bool

  The holeNegative declaration.

• tailTokens : List (ReductionToken n)

  The tailTokens declaration.

• rotated : tokens ~r ReductionToken.residual (dart self.carrier self.carrierNegative) :: ReductionToken.extracted (ExtractedBlock.boundary self.hole self.holeNegative) :: ReductionToken.residual (dart self.carrier !self.carrierNegative) :: self.tailTokens

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

Exact three-dart spelling of the closed boundary loop.

Equations

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

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

Marked target obtained by replacing the displayed succession with one atomic protected word.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryClosure.expand_isRotated_target {n : ℕ} {tokens : List (ReductionToken n)} (closure : MarkedBoundaryClosure tokens) : ReductionToken.expand tokens ~r ReductionToken.expand closure.targetTokens

The source expansion is a cyclic rotation of the exact boundary-closure target expansion.

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

Boundary closure preserves the classified-token grammar.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryClosure.carrier_not_mem_tail {n : ℕ} {tokens : List (ReductionToken n)} (closure : MarkedBoundaryClosure tokens) (separated : ReductionToken.IsSeparated tokens) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : closure.carrier ∉ List.map edgeOfDart (ReductionToken.expand closure.tailTokens)

Surface multiplicity forces the loop carrier to be absent from the remaining marked tail.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryClosure.targetTokens_isSeparated {n : ℕ} {tokens : List (ReductionToken n)} (closure : MarkedBoundaryClosure tokens) (separated : ReductionToken.IsSeparated tokens) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : ReductionToken.IsSeparated closure.targetTokens

Closing a boundary singleton preserves separation of the remaining residual names from all protected loop and block names.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryClosure.targetTokens_protectedNames_nodup {n : ℕ} {tokens : List (ReductionToken n)} (closure : MarkedBoundaryClosure tokens) (separated : ReductionToken.IsSeparated tokens) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) (nodup : (ReductionToken.protectedNames tokens).Nodup) : (ReductionToken.protectedNames closure.targetTokens).Nodup

Closing a raw boundary singleton transfers its residual carrier into protected ownership without duplicating any protected name.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryAtomRotate {n : ℕ} (tokens : List (ReductionToken n)) : Type

A raw boundary atom followed by a protected interval inside a residual inverse pair. One Dyck move rotates the raw atom behind that interval, exposing the next protected atom.

• carrier : Fin n

  The carrier declaration.

• hole : Fin n

  The hole declaration.

• carrierNegative : Bool

  The carrierNegative declaration.

• holeNegative : Bool

  The holeNegative declaration.

• insideTokens : List (ReductionToken n)

  The insideTokens declaration.

• outsideTokens : List (ReductionToken n)

  The outsideTokens declaration.

• rotated : tokens ~r ReductionToken.residual (dart self.carrier self.carrierNegative) :: ReductionToken.extracted (ExtractedBlock.boundary self.hole self.holeNegative) :: self.insideTokens ++ ReductionToken.residual (dart self.carrier !self.carrierNegative) :: self.outsideTokens
• residual_inside : ReductionToken.residualDarts self.insideTokens = []
• carrier_ne_hole : self.carrier ≠ self.hole
• carrier_not_mem_inside : self.carrier ∉ List.map edgeOfDart (ReductionToken.expand self.insideTokens)
• carrier_not_mem_outside : self.carrier ∉ List.map edgeOfDart (ReductionToken.expand self.outsideTokens)

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

Exact marked target of moving the raw boundary atom to the end of its protected interval.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryAtomRotate.perm_targetTokens {n : ℕ} {tokens : List (ReductionToken n)} (step : MarkedBoundaryAtomRotate tokens) : tokens.Perm step.targetTokens

Boundary-atom rotation only permutes atomic marked tokens.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryAtomRotate.expand_isRotated_sourceWord {n : ℕ} {tokens : List (ReductionToken n)} (step : MarkedBoundaryAtomRotate tokens) : ReductionToken.expand tokens ~r BoundaryAtomRotate.sourceWord step.carrier step.hole step.carrierNegative step.holeNegative (ReductionToken.expand step.insideTokens) (ReductionToken.expand step.outsideTokens)

Expansion of the marked source has the word-level boundary-atom rotation spelling.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryAtomRotate.expand_targetTokens {n : ℕ} {tokens : List (ReductionToken n)} (step : MarkedBoundaryAtomRotate tokens) : ReductionToken.expand step.targetTokens = BoundaryAtomRotate.targetWord step.carrier step.hole step.carrierNegative step.holeNegative (ReductionToken.expand step.insideTokens) (ReductionToken.expand step.outsideTokens)

Expansion of the exact marked target is the word-level rotation target.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryAtomRotate.targetTokens_isSeparated {n : ℕ} {tokens : List (ReductionToken n)} (step : MarkedBoundaryAtomRotate tokens) (separated : ReductionToken.IsSeparated tokens) : ReductionToken.IsSeparated step.targetTokens

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryAtomRotate.targetTokens_protectedNames_nodup {n : ℕ} {tokens : List (ReductionToken n)} (step : MarkedBoundaryAtomRotate tokens) (nodup : (ReductionToken.protectedNames tokens).Nodup) : (ReductionToken.protectedNames step.targetTokens).Nodup

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryAtomRotate.targetPair {n : ℕ} {tokens : List (ReductionToken n)} (step : MarkedBoundaryAtomRotate tokens) : MarkedResidualCancellablePair step.targetTokens

The same residual pair surrounds the rotated protected interval at the exact marked target.

Equations

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

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryBlockCommute {n : ℕ} (tokens : List (ReductionToken n)) : Type

A completed boundary-loop atom at the head of a protected residual-pair interval. One LoopGrouping move commutes this atom out of that interval.

• outer : Fin n

  The outer declaration.

• carrier : Fin n

  The carrier declaration.

• hole : Fin n

  The hole declaration.

• outerNegative : Bool

  The outerNegative declaration.

• carrierNegative : Bool

  The carrierNegative declaration.

• holeNegative : Bool

  The holeNegative declaration.

• insideTokens : List (ReductionToken n)

  The insideTokens declaration.

• outsideTokens : List (ReductionToken n)

  The outsideTokens declaration.

• rotated : tokens ~r ReductionToken.residual (dart self.outer self.outerNegative) :: ReductionToken.completed (CompletedBlock.boundary self.carrier self.hole self.carrierNegative self.holeNegative) :: self.insideTokens ++ ReductionToken.residual (dart self.outer !self.outerNegative) :: self.outsideTokens
• carrier_ne_hole : self.carrier ≠ self.hole
• carrier_ne_outer : self.carrier ≠ self.outer
• carrier_not_mem_inside : self.carrier ∉ List.map edgeOfDart (ReductionToken.expand self.insideTokens)
• carrier_not_mem_outside : self.carrier ∉ List.map edgeOfDart (ReductionToken.expand self.outsideTokens)

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

Exact marked target after commuting the completed boundary loop out of the residual pair.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryBlockCommute.perm_targetTokens {n : ℕ} {tokens : List (ReductionToken n)} (commute : MarkedBoundaryBlockCommute tokens) : tokens.Perm commute.targetTokens

The commute target merely permutes atomic marked tokens.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryBlockCommute.expand_isRotated_sourceWord {n : ℕ} {tokens : List (ReductionToken n)} (commute : MarkedBoundaryBlockCommute tokens) : ReductionToken.expand tokens ~r if commute.carrierNegative = true then BoundaryBlockCommute.negativeSourceWord commute.outer commute.carrier commute.hole commute.outerNegative commute.holeNegative (ReductionToken.expand commute.insideTokens) (ReductionToken.expand commute.outsideTokens) else BoundaryBlockCommute.sourceWord commute.outer commute.carrier commute.hole commute.outerNegative commute.holeNegative (ReductionToken.expand commute.insideTokens) (ReductionToken.expand commute.outsideTokens)

Expansion of the marked source has exactly the word-level boundary-block commute spelling.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryBlockCommute.expand_targetTokens {n : ℕ} {tokens : List (ReductionToken n)} (commute : MarkedBoundaryBlockCommute tokens) : ReductionToken.expand commute.targetTokens = if commute.carrierNegative = true then BoundaryBlockCommute.negativeTargetWord commute.outer commute.carrier commute.hole commute.outerNegative commute.holeNegative (ReductionToken.expand commute.insideTokens) (ReductionToken.expand commute.outsideTokens) else BoundaryBlockCommute.targetWord commute.outer commute.carrier commute.hole commute.outerNegative commute.holeNegative (ReductionToken.expand commute.insideTokens) (ReductionToken.expand commute.outsideTokens)

Expansion of the exact marked target is the word-level commute target.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryBlockCommute.targetTokens_isSeparated {n : ℕ} {tokens : List (ReductionToken n)} (commute : MarkedBoundaryBlockCommute tokens) (separated : ReductionToken.IsSeparated tokens) : ReductionToken.IsSeparated commute.targetTokens

Boundary-block commuting preserves the separated namespace invariant.

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

Boundary-block commuting preserves the classified-token grammar.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryBlockCommute.targetTokens_protectedNames_nodup {n : ℕ} {tokens : List (ReductionToken n)} (commute : MarkedBoundaryBlockCommute tokens) (nodup : (ReductionToken.protectedNames tokens).Nodup) : (ReductionToken.protectedNames commute.targetTokens).Nodup

Boundary-loop commuting preserves unique ownership of protected names.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedCrosscapBlockCommute {n : ℕ} (tokens : List (ReductionToken n)) : Type

A completed crosscap at the head of a protected residual-pair interval. Commuting it through the pair exchanges the residual and completed carriers and shortens that protected interval.

• outer : Fin n

  The outer declaration.

• carrier : Fin n

  The carrier declaration.

• outerNegative : Bool

  The outerNegative declaration.

• carrierNegative : Bool

  The carrierNegative declaration.

• insideTokens : List (ReductionToken n)

  The insideTokens declaration.

• outsideTokens : List (ReductionToken n)

  The outsideTokens declaration.

• rotated : tokens ~r ReductionToken.residual (dart self.outer self.outerNegative) :: ReductionToken.completed (CompletedBlock.crosscap self.carrier self.carrierNegative) :: self.insideTokens ++ ReductionToken.residual (dart self.outer !self.outerNegative) :: self.outsideTokens
• carrier_ne_outer : self.carrier ≠ self.outer
• carrier_not_mem_inside : self.carrier ∉ List.map edgeOfDart (ReductionToken.expand self.insideTokens)
• carrier_not_mem_outside : self.carrier ∉ List.map edgeOfDart (ReductionToken.expand self.outsideTokens)
• outer_not_mem_inside : self.outer ∉ List.map edgeOfDart (ReductionToken.expand self.insideTokens)
• outer_not_mem_outside : self.outer ∉ List.map edgeOfDart (ReductionToken.expand self.outsideTokens)

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

Exact marked target of contextual crosscap commuting.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedCrosscapBlockCommute.expand_isRotated_sourceWord {n : ℕ} {tokens : List (ReductionToken n)} (commute : MarkedCrosscapBlockCommute tokens) : ReductionToken.expand tokens ~r CrosscapBlockCommute.sourceWord commute.outer commute.carrier commute.outerNegative commute.carrierNegative (ReductionToken.expand commute.insideTokens) (ReductionToken.expand commute.outsideTokens)

Expansion of the marked source is the generic contextual crosscap source spelling.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedCrosscapBlockCommute.expand_targetTokens {n : ℕ} {tokens : List (ReductionToken n)} (commute : MarkedCrosscapBlockCommute tokens) : ReductionToken.expand commute.targetTokens = CrosscapBlockCommute.targetWord commute.outer commute.carrier commute.outerNegative commute.carrierNegative (ReductionToken.expand commute.insideTokens) (ReductionToken.expand commute.outsideTokens)

Expansion of the exact marked target is the generic contextual crosscap target spelling.

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

Contextual crosscap commuting preserves the classified-token grammar.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedCrosscapBlockCommute.targetTokens_isSeparated {n : ℕ} {tokens : List (ReductionToken n)} (commute : MarkedCrosscapBlockCommute tokens) (separated : ReductionToken.IsSeparated tokens) : ReductionToken.IsSeparated commute.targetTokens

Contextual crosscap commuting preserves separation of residual and protected edge names.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedCrosscapBlockCommute.targetTokens_protectedNames_nodup {n : ℕ} {tokens : List (ReductionToken n)} (commute : MarkedCrosscapBlockCommute tokens) (nodup : (ReductionToken.protectedNames tokens).Nodup) : (ReductionToken.protectedNames commute.targetTokens).Nodup

Crosscap commuting exchanges a protected carrier with a fresh residual carrier while preserving unique protected-name ownership.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedHandleBlockCommute {n : ℕ} (tokens : List (ReductionToken n)) : Type

A completed handle at the head of a protected residual-pair interval.

• outer : Fin n

  The outer declaration.

• first : Fin n

  The first declaration.

• second : Fin n

  The second declaration.

• outerNegative : Bool

  The outerNegative declaration.

• insideTokens : List (ReductionToken n)

  The insideTokens declaration.

• outsideTokens : List (ReductionToken n)

  The outsideTokens declaration.

• rotated : tokens ~r ReductionToken.residual (dart self.outer self.outerNegative) :: ReductionToken.completed (CompletedBlock.handle self.first self.second) :: self.insideTokens ++ ReductionToken.residual (dart self.outer !self.outerNegative) :: self.outsideTokens
• first_ne_second : self.first ≠ self.second
• first_ne_outer : self.first ≠ self.outer
• second_ne_outer : self.second ≠ self.outer
• first_not_mem_inside : self.first ∉ List.map edgeOfDart (ReductionToken.expand self.insideTokens)
• first_not_mem_outside : self.first ∉ List.map edgeOfDart (ReductionToken.expand self.outsideTokens)
• second_not_mem_inside : self.second ∉ List.map edgeOfDart (ReductionToken.expand self.insideTokens)
• second_not_mem_outside : self.second ∉ List.map edgeOfDart (ReductionToken.expand self.outsideTokens)
• outer_not_mem_inside : self.outer ∉ List.map edgeOfDart (ReductionToken.expand self.insideTokens)
• outer_not_mem_outside : self.outer ∉ List.map edgeOfDart (ReductionToken.expand self.outsideTokens)

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

Exact marked target after moving the completed handle outside the residual pair.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedHandleBlockCommute.perm_targetTokens {n : ℕ} {tokens : List (ReductionToken n)} (commute : MarkedHandleBlockCommute tokens) : tokens.Perm commute.targetTokens

Handle commuting merely permutes atomic marked tokens.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedHandleBlockCommute.expand_isRotated_sourceWord {n : ℕ} {tokens : List (ReductionToken n)} (commute : MarkedHandleBlockCommute tokens) : ReductionToken.expand tokens ~r HandleBlockCommute.sourceWord commute.outer commute.first commute.second commute.outerNegative (ReductionToken.expand commute.insideTokens) (ReductionToken.expand commute.outsideTokens)

Expansion of the marked source is the generic contextual handle source spelling.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedHandleBlockCommute.expand_targetTokens {n : ℕ} {tokens : List (ReductionToken n)} (commute : MarkedHandleBlockCommute tokens) : ReductionToken.expand commute.targetTokens = HandleBlockCommute.targetWord commute.outer commute.first commute.second commute.outerNegative (ReductionToken.expand commute.insideTokens) (ReductionToken.expand commute.outsideTokens)

Expansion of the exact marked target is the generic contextual handle target spelling.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedHandleBlockCommute.targetTokens_isSeparated {n : ℕ} {tokens : List (ReductionToken n)} (commute : MarkedHandleBlockCommute tokens) (separated : ReductionToken.IsSeparated tokens) : ReductionToken.IsSeparated commute.targetTokens

Handle commuting preserves the separated namespace invariant.

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

Handle commuting preserves the classified-token grammar.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedHandleBlockCommute.targetTokens_protectedNames_nodup {n : ℕ} {tokens : List (ReductionToken n)} (commute : MarkedHandleBlockCommute tokens) (nodup : (ReductionToken.protectedNames tokens).Nodup) : (ReductionToken.protectedNames commute.targetTokens).Nodup

Handle commuting preserves unique ownership of protected names.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryPairContraction {n : ℕ} (tokens : List (ReductionToken (n + 1))) : Type

Two adjacent extracted boundary singletons which form a P1-subdivided boundary segment.

• first : Fin (n + 1)

  The first declaration.

• second : Fin (n + 1)

  The second declaration.

• firstNegative : Bool

  The firstNegative declaration.

• secondNegative : Bool

  The secondNegative declaration.

• tailTokens : List (ReductionToken (n + 1))

  The tailTokens declaration.

• rotated : tokens ~r [ReductionToken.extracted (ExtractedBlock.boundary self.first self.firstNegative), ReductionToken.extracted (ExtractedBlock.boundary self.second self.secondNegative)] ++ self.tailTokens
• first_ne_second : self.first ≠ self.second
• first_not_mem_tail : self.first ∉ List.map edgeOfDart (ReductionToken.expand self.tailTokens)
• second_not_mem_tail : self.second ∉ List.map edgeOfDart (ReductionToken.expand self.tailTokens)

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryPairContraction.ofRotatedOfProtectedNodup {n : ℕ} {tokens : List (ReductionToken (n + 1))} (first second : Fin (n + 1)) (firstNegative secondNegative : Bool) (tailTokens : List (ReductionToken (n + 1))) (rotated : tokens ~r [ReductionToken.extracted (ExtractedBlock.boundary first firstNegative), ReductionToken.extracted (ExtractedBlock.boundary second secondNegative)] ++ tailTokens) (separated : ReductionToken.IsSeparated tokens) (protectedNodup : (ReductionToken.protectedNames tokens).Nodup) : MarkedBoundaryPairContraction tokens

Build a boundary contraction from a displayed adjacent pair. Separation rules the protected names out of the residual tail, while duplicate-freeness of protected names supplies distinctness and rules them out of every protected tail token.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryPairContraction.targetTokens {n : ℕ} {tokens : List (ReductionToken (n + 1))} (contraction : MarkedBoundaryPairContraction tokens) : List (ReductionToken n)

Exact marked target after contracting the second boundary subdivision edge.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryPairContraction.expand_isRotated_sourceWord {n : ℕ} {tokens : List (ReductionToken (n + 1))} (contraction : MarkedBoundaryPairContraction tokens) : ReductionToken.expand tokens ~r BoundaryPairContraction.sourceWord contraction.first contraction.second contraction.firstNegative contraction.secondNegative (ReductionToken.expand contraction.tailTokens)

Expansion of the marked source is the adjacent-boundary contraction source spelling.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryPairContraction.expand_targetTokens {n : ℕ} {tokens : List (ReductionToken (n + 1))} (contraction : MarkedBoundaryPairContraction tokens) : ReductionToken.expand contraction.targetTokens = BoundaryPairContraction.targetWord contraction.first contraction.second ⋯ (ReductionToken.expand contraction.tailTokens)

Expansion of the marked target is the word-level P1 contraction target.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryPairContraction.targetTokens_allClassified {n : ℕ} {tokens : List (ReductionToken (n + 1))} (contraction : MarkedBoundaryPairContraction tokens) (classified : ReductionToken.AllClassified tokens) : ReductionToken.AllClassified contraction.targetTokens

Boundary-subdivision contraction preserves the classified-token grammar.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryPairContraction.targetTokens_isSeparated {n : ℕ} {tokens : List (ReductionToken (n + 1))} (contraction : MarkedBoundaryPairContraction tokens) (separated : ReductionToken.IsSeparated tokens) : ReductionToken.IsSeparated contraction.targetTokens

Boundary-subdivision contraction preserves separation of residual and protected names.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryPairContraction.targetTokens_protectedNames_nodup {n : ℕ} {tokens : List (ReductionToken (n + 1))} (contraction : MarkedBoundaryPairContraction tokens) (nodup : (ReductionToken.protectedNames tokens).Nodup) : (ReductionToken.protectedNames contraction.targetTokens).Nodup

Boundary-subdivision contraction preserves duplicate-freeness of protected name spines.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryPairContraction.residualDarts_targetTokens_length_eq {n : ℕ} {tokens : List (ReductionToken (n + 1))} (contraction : MarkedBoundaryPairContraction tokens) : (ReductionToken.residualDarts contraction.targetTokens).length = (ReductionToken.residualDarts tokens).length

Boundary-subdivision contraction preserves the number of residual darts.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryBlockCommute.targetPair {n : ℕ} {tokens : List (ReductionToken (n + 1))} (commute : MarkedBoundaryBlockCommute tokens) (residualInside : ReductionToken.residualDarts commute.insideTokens = []) : MarkedResidualCancellablePair commute.targetTokens

After commuting a completed boundary loop, the same residual pair surrounds exactly 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.MarkedCrosscapBlockCommute.targetPair {n : ℕ} {tokens : List (ReductionToken (n + 1))} (commute : MarkedCrosscapBlockCommute tokens) (residualInside : ReductionToken.residualDarts commute.insideTokens = []) : MarkedResidualCancellablePair commute.targetTokens

After contextual crosscap commuting, the old crosscap carrier is the new residual carrier around exactly the strict tail of the protected interval.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedHandleBlockCommute.targetPair {n : ℕ} {tokens : List (ReductionToken (n + 1))} (commute : MarkedHandleBlockCommute tokens) (residualInside : ReductionToken.residualDarts commute.insideTokens = []) : MarkedResidualCancellablePair commute.targetTokens

After commuting a completed handle, the same residual pair surrounds exactly the strict tail of the protected interval.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.exists_betweenAtoms {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (classified : ReductionToken.AllClassified tokens) : ∃ (atoms : List (ProtectedAtom (n + 1))), pair.betweenTokens = List.map ReductionToken.ofProtectedAtom atoms

Under the classified-state invariant, the interval crossed by a lifted residual cancellation is an exact finite list of typed protected atoms.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.toBoundaryAtomRotateOfValid {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (hole : Fin (n + 1)) (holeNegative : Bool) (insideTokens : List (ReductionToken (n + 1))) (hbetween : pair.betweenTokens = ReductionToken.extracted (ExtractedBlock.boundary hole holeNegative) :: insideTokens) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : MarkedBoundaryAtomRotate tokens

A raw boundary atom with a nonempty protected suffix exposes the Dyck transition which moves that raw atom behind the suffix.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.toBoundaryPairContraction {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (first second : Fin (n + 1)) (firstNegative secondNegative : Bool) (insideTokens : List (ReductionToken (n + 1))) (hbetween : pair.betweenTokens = [ReductionToken.extracted (ExtractedBlock.boundary first firstNegative), ReductionToken.extracted (ExtractedBlock.boundary second secondNegative)] ++ insideTokens) (separated : ReductionToken.IsSeparated tokens) (protectedNodup : (ReductionToken.protectedNames tokens).Nodup) : MarkedBoundaryPairContraction tokens

Two raw boundary atoms at the head of a protected residual-pair interval expose an adjacent P1 contraction after one cyclic token rotation.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.boundaryContractionTargetPair {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (first second : Fin (n + 1)) (firstNegative secondNegative : Bool) (insideTokens : List (ReductionToken (n + 1))) (hbetween : pair.betweenTokens = [ReductionToken.extracted (ExtractedBlock.boundary first firstNegative), ReductionToken.extracted (ExtractedBlock.boundary second secondNegative)] ++ insideTokens) (separated : ReductionToken.IsSeparated tokens) (protectedNodup : (ReductionToken.protectedNames tokens).Nodup) : MarkedResidualCancellablePair (pair.toBoundaryPairContraction first second firstNegative secondNegative insideTokens hbetween separated protectedNodup).targetTokens

After contracting the first two raw boundary atoms, the same residual inverse pair surrounds their merged singleton followed by the strict tail of the old protected interval.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.boundaryContractionTargetPair_between_length_lt {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (first second : Fin (n + 1)) (firstNegative secondNegative : Bool) (insideTokens : List (ReductionToken (n + 1))) (hbetween : pair.betweenTokens = [ReductionToken.extracted (ExtractedBlock.boundary first firstNegative), ReductionToken.extracted (ExtractedBlock.boundary second secondNegative)] ++ insideTokens) (separated : ReductionToken.IsSeparated tokens) (protectedNodup : (ReductionToken.protectedNames tokens).Nodup) : (pair.boundaryContractionTargetPair first second firstNegative secondNegative insideTokens hbetween separated protectedNodup).betweenTokens.length < pair.betweenTokens.length

A boundary contraction removes one protected atom from the selected residual-pair interval.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.toBoundaryClosure {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (hole : Fin (n + 1)) (holeNegative : Bool) (hbetween : pair.betweenTokens = [ReductionToken.extracted (ExtractedBlock.boundary hole holeNegative)]) : MarkedBoundaryClosure tokens

A lifted residual pair surrounding exactly one boundary singleton is a boundary closure.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.toBoundaryBlockCommute {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (carrier hole : Fin (n + 1)) (carrierNegative holeNegative : Bool) (insideTokens : List (ReductionToken (n + 1))) (hbetween : pair.betweenTokens = ReductionToken.completed (CompletedBlock.boundary carrier hole carrierNegative holeNegative) :: insideTokens) (hcarrierHole : carrier ≠ hole) (hcarrierOuter : carrier ≠ pair.edge) (hcarrierInside : carrier ∉ List.map edgeOfDart (ReductionToken.expand insideTokens)) (hcarrierOutside : carrier ∉ List.map edgeOfDart (ReductionToken.expand pair.tailTokens)) : MarkedBoundaryBlockCommute tokens

A lifted residual pair whose protected interval begins with a completed boundary loop exposes the exact boundary-block commute transition.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.toBoundaryBlockCommuteOfValid {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (carrier hole : Fin (n + 1)) (carrierNegative holeNegative : Bool) (insideTokens : List (ReductionToken (n + 1))) (hbetween : pair.betweenTokens = ReductionToken.completed (CompletedBlock.boundary carrier hole carrierNegative holeNegative) :: insideTokens) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : MarkedBoundaryBlockCommute tokens

Surface multiplicity supplies all freshness conditions needed to commute a completed boundary-loop atom at the head of a lifted residual-pair interval.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.toCrosscapBlockCommute {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (carrier : Fin (n + 1)) (carrierNegative : Bool) (insideTokens : List (ReductionToken (n + 1))) (hbetween : pair.betweenTokens = ReductionToken.completed (CompletedBlock.crosscap carrier carrierNegative) :: insideTokens) (hcarrierOuter : carrier ≠ pair.edge) (hcarrierInside : carrier ∉ List.map edgeOfDart (ReductionToken.expand insideTokens)) (hcarrierOutside : carrier ∉ List.map edgeOfDart (ReductionToken.expand pair.tailTokens)) (houterInside : pair.edge ∉ List.map edgeOfDart (ReductionToken.expand insideTokens)) (houterOutside : pair.edge ∉ List.map edgeOfDart (ReductionToken.expand pair.tailTokens)) : MarkedCrosscapBlockCommute tokens

A lifted residual pair whose protected interval begins with a completed crosscap exposes the exact contextual crosscap transition.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.toCrosscapBlockCommuteOfValid {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (carrier : Fin (n + 1)) (carrierNegative : Bool) (insideTokens : List (ReductionToken (n + 1))) (hbetween : pair.betweenTokens = ReductionToken.completed (CompletedBlock.crosscap carrier carrierNegative) :: insideTokens) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : MarkedCrosscapBlockCommute tokens

Surface multiplicity supplies every freshness condition needed for a contextual crosscap transition at the head of a lifted residual-pair interval.

Equations

• pair.toCrosscapBlockCommuteOfValid carrier carrierNegative insideTokens hbetween valid = pair.toCrosscapBlockCommute carrier carrierNegative insideTokens hbetween ⋯ ⋯ ⋯ ⋯ ⋯

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.toHandleBlockCommute {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (first second : Fin (n + 1)) (insideTokens : List (ReductionToken (n + 1))) (hbetween : pair.betweenTokens = ReductionToken.completed (CompletedBlock.handle first second) :: insideTokens) (hfirstSecond : first ≠ second) (hfirstOuter : first ≠ pair.edge) (hsecondOuter : second ≠ pair.edge) (hfirstInside : first ∉ List.map edgeOfDart (ReductionToken.expand insideTokens)) (hfirstOutside : first ∉ List.map edgeOfDart (ReductionToken.expand pair.tailTokens)) (hsecondInside : second ∉ List.map edgeOfDart (ReductionToken.expand insideTokens)) (hsecondOutside : second ∉ List.map edgeOfDart (ReductionToken.expand pair.tailTokens)) (houterInside : pair.edge ∉ List.map edgeOfDart (ReductionToken.expand insideTokens)) (houterOutside : pair.edge ∉ List.map edgeOfDart (ReductionToken.expand pair.tailTokens)) : MarkedHandleBlockCommute tokens

A lifted residual pair whose protected interval begins with a completed handle exposes the exact contextual handle transition.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.toHandleBlockCommuteOfValid {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (first second : Fin (n + 1)) (insideTokens : List (ReductionToken (n + 1))) (hbetween : pair.betweenTokens = ReductionToken.completed (CompletedBlock.handle first second) :: insideTokens) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : MarkedHandleBlockCommute tokens

Surface multiplicity supplies every distinction and freshness condition needed for a contextual handle transition.

Equations

• pair.toHandleBlockCommuteOfValid first second insideTokens hbetween valid = pair.toHandleBlockCommute first second insideTokens hbetween ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯ ⋯

inductive LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.Disposition {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) : Type

Exhaustive local disposition of a lifted residual inverse pair. The first two constructors are already executable. The final constructor isolates the remaining contextual move: commuting a nontrivial protected interval out of the inverse pair before cancellation.

• adjacent {n : ℕ} {tokens : List (ReductionToken (n + 1))} {pair : MarkedResidualCancellablePair tokens} (between_eq : pair.betweenTokens = []) : pair.Disposition
• boundary {n : ℕ} {tokens : List (ReductionToken (n + 1))} {pair : MarkedResidualCancellablePair tokens} (hole : Fin (n + 1)) (holeNegative : Bool) (between_eq : pair.betweenTokens = [ReductionToken.extracted (ExtractedBlock.boundary hole holeNegative)]) : pair.Disposition
• contextual {n : ℕ} {tokens : List (ReductionToken (n + 1))} {pair : MarkedResidualCancellablePair tokens} (between_ne : pair.betweenTokens ≠ []) (not_boundary : ∀ (hole : Fin (n + 1)) (holeNegative : Bool), pair.betweenTokens ≠ [ReductionToken.extracted (ExtractedBlock.boundary hole holeNegative)]) : pair.Disposition

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.disposition {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) : pair.Disposition

Classify every lifted residual pair into the two completed executable cases or the exact remaining contextual case.

Equations

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

inductive LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.ClassifiedDisposition {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) : Type

Classified-state refinement of Disposition: every genuinely contextual interval exposes its first typed protected atom and the exact remaining atom list.

• adjacent {n : ℕ} {tokens : List (ReductionToken (n + 1))} {pair : MarkedResidualCancellablePair tokens} (between_eq : pair.betweenTokens = []) : pair.ClassifiedDisposition
• boundary {n : ℕ} {tokens : List (ReductionToken (n + 1))} {pair : MarkedResidualCancellablePair tokens} (hole : Fin (n + 1)) (holeNegative : Bool) (between_eq : pair.betweenTokens = [ReductionToken.extracted (ExtractedBlock.boundary hole holeNegative)]) : pair.ClassifiedDisposition
• structured {n : ℕ} {tokens : List (ReductionToken (n + 1))} {pair : MarkedResidualCancellablePair tokens} (first : ProtectedAtom (n + 1)) (rest : List (ProtectedAtom (n + 1))) (between_eq : pair.betweenTokens = List.map ReductionToken.ofProtectedAtom (first :: rest)) : pair.ClassifiedDisposition

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.classifiedDisposition {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (classified : ReductionToken.AllClassified tokens) : pair.ClassifiedDisposition

Exhaustively expose the typed protected interval of a lifted residual pair. A singleton raw boundary atom is kept as the dedicated executable boundary-closure case.

Equations

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

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

A complete proof-relevant decomposition trace. Each step extracts one certified block, then pair-reduces the strictly shorter residual before continuing.

• done {n : ℕ} : ResidualDecomposition []
• step {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (feature : ActionablePairReductionFeature word) (reduction : ResidualPairReduction feature.residualWord) (tail : ResidualDecomposition reduction.reducedWord) : ResidualDecomposition word

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

Extracted blocks, in recursive extraction order.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ResidualDecomposition.done.blocks = []
• (LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ResidualDecomposition.step feature reduction tail).blocks = feature.block :: tail.blocks

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

Edge names consumed by all blocks in extraction order.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ResidualDecomposition.done.extractedEdges = []

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

Number of boundary singleton blocks in a decomposition.

Equations

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

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

Number of crosscap square blocks in a decomposition.

Equations

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

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

Number of handle blocks in a decomposition.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ResidualDecomposition.normalForm {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (decomposition : ResidualDecomposition word) : NormalForm

The normal-form parameters selected by a complete block decomposition. In the presence of any crosscap, each handle contributes two additional crosscaps via Gallier--Xu Step 5.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ResidualDecomposition.count_sum_eq_blocks_length {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (decomposition : ResidualDecomposition word) : decomposition.boundaryCount + decomposition.crosscapCount + decomposition.handleCount = decomposition.blocks.length

Every extracted block belongs to exactly one of the three block classes.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ResidualDecomposition.blocks_ne_nil_of_word_ne_nil {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (decomposition : ResidualDecomposition word) (hne : word ≠ []) : decomposition.blocks ≠ []

A decomposition of a nonempty word extracts at least one block.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ResidualDecomposition.normalForm_isEvalAdmissible_of_word_ne_nil {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (decomposition : ResidualDecomposition word) (hne : word ≠ []) : decomposition.normalForm.IsEvalAdmissible

The normal form selected from a nonempty decomposition is Eval-admissible.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ResidualDecomposition.mem_source_of_mem_extractedEdges {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (decomposition : ResidualDecomposition word) (e : Fin n) (he : e ∈ decomposition.extractedEdges) : e ∈ List.map edgeOfDart word

Every edge recorded by a decomposition occurs in that decomposition's source word.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ResidualDecomposition.extractedEdges_nodup {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (decomposition : ResidualDecomposition word) : decomposition.extractedEdges.Nodup

Distinct extraction steps consume disjoint edge names.

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

One descent step from a directed opposite arc: either an immediately extractable feature, or a strictly shorter opposite arc nested inside it.

• actionable {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a : Fin n} {form : OppositeArcForm word a} (feature : ActionablePairReductionFeature word) : OppositeArcStep word form
• nested {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a : Fin n} {form : OppositeArcForm word a} (b : Fin n) (inner : OppositeArcForm word b) (shorter : inner.between.length < form.between.length) : OppositeArcStep word form

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

Every once-used edge can be displayed at the cyclic head.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.OppositeArcForm.exists_step_of_usedMultiplicities {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a : Fin n} (form : OppositeArcForm word a) (multiplicities : HasValidUsedMultiplicities word) (reduced : IsPairReduced word) : Nonempty (OppositeArcStep word form)

Inspect the first dart of a nonempty opposite arc. A boundary or equal-orientation edge is immediately actionable. An opposite edge either crosses the selected pair, yielding a handle, or closes inside it, yielding a strictly shorter directed arc.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.OppositeArcForm.exists_step {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a : Fin n} (form : OppositeArcForm word a) (valid : (Dyck.oneFace word).IsSurfaceValid) (reduced : IsPairReduced word) : Nonempty (OppositeArcStep word form)

Surface-valid words supply the residual multiplicity hypothesis required by one opposite-arc descent step.

@[irreducible]

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.OppositeArcForm.findActionableOfUsedMultiplicities {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a : Fin n} (form : OppositeArcForm word a) (multiplicities : HasValidUsedMultiplicities word) (reduced : IsPairReduced word) : ActionablePairReductionFeature word

Well-founded descent through nested opposite pairs terminates at a boundary, crosscap, or interleaved handle feature.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.OppositeArcForm.findActionable {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a : Fin n} (form : OppositeArcForm word a) (valid : (Dyck.oneFace word).IsSurfaceValid) (reduced : IsPairReduced word) : ActionablePairReductionFeature word

Validity-specialized spelling of the residual opposite-arc descent.

Equations

• form.findActionable valid reduced = form.findActionableOfUsedMultiplicities ⋯ reduced

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

In a pair-reduced word, the two darts of an opposite form have a nonempty intervening word.

Proof-producing extraction of the easy pairing features

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

The displayed cyclic word carried by an interleaved-pair certificate.

Equations

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

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

The adjacent handle block produced by the three-Dyck extraction chain.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.InterleavedOccurrenceForm.negativeInsideSignedIso {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a b : Fin n} (form : InterleavedOccurrenceForm word a b) (hnegative : form.bNegativeInside = true) : (Dyck.oneFace form.displayedWord).SignedPresentationIso (Handle.source a b form.beforeB form.beforeNegA form.beforeOutsideB form.remainder)

When b is encountered negative inside the a-pair, reverse that edge to obtain the positive-first source spelling required by handle extraction.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.InterleavedOccurrenceForm.exists_normalizationEquivalent_grouped {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a b : Fin n} (form : InterleavedOccurrenceForm word a b) (valid : (Dyck.oneFace word).IsSurfaceValid) : ∃ (validGrouped : (Dyck.oneFace form.groupedWord).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace word, valid := valid } { presentation := Dyck.oneFace form.groupedWord, valid := validGrouped }

A certified interleaved pair produces an adjacent handle block through the existing three-Dyck normalization chain. If the inner occurrence of b is negative, the chain begins by reversing the orientation assigned to b.

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

The cyclic spelling obtained by displaying a boundary edge at the head of its word.

Equations

• form.headWord = LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.dart a form.negative :: form.remainder

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.BoundaryOccurrenceForm.exists_normalizationEquivalent_head {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a : Fin n} (form : BoundaryOccurrenceForm word a) (valid : (Dyck.oneFace word).IsSurfaceValid) : ∃ (validHead : (Dyck.oneFace form.headWord).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace word, valid := valid } { presentation := Dyck.oneFace form.headWord, valid := validHead }

Displaying a certified boundary occurrence at the head is already a normalization equivalence: it is only a cyclic change of the distinguished face word.

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

The grouped spelling produced from a certified crosscap occurrence. The segment after the second occurrence is reversed, exactly as in the Gallier--Xu crosscap rewrite.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CrosscapOccurrenceForm.positiveTarget_isRotated_grouped {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a : Fin n} (form : CrosscapOccurrenceForm word a) (hpositive : form.negative = false) : (Crosscap.target a form.between form.remainder).boundary 0 ~r form.groupedWord

The positive crosscap target is cyclically the chosen grouped spelling.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CrosscapOccurrenceForm.negativeTarget_isRotated_grouped {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a : Fin n} (form : CrosscapOccurrenceForm word a) (hnegative : form.negative = true) : (Crosscap.negativeTarget a form.between form.remainder).boundary 0 ~r form.groupedWord

The negative crosscap target is cyclically the chosen grouped spelling.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CrosscapOccurrenceForm.exists_normalizationEquivalent_grouped {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {a : Fin n} (form : CrosscapOccurrenceForm word a) (valid : (Dyck.oneFace word).IsSurfaceValid) : ∃ (validGrouped : (Dyck.oneFace form.groupedWord).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace word, valid := valid } { presentation := Dyck.oneFace form.groupedWord, valid := validGrouped }

A certified equally oriented pair can be moved to an adjacent crosscap block by an exact normalization chain. Both signs are supported; the grouped block retains the input sign.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionFeature.block_word_append_residualWord {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (feature : ActionablePairReductionFeature word) : feature.block.word ++ feature.residualWord = match feature with | boundary a form => form.headWord | crosscap a form => form.groupedWord | handle a b form => form.groupedWord

Each local extraction target is definitionally its extracted block followed by the residual word used by the global recursion.

inductive LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionResult {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (valid : (Dyck.oneFace word).IsSurfaceValid) : Type

A proof-producing result of acting on one certified pairing feature. The constructor records the exact extracted spelling, its transported validity, and the normalization chain from the original word.

• boundary {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {valid : (Dyck.oneFace word).IsSurfaceValid} (a : Fin n) (form : BoundaryOccurrenceForm word a) (validHead : (Dyck.oneFace form.headWord).IsSurfaceValid) (equivalent : NormalizationEquivalent { presentation := Dyck.oneFace word, valid := valid } { presentation := Dyck.oneFace form.headWord, valid := validHead }) : ActionablePairReductionResult word valid
• crosscap {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {valid : (Dyck.oneFace word).IsSurfaceValid} (a : Fin n) (form : CrosscapOccurrenceForm word a) (validGrouped : (Dyck.oneFace form.groupedWord).IsSurfaceValid) (equivalent : NormalizationEquivalent { presentation := Dyck.oneFace word, valid := valid } { presentation := Dyck.oneFace form.groupedWord, valid := validGrouped }) : ActionablePairReductionResult word valid
• handle {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {valid : (Dyck.oneFace word).IsSurfaceValid} (a b : Fin n) (form : InterleavedOccurrenceForm word a b) (validGrouped : (Dyck.oneFace form.groupedWord).IsSurfaceValid) (equivalent : NormalizationEquivalent { presentation := Dyck.oneFace word, valid := valid } { presentation := Dyck.oneFace form.groupedWord, valid := validGrouped }) : ActionablePairReductionResult word valid

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionResult.feature {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {valid : (Dyck.oneFace word).IsSurfaceValid} : ActionablePairReductionResult word valid → ActionablePairReductionFeature word

Feature whose local normalization chain was executed.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionResult.targetWord {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {valid : (Dyck.oneFace word).IsSurfaceValid} (result : ActionablePairReductionResult word valid) : List (SurfaceCellComplex.SignedDart (Fin n))

Exact block-plus-residual word reached by an executed extraction.

Equations

• result.targetWord = result.feature.block.word ++ result.feature.residualWord

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionResult.target {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {valid : (Dyck.oneFace word).IsSurfaceValid} : ActionablePairReductionResult word valid → ValidPresentation

Valid presentation reached by one actionable extraction.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionResult.target_presentation_eq_oneFace_targetWord {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {valid : (Dyck.oneFace word).IsSurfaceValid} (result : ActionablePairReductionResult word valid) : result.target.presentation = Dyck.oneFace result.targetWord

The stored target presentation is the one-face presentation on targetWord.

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

Validity witness for the exact block-plus-residual target word.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionResult.equivalent {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {valid : (Dyck.oneFace word).IsSurfaceValid} (result : ActionablePairReductionResult word valid) : NormalizationEquivalent { presentation := Dyck.oneFace word, valid := valid } result.target

Normalization equivalence certified by one actionable extraction.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionResult.equivalent_to_targetWord {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} {valid : (Dyck.oneFace word).IsSurfaceValid} (result : ActionablePairReductionResult word valid) : NormalizationEquivalent { presentation := Dyck.oneFace word, valid := valid } { presentation := Dyck.oneFace result.targetWord, valid := ⋯ }

Normalization equivalence to the stable exact block-plus-residual spelling.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionFeature.extract {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (feature : ActionablePairReductionFeature word) (valid : (Dyck.oneFace word).IsSurfaceValid) : ActionablePairReductionResult word valid

Execute an actionable pairing feature using the corresponding proof-producing rewrite endpoint.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionFeature.feature_extract {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (feature : ActionablePairReductionFeature word) (valid : (Dyck.oneFace word).IsSurfaceValid) : (feature.extract valid).feature = feature

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ActionablePairReductionFeature.targetWord_extract {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (feature : ActionablePairReductionFeature word) (valid : (Dyck.oneFace word).IsSurfaceValid) : (feature.extract valid).targetWord = feature.block.word ++ feature.residualWord

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedActionablePairReductionResult {n : ℕ} {tokens : List (ReductionToken n)} (marked : MarkedActionablePairReductionFeature tokens) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : Prop

Proof-producing execution of an extraction on a marked word, with the exact marked target retained as its public endpoint.

• targetValid : (Dyck.oneFace (ReductionToken.expand marked.targetTokens)).IsSurfaceValid
• targetSeparated : ReductionToken.IsSeparated marked.targetTokens
• targetClassified : ReductionToken.AllClassified marked.targetTokens
• targetProtectedNodup : (ReductionToken.protectedNames marked.targetTokens).Nodup
• equivalent : NormalizationEquivalent { presentation := Dyck.oneFace (ReductionToken.expand tokens), valid := valid } { presentation := Dyck.oneFace (ReductionToken.expand marked.targetTokens), valid := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedActionablePairReductionFeature.extract {n : ℕ} {tokens : List (ReductionToken n)} (marked : MarkedActionablePairReductionFeature tokens) (separated : ReductionToken.IsSeparated tokens) (classified : ReductionToken.AllClassified tokens) (protectedNodup : (ReductionToken.protectedNames tokens).Nodup) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : MarkedActionablePairReductionResult marked valid

Execute a marked feature by expanding it, applying the corresponding Gallier--Xu move, and transporting the result back to the exact marked target spelling.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedCancellablePair.cancellationTargetTokens {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedCancellablePair tokens) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : List (ReductionToken n)

Exact lowered marked endpoint of an adjacent inverse-pair cancellation.

Equations

• pair.cancellationTargetTokens valid = LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.lowerTokensAvoiding pair.edge pair.tailTokens ⋯

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedCancellationResult {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedCancellablePair tokens) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : Prop

Proof-producing cancellation of a token-adjacent inverse pair, retaining the lowered marked target rather than flattening previously extracted blocks.

• targetValid : (Dyck.oneFace (ReductionToken.expand (pair.cancellationTargetTokens valid))).IsSurfaceValid
• targetSeparated : ReductionToken.IsSeparated (pair.cancellationTargetTokens valid)
• targetClassified : ReductionToken.AllClassified (pair.cancellationTargetTokens valid)
• targetProtectedNodup : (ReductionToken.protectedNames (pair.cancellationTargetTokens valid)).Nodup
• equivalent : NormalizationEquivalent { presentation := Dyck.oneFace (ReductionToken.expand tokens), valid := valid } { presentation := Dyck.oneFace (ReductionToken.expand (pair.cancellationTargetTokens valid)), valid := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedCancellablePair.cancel {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedCancellablePair tokens) (separated : ReductionToken.IsSeparated tokens) (classified : ReductionToken.AllClassified tokens) (protectedNodup : (ReductionToken.protectedNames tokens).Nodup) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) (tail_nonempty : ReductionToken.expand pair.tailTokens ≠ []) : MarkedCancellationResult pair valid

Execute an inverse pair which is genuinely adjacent in the marked word. The nonempty-tail hypothesis selects the ordinary cancellation endpoint; the empty-tail sphere endpoint remains handled by the outer cancellation recursion.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryClosureResult {n : ℕ} {tokens : List (ReductionToken n)} (closure : MarkedBoundaryClosure tokens) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : Prop

Proof-producing reclassification of a residual inverse pair and boundary singleton as one atomic protected loop.

• targetValid : (Dyck.oneFace (ReductionToken.expand closure.targetTokens)).IsSurfaceValid
• targetSeparated : ReductionToken.IsSeparated closure.targetTokens
• targetClassified : ReductionToken.AllClassified closure.targetTokens
• targetProtectedNodup : (ReductionToken.protectedNames closure.targetTokens).Nodup
• equivalent : NormalizationEquivalent { presentation := Dyck.oneFace (ReductionToken.expand tokens), valid := valid } { presentation := Dyck.oneFace (ReductionToken.expand closure.targetTokens), valid := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryClosure.close {n : ℕ} {tokens : List (ReductionToken n)} (closure : MarkedBoundaryClosure tokens) (separated : ReductionToken.IsSeparated tokens) (classified : ReductionToken.AllClassified tokens) (protectedNodup : (ReductionToken.protectedNames tokens).Nodup) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : MarkedBoundaryClosureResult closure valid

Close an extracted boundary singleton into an atomic loop. The underlying signed word changes only by cyclic rotation, while the residual measure drops by the two carrier darts.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryAtomRotateResult {n : ℕ} {tokens : List (ReductionToken n)} (step : MarkedBoundaryAtomRotate tokens) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : Prop

Proof-producing Dyck rotation of a raw boundary atom behind a protected interval.

• targetValid : (Dyck.oneFace (ReductionToken.expand step.targetTokens)).IsSurfaceValid
• targetSeparated : ReductionToken.IsSeparated step.targetTokens
• targetClassified : ReductionToken.AllClassified step.targetTokens
• targetProtectedNodup : (ReductionToken.protectedNames step.targetTokens).Nodup
• equivalent : NormalizationEquivalent { presentation := Dyck.oneFace (ReductionToken.expand tokens), valid := valid } { presentation := Dyck.oneFace (ReductionToken.expand step.targetTokens), valid := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryAtomRotate.rotate {n : ℕ} {tokens : List (ReductionToken n)} (step : MarkedBoundaryAtomRotate tokens) (separated : ReductionToken.IsSeparated tokens) (classified : ReductionToken.AllClassified tokens) (protectedNodup : (ReductionToken.protectedNames tokens).Nodup) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : MarkedBoundaryAtomRotateResult step valid

Execute the raw-boundary rotation through the exact signed Dyck chain.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryBlockCommuteResult {n : ℕ} {tokens : List (ReductionToken n)} (commute : MarkedBoundaryBlockCommute tokens) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : Prop

Proof-producing commute of one completed boundary loop out of a contextual residual pair.

• targetValid : (Dyck.oneFace (ReductionToken.expand commute.targetTokens)).IsSurfaceValid
• targetSeparated : ReductionToken.IsSeparated commute.targetTokens
• targetClassified : ReductionToken.AllClassified commute.targetTokens
• targetProtectedNodup : (ReductionToken.protectedNames commute.targetTokens).Nodup
• equivalent : NormalizationEquivalent { presentation := Dyck.oneFace (ReductionToken.expand tokens), valid := valid } { presentation := Dyck.oneFace (ReductionToken.expand commute.targetTokens), valid := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryBlockCommute.commute {n : ℕ} {tokens : List (ReductionToken n)} (step : MarkedBoundaryBlockCommute tokens) (separated : ReductionToken.IsSeparated tokens) (classified : ReductionToken.AllClassified tokens) (protectedNodup : (ReductionToken.protectedNames tokens).Nodup) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : MarkedBoundaryBlockCommuteResult step valid

Execute the contextual boundary-loop commute through the exact word-level LoopGrouping chain, supporting either orientation of the loop carrier.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedCrosscapBlockCommuteResult {n : ℕ} {tokens : List (ReductionToken n)} (commute : MarkedCrosscapBlockCommute tokens) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : Prop

Proof-producing commute of one completed crosscap through a contextual residual pair.

• targetValid : (Dyck.oneFace (ReductionToken.expand commute.targetTokens)).IsSurfaceValid
• targetSeparated : ReductionToken.IsSeparated commute.targetTokens
• targetClassified : ReductionToken.AllClassified commute.targetTokens
• targetProtectedNodup : (ReductionToken.protectedNames commute.targetTokens).Nodup
• equivalent : NormalizationEquivalent { presentation := Dyck.oneFace (ReductionToken.expand tokens), valid := valid } { presentation := Dyck.oneFace (ReductionToken.expand commute.targetTokens), valid := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedCrosscapBlockCommute.commute {n : ℕ} {tokens : List (ReductionToken n)} (step : MarkedCrosscapBlockCommute tokens) (separated : ReductionToken.IsSeparated tokens) (classified : ReductionToken.AllClassified tokens) (protectedNodup : (ReductionToken.protectedNames tokens).Nodup) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : MarkedCrosscapBlockCommuteResult step valid

Execute contextual crosscap commuting through the exact two-crosscap word chain.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedHandleBlockCommuteResult {n : ℕ} {tokens : List (ReductionToken n)} (commute : MarkedHandleBlockCommute tokens) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : Prop

Proof-producing commute of one completed handle through a contextual residual pair.

• targetValid : (Dyck.oneFace (ReductionToken.expand commute.targetTokens)).IsSurfaceValid
• targetSeparated : ReductionToken.IsSeparated commute.targetTokens
• targetClassified : ReductionToken.AllClassified commute.targetTokens
• targetProtectedNodup : (ReductionToken.protectedNames commute.targetTokens).Nodup
• equivalent : NormalizationEquivalent { presentation := Dyck.oneFace (ReductionToken.expand tokens), valid := valid } { presentation := Dyck.oneFace (ReductionToken.expand commute.targetTokens), valid := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedHandleBlockCommute.commute {n : ℕ} {tokens : List (ReductionToken n)} (step : MarkedHandleBlockCommute tokens) (separated : ReductionToken.IsSeparated tokens) (classified : ReductionToken.AllClassified tokens) (protectedNodup : (ReductionToken.protectedNames tokens).Nodup) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : MarkedHandleBlockCommuteResult step valid

Execute contextual handle commuting through the exact four-Dyck word chain.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryPairContractionResult {n : ℕ} {tokens : List (ReductionToken (n + 1))} (contraction : MarkedBoundaryPairContraction tokens) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : Prop

Proof-producing contraction of two adjacent extracted boundary subdivisions.

• targetValid : (Dyck.oneFace (ReductionToken.expand contraction.targetTokens)).IsSurfaceValid
• targetSeparated : ReductionToken.IsSeparated contraction.targetTokens
• targetClassified : ReductionToken.AllClassified contraction.targetTokens
• targetProtectedNodup : (ReductionToken.protectedNames contraction.targetTokens).Nodup
• equivalent : NormalizationEquivalent { presentation := Dyck.oneFace (ReductionToken.expand tokens), valid := valid } { presentation := Dyck.oneFace (ReductionToken.expand contraction.targetTokens), valid := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedBoundaryPairContraction.contract {n : ℕ} {tokens : List (ReductionToken (n + 1))} (step : MarkedBoundaryPairContraction tokens) (separated : ReductionToken.IsSeparated tokens) (classified : ReductionToken.AllClassified tokens) (protectedNodup : (ReductionToken.protectedNames tokens).Nodup) (valid : (Dyck.oneFace (ReductionToken.expand tokens)).IsSurfaceValid) : MarkedBoundaryPairContractionResult step valid

Execute one adjacent-boundary P1 contraction, lowering the ambient edge type by one.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualPairShortening {n : ℕ} {tokens : List (ReductionToken n)} (pair : MarkedResidualCancellablePair tokens) (state : MarkedExecutionState tokens) : Type

One certified transition which strictly shortens the protected interval of a lifted residual pair while preserving the total number of residual darts.

• targetEdgeCount : ℕ

  The targetEdgeCount declaration.

• targetTokens : List (ReductionToken self.targetEdgeCount)

  The targetTokens declaration.

• targetPair : MarkedResidualCancellablePair self.targetTokens

  The targetPair declaration.

• targetState : MarkedExecutionState self.targetTokens
• targetProtectedNonempty : ReductionToken.protectedNames self.targetTokens ≠ []
• equivalent : NormalizationEquivalent { presentation := Dyck.oneFace (ReductionToken.expand tokens), valid := ⋯ } { presentation := Dyck.oneFace (ReductionToken.expand self.targetTokens), valid := ⋯ }
• residualLengthEq : (ReductionToken.residualDarts self.targetTokens).length = (ReductionToken.residualDarts tokens).length
• rawBoundaryCountTailEq : ReductionToken.rawBoundaryCount self.targetPair.tailTokens = ReductionToken.rawBoundaryCount pair.tailTokens
• betweenLengthLt : self.targetPair.betweenTokens.length < pair.betweenTokens.length

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualPairShortening.prepend {n m : ℕ} {tokens : List (ReductionToken n)} (pair : MarkedResidualCancellablePair tokens) (state : MarkedExecutionState tokens) {middleTokens : List (ReductionToken m)} (middlePair : MarkedResidualCancellablePair middleTokens) (middleState : MarkedExecutionState middleTokens) (stepEquivalent : NormalizationEquivalent { presentation := Dyck.oneFace (ReductionToken.expand tokens), valid := ⋯ } { presentation := Dyck.oneFace (ReductionToken.expand middleTokens), valid := ⋯ }) (residualLengthEq : (ReductionToken.residualDarts middleTokens).length = (ReductionToken.residualDarts tokens).length) (betweenLengthEq : middlePair.betweenTokens.length = pair.betweenTokens.length) (rawBoundaryCountTailEq : ReductionToken.rawBoundaryCount middlePair.tailTokens = ReductionToken.rawBoundaryCount pair.tailTokens) (tail : MarkedResidualPairShortening middlePair middleState) : MarkedResidualPairShortening pair state

Prepend a residual- and interval-length-preserving marked transition to a strict shortening.

Equations

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

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualPairRotation {n : ℕ} {tokens : List (ReductionToken n)} (pair : MarkedResidualCancellablePair tokens) (state : MarkedExecutionState tokens) : Type

One certified transition which preserves both residual length and protected-interval length.

• targetTokens : List (ReductionToken n)

  The targetTokens declaration.

• targetPair : MarkedResidualCancellablePair self.targetTokens

  The targetPair declaration.

• targetState : MarkedExecutionState self.targetTokens
• targetProtectedNonempty : ReductionToken.protectedNames self.targetTokens ≠ []
• equivalent : NormalizationEquivalent { presentation := Dyck.oneFace (ReductionToken.expand tokens), valid := ⋯ } { presentation := Dyck.oneFace (ReductionToken.expand self.targetTokens), valid := ⋯ }
• residualLengthEq : (ReductionToken.residualDarts self.targetTokens).length = (ReductionToken.residualDarts tokens).length
• rawBoundaryCountTailEq : ReductionToken.rawBoundaryCount self.targetPair.tailTokens = ReductionToken.rawBoundaryCount pair.tailTokens
• betweenLengthEq : self.targetPair.betweenTokens.length = pair.betweenTokens.length

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.rotateBoundaryAtom {n : ℕ} {tokens : List (ReductionToken n)} (pair : MarkedResidualCancellablePair tokens) (state : MarkedExecutionState tokens) (protectedNonempty : ReductionToken.protectedNames tokens ≠ []) (hole : Fin n) (holeNegative : Bool) (insideTokens : List (ReductionToken n)) (hbetween : pair.betweenTokens = ReductionToken.extracted (ExtractedBlock.boundary hole holeNegative) :: insideTokens) : MarkedResidualPairRotation pair state

Move a leading raw boundary atom behind a nonempty protected suffix without changing either the residual or protected-interval measure.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.rotateBoundaryAtom_targetPair_betweenTokens {n : ℕ} {tokens : List (ReductionToken n)} (pair : MarkedResidualCancellablePair tokens) (state : MarkedExecutionState tokens) (protectedNonempty : ReductionToken.protectedNames tokens ≠ []) (hole : Fin n) (holeNegative : Bool) (insideTokens : List (ReductionToken n)) (hbetween : pair.betweenTokens = ReductionToken.extracted (ExtractedBlock.boundary hole holeNegative) :: insideTokens) : (pair.rotateBoundaryAtom state protectedNonempty hole holeNegative insideTokens hbetween).targetPair.betweenTokens = insideTokens ++ [ReductionToken.extracted (ExtractedBlock.boundary hole holeNegative)]

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.shortenBoundaryBlock {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (state : MarkedExecutionState tokens) (protectedNonempty : ReductionToken.protectedNames tokens ≠ []) (carrier hole : Fin (n + 1)) (carrierNegative holeNegative : Bool) (insideTokens : List (ReductionToken (n + 1))) (hbetween : pair.betweenTokens = ReductionToken.completed (CompletedBlock.boundary carrier hole carrierNegative holeNegative) :: insideTokens) : MarkedResidualPairShortening pair state

Commute a completed boundary loop out of a lifted pair, producing a strict interval shortening.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.shortenCrosscapBlock {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (state : MarkedExecutionState tokens) (carrier : Fin (n + 1)) (carrierNegative : Bool) (insideTokens : List (ReductionToken (n + 1))) (hbetween : pair.betweenTokens = ReductionToken.completed (CompletedBlock.crosscap carrier carrierNegative) :: insideTokens) : MarkedResidualPairShortening pair state

Commute a completed crosscap out of a lifted pair, producing a strict interval shortening.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.shortenHandleBlock {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (state : MarkedExecutionState tokens) (protectedNonempty : ReductionToken.protectedNames tokens ≠ []) (first second : Fin (n + 1)) (insideTokens : List (ReductionToken (n + 1))) (hbetween : pair.betweenTokens = ReductionToken.completed (CompletedBlock.handle first second) :: insideTokens) : MarkedResidualPairShortening pair state

Commute a completed handle out of a lifted pair, producing a strict interval shortening.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.shortenBoundaryPair {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (state : MarkedExecutionState tokens) (first second : Fin (n + 1)) (firstNegative secondNegative : Bool) (insideTokens : List (ReductionToken (n + 1))) (hbetween : pair.betweenTokens = [ReductionToken.extracted (ExtractedBlock.boundary first firstNegative), ReductionToken.extracted (ExtractedBlock.boundary second secondNegative)] ++ insideTokens) : MarkedResidualPairShortening pair state

Contract two adjacent raw boundary atoms, producing a strict interval shortening in the lowered ambient edge type.

Equations

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

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualPairResolution {n : ℕ} {tokens : List (ReductionToken n)} (pair : MarkedResidualCancellablePair tokens) (state : MarkedExecutionState tokens) : Type

Certified elimination of one lifted residual inverse pair. The target may have a smaller ambient edge type after P1 cancellation or boundary contraction, but always has strictly fewer residual darts and retains at least one protected name.

• targetEdgeCount : ℕ

  The targetEdgeCount declaration.

• targetTokens : List (ReductionToken self.targetEdgeCount)

  The targetTokens declaration.

• targetState : MarkedExecutionState self.targetTokens
• targetProtectedNonempty : ReductionToken.protectedNames self.targetTokens ≠ []
• equivalent : NormalizationEquivalent { presentation := Dyck.oneFace (ReductionToken.expand tokens), valid := ⋯ } { presentation := Dyck.oneFace (ReductionToken.expand self.targetTokens), valid := ⋯ }
• residualLengthEqTail : (ReductionToken.residualDarts self.targetTokens).length = (ReductionToken.residualDarts pair.tailTokens).length
• rawBoundaryCountEqTail : ReductionToken.rawBoundaryCount self.targetTokens = ReductionToken.rawBoundaryCount pair.tailTokens
• residualLengthLt : (ReductionToken.residualDarts self.targetTokens).length < (ReductionToken.residualDarts tokens).length

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualPairResolution.prepend {n m : ℕ} {tokens : List (ReductionToken n)} (pair : MarkedResidualCancellablePair tokens) (state : MarkedExecutionState tokens) {middleTokens : List (ReductionToken m)} (middlePair : MarkedResidualCancellablePair middleTokens) (middleState : MarkedExecutionState middleTokens) (stepEquivalent : NormalizationEquivalent { presentation := Dyck.oneFace (ReductionToken.expand tokens), valid := ⋯ } { presentation := Dyck.oneFace (ReductionToken.expand middleTokens), valid := ⋯ }) (residualLengthEq : (ReductionToken.residualDarts middleTokens).length = (ReductionToken.residualDarts tokens).length) (rawBoundaryCountTailEq : ReductionToken.rawBoundaryCount middlePair.tailTokens = ReductionToken.rawBoundaryCount pair.tailTokens) (tail : MarkedResidualPairResolution middlePair middleState) : MarkedResidualPairResolution pair state

Prepend a residual-length-preserving marked transition to a completed pair resolution.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.resolveAdjacent {n : ℕ} {tokens : List (ReductionToken n)} (pair : MarkedResidualCancellablePair tokens) (state : MarkedExecutionState tokens) (protectedNonempty : ReductionToken.protectedNames tokens ≠ []) (hempty : pair.betweenTokens = []) : MarkedResidualPairResolution pair state

Eliminate an adjacent lifted pair by ordinary cancellation. A protected-name witness rules out the exceptional empty-tail sphere endpoint.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.resolveBoundary {n : ℕ} {tokens : List (ReductionToken (n + 1))} (pair : MarkedResidualCancellablePair tokens) (state : MarkedExecutionState tokens) (hole : Fin (n + 1)) (holeNegative : Bool) (hbetween : pair.betweenTokens = [ReductionToken.extracted (ExtractedBlock.boundary hole holeNegative)]) : MarkedResidualPairResolution pair state

Eliminate a lifted pair surrounding one raw boundary atom by reclassifying the three displayed tokens as one completed boundary loop.

Equations

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

@[irreducible]

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.resolveFuel {n : ℕ} {tokens : List (ReductionToken n)} (fuel : ℕ) (pair : MarkedResidualCancellablePair tokens) (state : MarkedExecutionState tokens) (protectedNonempty : ReductionToken.protectedNames tokens ≠ []) (hbound : pair.betweenTokens.length ≤ fuel) : MarkedResidualPairResolution pair state

Resolve one lifted residual inverse pair. The fuel measures the protected interval: every contextual step strictly shortens it, while the terminal cases eliminate the residual pair.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedResidualCancellablePair.resolve {n : ℕ} {tokens : List (ReductionToken n)} (pair : MarkedResidualCancellablePair tokens) (state : MarkedExecutionState tokens) (protectedNonempty : ReductionToken.protectedNames tokens ≠ []) : MarkedResidualPairResolution pair state

Eliminate one lifted residual inverse pair by the terminating protected-interval resolver.

Equations

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

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedPairReductionResult {n : ℕ} {tokens : List (ReductionToken n)} (state : MarkedExecutionState tokens) : Type

Certified marked endpoint after all cancellable pairs have been removed from the erased residual word. Already protected names remain present, even when cancellations lower the ambient edge type.

• targetEdgeCount : ℕ

  The targetEdgeCount declaration.

• targetTokens : List (ReductionToken self.targetEdgeCount)

  The targetTokens declaration.

• targetState : MarkedExecutionState self.targetTokens
• targetProtectedNonempty : ReductionToken.protectedNames self.targetTokens ≠ []
• targetReduced : IsPairReduced (ReductionToken.residualDarts self.targetTokens)
• targetResidualLengthLe : (ReductionToken.residualDarts self.targetTokens).length ≤ (ReductionToken.residualDarts tokens).length
• equivalent : NormalizationEquivalent { presentation := Dyck.oneFace (ReductionToken.expand tokens), valid := ⋯ } { presentation := Dyck.oneFace (ReductionToken.expand self.targetTokens), valid := ⋯ }

@[irreducible]

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedExecutionState.reduceResidualPairsFuel {n : ℕ} {tokens : List (ReductionToken n)} (fuel : ℕ) (state : MarkedExecutionState tokens) (protectedNonempty : ReductionToken.protectedNames tokens ≠ []) (hbound : (ReductionToken.residualDarts tokens).length ≤ fuel) : MarkedPairReductionResult state

Fuel-bounded execution of residual inverse-pair reduction inside a classified marked word. Each resolved pair strictly decreases the erased residual length.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedExecutionState.reduceResidualPairs {n : ℕ} {tokens : List (ReductionToken n)} (state : MarkedExecutionState tokens) (protectedNonempty : ReductionToken.protectedNames tokens ≠ []) : MarkedPairReductionResult state

Execute all residual inverse-pair cancellations in a marked state which already owns at least one protected name.

Equations

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

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

The local feature exposed at a selected edge of a pair-reduced valid word.

• boundary {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (a : Fin n) (form : BoundaryOccurrenceForm word a) : PairReductionFeature word
• crosscap {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (a : Fin n) (form : CrosscapOccurrenceForm word a) : PairReductionFeature word
• opposite {n : ℕ} {word : List (SurfaceCellComplex.SignedDart (Fin n))} (a : Fin n) (form : OppositeOccurrenceForm word a) (between_nonempty : form.between ≠ []) : PairReductionFeature word

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.exists_pairReductionFeature {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (valid : (Dyck.oneFace word).IsSurfaceValid) (reduced : IsPairReduced word) (hn : 0 < n) : Nonempty (PairReductionFeature word)

Every pair-reduced valid word with at least one edge exposes either a boundary dart, an equally oriented crosscap pair, or a nondegenerate opposite pair.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.exists_actionablePairReductionFeature {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (valid : (Dyck.oneFace word).IsSurfaceValid) (reduced : IsPairReduced word) (hn : 0 < n) : Nonempty (ActionablePairReductionFeature word)

Every nonempty pair-reduced valid word exposes a feature with a complete local normalization chain: a boundary edge, a crosscap pair, or an interleaved pair ready for handle extraction.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.exists_actionablePairReductionFeature_of_usedMultiplicities {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (multiplicities : HasValidUsedMultiplicities word) (reduced : IsPairReduced word) (hne : word ≠ []) : Nonempty (ActionablePairReductionFeature word)

Residual form of actionable-feature existence. It needs only a nonempty residual word, surface multiplicities for names still used there, and pair reduction; already-grouped ambient edge names may be absent.

@[irreducible]

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

Fuel-bounded decomposition of a pair-reduced residual word into boundary, crosscap, and handle blocks. Pair cancellation after each extraction restores the induction hypothesis.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.decomposeResidual {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (multiplicities : HasValidUsedMultiplicities word) (reduced : IsPairReduced word) : ResidualDecomposition word

Every pair-reduced residual word with valid used-edge multiplicities admits a terminating block decomposition.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.decomposePairReduced {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (valid : (Dyck.oneFace word).IsSurfaceValid) (reduced : IsPairReduced word) : ResidualDecomposition word

Surface-valid pair-reduced one-face words admit the residual block decomposition needed by the global Gallier--Xu normalization recursion.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.pairReducedNormalForm {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (valid : (Dyck.oneFace word).IsSurfaceValid) (reduced : IsPairReduced word) : NormalForm

Normal-form parameters computed from the certified decomposition of a pair-reduced valid one-face word.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.pairReducedNormalForm_isEvalAdmissible {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (valid : (Dyck.oneFace word).IsSurfaceValid) (reduced : IsPairReduced word) : (pairReducedNormalForm word valid reduced).IsEvalAdmissible

The normal-form parameters selected from a pair-reduced valid word satisfy the exact Lean-Eval admissibility predicate.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.extractPairReductionFeature {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (valid : (Dyck.oneFace word).IsSurfaceValid) (reduced : IsPairReduced word) (hn : 0 < n) : ActionablePairReductionResult word valid

Find and execute one certified normalization step on any nonempty pair-reduced valid word.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.extractPairReductionFeature word valid reduced hn = (Classical.choice ⋯).extract valid

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedExtractionResult {n : ℕ} {tokens : List (ReductionToken n)} (state : MarkedExecutionState tokens) : Type

Certified endpoint of the marked extraction recursion: no residual darts remain, every token is classified, and at least one protected name survives.

• targetEdgeCount : ℕ

  The targetEdgeCount declaration.

• targetTokens : List (ReductionToken self.targetEdgeCount)

  The targetTokens declaration.

• targetState : MarkedExecutionState self.targetTokens
• targetProtectedNonempty : ReductionToken.protectedNames self.targetTokens ≠ []
• targetResidualEmpty : ReductionToken.residualDarts self.targetTokens = []
• equivalent : NormalizationEquivalent { presentation := Dyck.oneFace (ReductionToken.expand tokens), valid := ⋯ } { presentation := Dyck.oneFace (ReductionToken.expand self.targetTokens), valid := ⋯ }

@[irreducible]

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedExecutionState.finishExtractionsFuel {n : ℕ} {tokens : List (ReductionToken n)} (fuel : ℕ) (state : MarkedExecutionState tokens) (protectedNonempty : ReductionToken.protectedNames tokens ≠ []) (reduced : IsPairReduced (ReductionToken.residualDarts tokens)) (hbound : (ReductionToken.residualDarts tokens).length ≤ fuel) : MarkedExtractionResult state

Fuel-bounded marked Gallier--Xu extraction after at least one protected block has been created. Every extraction strictly shortens the residual word, and the intervening marked pair reducer restores pair reduction before the recursive call.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedExecutionState.finishExtractions {n : ℕ} {tokens : List (ReductionToken n)} (state : MarkedExecutionState tokens) (protectedNonempty : ReductionToken.protectedNames tokens ≠ []) (reduced : IsPairReduced (ReductionToken.residualDarts tokens)) : MarkedExtractionResult state

Finish marked extraction from a pair-reduced state which already owns a protected name.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedExecutionState.normalizePairReducedMarked {n : ℕ} (word : List (SurfaceCellComplex.SignedDart (Fin n))) (valid : (Dyck.oneFace word).IsSurfaceValid) (reduced : IsPairReduced word) : MarkedExtractionResult ⋯

Execute the complete marked extraction recursion from an arbitrary pair-reduced valid one-face word. The first extraction establishes protected-name ownership; subsequent calls use finishExtractions.

Equations

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

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord : Type

Exact atom-level endpoint of the marked recursion. Its name spine is duplicate-free, its word is surface-valid, and at least one protected atom remains.

• edgeCount : ℕ

  The edgeCount declaration.

• atoms : List (ProtectedAtom self.edgeCount)

  The atoms declaration.

• atomsNonempty : self.atoms ≠ []
• namesNodup : (ProtectedAtom.sequenceNames self.atoms).Nodup
• valid : (Dyck.oneFace (ProtectedAtom.sequenceWord self.atoms)).IsSurfaceValid

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.validPresentation (terminal : TerminalProtectedWord) : ValidPresentation

Validity-bundled finite-cyclic presentation displayed by a terminal atom word.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.normalForm (terminal : TerminalProtectedWord) : NormalForm

Exact canonical normal form selected by a terminal atom word.

Equations

• terminal.normalForm = LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.normalForm terminal.atoms

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.admissible (terminal : TerminalProtectedWord) : terminal.normalForm.IsEvalAdmissible

A terminal atom word always selects an Eval-admissible canonical presentation.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.retainedAtoms (terminal : TerminalProtectedWord) : List (ProtectedAtom (terminal.edgeCount + 1))

Retain the terminal atom sequence after adding the fresh boundary-envelope carrier.

Equations

• terminal.retainedAtoms = List.map LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ProtectedAtom.retain terminal.atoms

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.retainedTokens (terminal : TerminalProtectedWord) : List (ReductionToken (terminal.edgeCount + 1))

Represent every retained terminal atom as one protected marked token.

Equations

• terminal.retainedTokens = List.map LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.ReductionToken.ofProtectedAtom terminal.retainedAtoms

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.envelopedTokens (terminal : TerminalProtectedWord) : List (ReductionToken (terminal.edgeCount + 1))

Marked target of the boundary envelope: the fresh opposite carrier pair surrounds all retained terminal atoms.

Equations

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

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.expand_retainedTokens (terminal : TerminalProtectedWord) : ReductionToken.expand terminal.retainedTokens = P2.retainWord (ProtectedAtom.sequenceWord terminal.atoms)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.expand_envelopedTokens (terminal : TerminalProtectedWord) : ReductionToken.expand terminal.envelopedTokens = BoundaryEnvelope.targetWord (ProtectedAtom.sequenceWord terminal.atoms)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.residualDarts_retainedTokens (terminal : TerminalProtectedWord) : ReductionToken.residualDarts terminal.retainedTokens = []

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.residualDarts_envelopedTokens (terminal : TerminalProtectedWord) : ReductionToken.residualDarts terminal.envelopedTokens = [SurfaceCellComplex.SignedDart.pos (BoundaryEnvelope.carrier terminal.edgeCount), SurfaceCellComplex.SignedDart.neg (BoundaryEnvelope.carrier terminal.edgeCount)]

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.protectedNames_retainedTokens (terminal : TerminalProtectedWord) : ReductionToken.protectedNames terminal.retainedTokens = List.map Fin.castSucc (ProtectedAtom.sequenceNames terminal.atoms)

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.protectedNames_envelopedTokens (terminal : TerminalProtectedWord) : ReductionToken.protectedNames terminal.envelopedTokens = List.map Fin.castSucc (ProtectedAtom.sequenceNames terminal.atoms)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.sequenceNames_ne_nil (terminal : TerminalProtectedWord) : ProtectedAtom.sequenceNames terminal.atoms ≠ []

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.protectedNames_envelopedTokens_ne_nil (terminal : TerminalProtectedWord) : ReductionToken.protectedNames terminal.envelopedTokens ≠ []

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.envelopedSeparated (terminal : TerminalProtectedWord) : ReductionToken.IsSeparated terminal.envelopedTokens

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.envelopedClassified (terminal : TerminalProtectedWord) : ReductionToken.AllClassified terminal.envelopedTokens

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.envelopedProtectedNodup (terminal : TerminalProtectedWord) : (ReductionToken.protectedNames terminal.envelopedTokens).Nodup

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.envelopedState (terminal : TerminalProtectedWord) : MarkedExecutionState terminal.envelopedTokens

Valid marked execution state carried by the fresh boundary envelope.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.envelopedPair (terminal : TerminalProtectedWord) : MarkedResidualCancellablePair terminal.envelopedTokens

The fresh boundary-envelope carrier as an actionable marked residual pair.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.resolveEnvelope (terminal : TerminalProtectedWord) : MarkedResidualPairResolution terminal.envelopedPair ⋯

Execute the existing protected-interval resolver on the fresh boundary envelope.

Equations

• terminal.resolveEnvelope = terminal.envelopedPair.resolve ⋯ ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.resolveEnvelope_residualLength_lt_two (terminal : TerminalProtectedWord) : (ReductionToken.residualDarts terminal.resolveEnvelope.targetTokens).length < 2

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.resolveEnvelope_residualDarts_eq_nil (terminal : TerminalProtectedWord) : ReductionToken.residualDarts terminal.resolveEnvelope.targetTokens = []

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.resolveEnvelope_rawBoundaryCount_eq_zero (terminal : TerminalProtectedWord) : ReductionToken.rawBoundaryCount terminal.resolveEnvelope.targetTokens = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.normalizationEquivalent_resolveEnvelope (terminal : TerminalProtectedWord) : NormalizationEquivalent terminal.validPresentation { presentation := Dyck.oneFace (ReductionToken.expand terminal.resolveEnvelope.targetTokens), valid := ⋯ }

Boundary enveloping followed by the existing marked resolver preserves the realization of the original terminal protected word.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.finishEnvelope (terminal : TerminalProtectedWord) : MarkedExtractionResult ⋯

Finish the fresh-carrier resolution at a certified residual-empty marked endpoint.

Equations

• terminal.finishEnvelope = ⋯.finishExtractions ⋯ ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.normalizationEquivalent_finishEnvelope (terminal : TerminalProtectedWord) : NormalizationEquivalent terminal.validPresentation { presentation := Dyck.oneFace (ReductionToken.expand terminal.finishEnvelope.targetTokens), valid := ⋯ }

The completely executed boundary-envelope chain preserves the original realization.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.finishEnvelope_residualDarts_eq_nil (terminal : TerminalProtectedWord) : ReductionToken.residualDarts terminal.finishEnvelope.targetTokens = []

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedExecutionState.toTerminalProtectedWord {n : ℕ} {tokens : List (ReductionToken n)} (state : MarkedExecutionState tokens) (protectedNonempty : ReductionToken.protectedNames tokens ≠ []) (residualEmpty : ReductionToken.residualDarts tokens = []) : TerminalProtectedWord

Forget the marked-token implementation of a residual-empty state and retain its exact terminal protected-atom word.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.MarkedExecutionState.expand_eq_toTerminalProtectedWord_sequenceWord {n : ℕ} {tokens : List (ReductionToken n)} (state : MarkedExecutionState tokens) (protectedNonempty : ReductionToken.protectedNames tokens ≠ []) (residualEmpty : ReductionToken.residualDarts tokens = []) : ReductionToken.expand tokens = ProtectedAtom.sequenceWord (state.toTerminalProtectedWord protectedNonempty residualEmpty).atoms

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalCompletedWord : Type

Exact block-level endpoint after every raw boundary singleton has been completed.

• edgeCount : ℕ

  The edgeCount declaration.

• blocks : List (CompletedBlock self.edgeCount)

  The blocks declaration.

• blocksNonempty : self.blocks ≠ []
• namesNodup : (CompletedBlock.sequenceNames self.blocks).Nodup
• valid : (Dyck.oneFace (CompletedBlock.sequenceWord self.blocks)).IsSurfaceValid

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalCompletedWord.validPresentation (terminal : TerminalCompletedWord) : ValidPresentation

Validity-bundled finite-cyclic presentation displayed by a terminal completed-block word.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalCompletedWord.normalForm (terminal : TerminalCompletedWord) : NormalForm

Exact canonical normal form selected by the completed block counts.

Equations

• terminal.normalForm = LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.normalForm terminal.blocks

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalCompletedWord.admissible (terminal : TerminalCompletedWord) : terminal.normalForm.IsEvalAdmissible

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.boundaryNormalizedWord (terminal : TerminalProtectedWord) : TerminalProtectedWord

Atom-level terminal word returned by the fully executed fresh boundary envelope.

Equations

• terminal.boundaryNormalizedWord = ⋯.toTerminalProtectedWord ⋯ ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.boundaryNormalizedWord_rawBoundaryCount_eq_zero (terminal : TerminalProtectedWord) : ProtectedAtom.rawBoundaryCount terminal.boundaryNormalizedWord.atoms = 0

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.normalizationEquivalent_boundaryNormalizedWord (terminal : TerminalProtectedWord) : NormalizationEquivalent terminal.validPresentation terminal.boundaryNormalizedWord.validPresentation

The boundary-envelope execution exposes a residual-empty protected atom word equivalent to the original terminal word.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.completedBlocks (terminal : TerminalProtectedWord) (hraw : ProtectedAtom.rawBoundaryCount terminal.atoms = 0) : List (CompletedBlock terminal.edgeCount)

Extract the unique completed-block sequence from a raw-free terminal atom word.

Equations

• terminal.completedBlocks hraw = Classical.choose ⋯

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.atoms_eq_map_completedBlocks (terminal : TerminalProtectedWord) (hraw : ProtectedAtom.rawBoundaryCount terminal.atoms = 0) : terminal.atoms = List.map ProtectedAtom.completed (terminal.completedBlocks hraw)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.completedBlocks_ne_nil (terminal : TerminalProtectedWord) (hraw : ProtectedAtom.rawBoundaryCount terminal.atoms = 0) : terminal.completedBlocks hraw ≠ []

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.boundaryCompletedWord (terminal : TerminalProtectedWord) : TerminalCompletedWord

Completed-block endpoint selected by the fully executed boundary normalization.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.normalizationEquivalent_boundaryCompletedWord (terminal : TerminalProtectedWord) : NormalizationEquivalent terminal.validPresentation terminal.boundaryCompletedWord.validPresentation

Boundary normalization lands exactly in the completed-block terminal interface.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.completedNormalForm (terminal : TerminalProtectedWord) : NormalForm

Exact normal form selected after constructive raw-boundary completion.

Equations

• terminal.completedNormalForm = terminal.boundaryCompletedWord.normalForm

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedWord.completedAdmissible (terminal : TerminalProtectedWord) : terminal.completedNormalForm.IsEvalAdmissible

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalMarkedNormalizer : Type

The isolated terminal obligation after the terminating marked recursion: normalize a valid, classified marked word whose residual contribution is empty.

• normalize {n : ℕ} {tokens : List (ReductionToken n)} (state : MarkedExecutionState tokens) : ReductionToken.protectedNames tokens ≠ [] → ReductionToken.residualDarts tokens = [] → NormalizationResult { presentation := Dyck.oneFace (ReductionToken.expand tokens), valid := ⋯ }

  The normalize declaration.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalCompletedNormalizer : Prop

Narrow completed-block obligation: order and orient a valid, nonempty, duplicate-free block sequence and perform the nonorientable handle conversion.

• equivalent (terminal : TerminalCompletedWord) : NormalizationEquivalent terminal.validPresentation (canonicalValidPresentation terminal.normalForm ⋯)

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedNormalizer : Prop

Narrow terminal obligation at the proof's stable seam: normalize a duplicate-free nonempty sequence of protected atoms to the exact canonical presentation selected after boundary completion.

• equivalent (terminal : TerminalProtectedWord) : NormalizationEquivalent terminal.validPresentation (canonicalValidPresentation terminal.completedNormalForm ⋯)

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalCompletedNormalizer.toTerminalProtectedNormalizer (normalizer : TerminalCompletedNormalizer) : TerminalProtectedNormalizer

A completed-block normalizer discharges the protected-word seam after constructive boundary completion.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedNormalizer.normalize (normalizer : TerminalProtectedNormalizer) (terminal : TerminalProtectedWord) : NormalizationResult terminal.validPresentation

Package a protected-word terminal equivalence as the standard exact normalization result.

Equations

• normalizer.normalize terminal = { normalForm := terminal.completedNormalForm, admissible := ⋯, equivalent := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalProtectedNormalizer.toTerminalMarkedNormalizer (normalizer : TerminalProtectedNormalizer) : TerminalMarkedNormalizer

A protected-word normalizer discharges the token-level terminal interface used by the marked extraction recursion.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.pairReducedNormalizerOfTerminal (terminal : TerminalMarkedNormalizer) : PairReducedNormalizer

A terminal block normalizer supplies the remaining PairReducedNormalizer field after the now-complete marked extraction recursion.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.normalizeConnectedOfTerminal (terminal : TerminalMarkedNormalizer) (P : ValidPresentation) (connectedP : P.presentation.IsConnected) : NormalizationResult P

The universal connected normalization theorem is reduced to the explicit terminal block normalizer, with face merging, initial cancellation, marked extraction, and canonical-result composition already discharged.

Equations

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