Terminal finite-cyclic word normalization

This file discharges the final completed-block seam of the Gallier--Xu normalization argument. Boundary loops are commuted behind the closed-surface blocks, handles are converted to crosscaps when a crosscap is present, and the resulting ordered word is signed-relabelled to the single project-owned NormalForm.canonicalPresentation.

@[simp]

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

The distinct-name spine respects block-sequence concatenation.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.mem_sequenceWord_edge_iff_mem_sequenceNames {n : ℕ} (blocks : List (CompletedBlock n)) (edge : Fin n) : edge ∈ List.map edgeOfDart (sequenceWord blocks) ↔ edge ∈ sequenceNames blocks

A name occurs in the exact block word precisely when it occurs in the block name spine.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.sequenceWord_perm {n : ℕ} {left right : List (CompletedBlock n)} (hperm : left.Perm right) : (sequenceWord left).Perm (sequenceWord right)

Permuting completed blocks permutes their exact concatenated words.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.sequenceNames_perm {n : ℕ} {left right : List (CompletedBlock n)} (hperm : left.Perm right) : (sequenceNames left).Perm (sequenceNames right)

Permuting completed blocks permutes their distinct-name spines.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.sequenceEdgeWord_perm {n : ℕ} {left right : List (CompletedBlock n)} (hperm : left.Perm right) : (List.map edgeOfDart (sequenceWord left)).Perm (List.map edgeOfDart (sequenceWord right))

Permuting completed blocks preserves the unoriented edge-occurrence multiset.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.CompletedBlock.sequenceWord_isSurfaceValid_of_perm {n : ℕ} {left right : List (CompletedBlock n)} (hperm : left.Perm right) (valid : (Dyck.oneFace (sequenceWord left)).IsSurfaceValid) : (Dyck.oneFace (sequenceWord right)).IsSurfaceValid

Surface validity transports across a permutation of completed blocks.

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.isBoundary {n : ℕ} : CompletedBlock n → Bool

Boolean classifier for completed boundary-loop blocks.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.isBoundary x✝ = false

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.isCrosscap {n : ℕ} : CompletedBlock n → Bool

Boolean classifier for completed crosscap blocks.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.isCrosscap x✝ = false

@[reducible, inline]

abbrev LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.isHandle {n : ℕ} : CompletedBlock n → Bool

Boolean classifier for completed handle blocks.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.isHandle x✝ = false

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

Closed-surface blocks, retaining their original relative order.

Equations

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

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

Boundary-loop blocks, retaining their original relative order.

Equations

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

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

Stable partition with every boundary-loop block placed last.

Equations

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

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

Replace every completed handle block by the two crosscap blocks contributed in the presence of a fixed ambient crosscap.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.orientableTargetNames (p n : ℕ) : List (NormalForm.OrientableEdge p n)

Canonical orientable edge names in the same order as the canonical handle and boundary blocks.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.nonOrientableTargetNames (p n : ℕ) : List (NormalForm.NonOrientableEdge p n)

Canonical nonorientable edge names in crosscap-then-boundary order.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.orientableTargetNames_nodup (p n : ℕ) : (orientableTargetNames p n).Nodup

The canonical orientable name enumeration contains no duplicate edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.mem_orientableTargetNames (p n : ℕ) (edge : NormalForm.OrientableEdge p n) : edge ∈ orientableTargetNames p n

Every canonical orientable edge occurs in its name enumeration.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.nonOrientableTargetNames_nodup (p n : ℕ) : (nonOrientableTargetNames p n).Nodup

The canonical nonorientable name enumeration contains no duplicate edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.mem_nonOrientableTargetNames (p n : ℕ) (edge : NormalForm.NonOrientableEdge p n) : edge ∈ nonOrientableTargetNames p n

Every canonical nonorientable edge occurs in its name enumeration.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.orientableTargetNames_length (p n : ℕ) : (orientableTargetNames p n).length = 2 * p + 2 * n

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.nonOrientableTargetNames_length (p n : ℕ) : (nonOrientableTargetNames p n).length = p + 2 * n

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.boundariesLast_perm {n : ℕ} (blocks : List (CompletedBlock n)) : (boundariesLast blocks).Perm blocks

The stable boundary partition is a permutation of the original block sequence.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.boundariesLastInContext_perm {n : ℕ} (before blocks after : List (CompletedBlock n)) : (before ++ boundariesLast blocks ++ after).Perm (before ++ blocks ++ after)

Boundary partitioning remains a permutation in arbitrary list context.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.crosscapCount_eq_countP {n : ℕ} (blocks : List (CompletedBlock n)) : CompletedBlock.crosscapCount blocks = List.countP isCrosscap blocks

The recursive crosscap count is the corresponding Boolean list count.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.handleCount_eq_countP {n : ℕ} (blocks : List (CompletedBlock n)) : CompletedBlock.handleCount blocks = List.countP isHandle blocks

The recursive handle count is the corresponding Boolean list count.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.boundaryCount_eq_countP {n : ℕ} (blocks : List (CompletedBlock n)) : CompletedBlock.boundaryCount blocks = List.countP isBoundary blocks

The recursive boundary count is the corresponding Boolean list count.

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

The distinct-name spine has one name per crosscap, two per handle, and two per boundary loop.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.counts_eq_of_perm {n : ℕ} {left right : List (CompletedBlock n)} (hperm : left.Perm right) : CompletedBlock.crosscapCount left = CompletedBlock.crosscapCount right ∧ CompletedBlock.handleCount left = CompletedBlock.handleCount right ∧ CompletedBlock.boundaryCount left = CompletedBlock.boundaryCount right

Block permutation preserves all three normal-form block counts.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.normalForm_eq_of_perm {n : ℕ} {left right : List (CompletedBlock n)} (hperm : left.Perm right) : CompletedBlock.normalForm left = CompletedBlock.normalForm right

Permuting completed blocks does not change the selected normal form.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.TerminalCompletedWord.allNamesMem (terminal : TerminalCompletedWord) (edge : Fin terminal.edgeCount) : edge ∈ CompletedBlock.sequenceNames terminal.blocks

Ordinary validity forces every ambient Fin edge to occur in the terminal name spine.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.edgeEquivOfNameLists {Source : Type u_1} {Target : Type u_2} [DecidableEq Source] [DecidableEq Target] (sourceNames : List Source) (targetNames : List Target) (sourceNodup : sourceNames.Nodup) (sourceAll : ∀ (source : Source), source ∈ sourceNames) (targetNodup : targetNames.Nodup) (targetAll : ∀ (target : Target), target ∈ targetNames) (length_eq : sourceNames.length = targetNames.length) : Source ≃ Target

Equivalence obtained by pairing two duplicate-free exhaustive name enumerations position by position.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.map_edgeEquivOfNameLists {Source : Type u_1} {Target : Type u_2} [DecidableEq Source] [DecidableEq Target] (sourceNames : List Source) (targetNames : List Target) (sourceNodup : sourceNames.Nodup) (sourceAll : ∀ (source : Source), source ∈ sourceNames) (targetNodup : targetNames.Nodup) (targetAll : ∀ (target : Target), target ∈ targetNames) (length_eq : sourceNames.length = targetNames.length) : List.map (⇑(edgeEquivOfNameLists sourceNames targetNames sourceNodup sourceAll targetNodup targetAll length_eq)) sourceNames = targetNames

The enumeration equivalence maps the entire source name list to the target list exactly.

inductive LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.BlockKind : Type

Shape of one completed normal-form block.

• crosscap : BlockKind
• handle : BlockKind
• boundary : BlockKind

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.instDecidableEqBlockKind : DecidableEq BlockKind

Equations

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

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.instReprBlockKind : Repr BlockKind

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.instReprBlockKind.repr : BlockKind → ℕ → Std.Format

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.blockKind {n : ℕ} : CompletedBlock n → BlockKind

Forget the edge names and signs of one completed block.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.blockKinds {n : ℕ} (blocks : List (CompletedBlock n)) : List BlockKind

Shape sequence of a completed block word.

Equations

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

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

Final orientation bit assigned to each edge name by its unique completed block.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.reverseForBlocks [] x✝ = false

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.normalizedBlockWord {n : ℕ} {Edge : Type u_1} (edgeEquiv : Fin n ≃ Edge) : CompletedBlock n → List (SurfaceCellComplex.SignedDart Edge)

Positively normalized spelling of one completed block after applying an edge equivalence.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.normalizedSequenceWord {n : ℕ} {Edge : Type u_1} (edgeEquiv : Fin n ≃ Edge) : List (CompletedBlock n) → List (SurfaceCellComplex.SignedDart Edge)

Positively normalize a full completed block sequence.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.normalizedSequenceWord edgeEquiv [] = []

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.wordFromKinds {Edge : Type u_1} : List BlockKind → List Edge → List (SurfaceCellComplex.SignedDart Edge)

Reconstruct a positively oriented block word from a shape list and its flat edge-name spine. Malformed shape/name pairs are assigned the empty word; completed block sequences always land in the exact-shape cases.

Equations

• One or more equations did not get rendered due to their size.
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.wordFromKinds [] x✝ = []
• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.wordFromKinds x✝¹ x✝ = []

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.normalizedSequenceWord_eq_wordFromKinds {n : ℕ} {Edge : Type u_1} (edgeEquiv : Fin n ≃ Edge) (blocks : List (CompletedBlock n)) : normalizedSequenceWord edgeEquiv blocks = wordFromKinds (blockKinds blocks) (List.map (⇑edgeEquiv) (CompletedBlock.sequenceNames blocks))

Positive normalization is determined entirely by the block shapes and mapped name spine.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.blockKinds_boundaryBlocks {n : ℕ} (blocks : List (CompletedBlock n)) : blockKinds (boundaryBlocks blocks) = List.replicate (CompletedBlock.boundaryCount blocks) BlockKind.boundary

Filtering out the boundary blocks leaves exactly one boundary shape per boundary count.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.blockKinds_closedBlocks_of_crosscapCount_eq_zero {n : ℕ} (blocks : List (CompletedBlock n)) (hzero : CompletedBlock.crosscapCount blocks = 0) : blockKinds (closedBlocks blocks) = List.replicate (CompletedBlock.handleCount blocks) BlockKind.handle

With no crosscaps, the closed portion consists of exactly the counted handles.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.blockKinds_closedBlocks_of_handleCount_eq_zero {n : ℕ} (blocks : List (CompletedBlock n)) (hzero : CompletedBlock.handleCount blocks = 0) : blockKinds (closedBlocks blocks) = List.replicate (CompletedBlock.crosscapCount blocks) BlockKind.crosscap

With no handles, the closed portion consists of exactly the counted crosscaps.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.blockKinds_boundariesLast_of_crosscapCount_eq_zero {n : ℕ} (blocks : List (CompletedBlock n)) (hzero : CompletedBlock.crosscapCount blocks = 0) : blockKinds (boundariesLast blocks) = List.replicate (CompletedBlock.handleCount blocks) BlockKind.handle ++ List.replicate (CompletedBlock.boundaryCount blocks) BlockKind.boundary

After stable boundary partitioning, an orientable block list has exactly the canonical handle-then-boundary shape.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.blockKinds_boundariesLast_of_handleCount_eq_zero {n : ℕ} (blocks : List (CompletedBlock n)) (hzero : CompletedBlock.handleCount blocks = 0) : blockKinds (boundariesLast blocks) = List.replicate (CompletedBlock.crosscapCount blocks) BlockKind.crosscap ++ List.replicate (CompletedBlock.boundaryCount blocks) BlockKind.boundary

After stable boundary partitioning, a handle-free block list has exactly the canonical crosscap-then-boundary shape.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.wordFromKinds_handles_append {Index : Type u_1} {Edge : Type u_2} (indices : List Index) (first second : Index → Edge) (kinds : List BlockKind) (names : List Edge) : wordFromKinds (List.replicate indices.length BlockKind.handle ++ kinds) ((List.map (fun (i : Index) => [first i, second i]) indices).flatten ++ names) = (List.map (fun (i : Index) => [SurfaceCellComplex.SignedDart.pos (first i), SurfaceCellComplex.SignedDart.pos (second i), SurfaceCellComplex.SignedDart.neg (first i), SurfaceCellComplex.SignedDart.neg (second i)]) indices).flatten ++ wordFromKinds kinds names

Consume an arbitrary list of named handle blocks before a remaining shape/name context.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.wordFromKinds_crosscaps_append {Index : Type u_1} {Edge : Type u_2} (indices : List Index) (edge : Index → Edge) (kinds : List BlockKind) (names : List Edge) : wordFromKinds (List.replicate indices.length BlockKind.crosscap ++ kinds) ((List.map (fun (i : Index) => [edge i]) indices).flatten ++ names) = (List.map (fun (i : Index) => [SurfaceCellComplex.SignedDart.pos (edge i), SurfaceCellComplex.SignedDart.pos (edge i)]) indices).flatten ++ wordFromKinds kinds names

Consume an arbitrary list of named crosscap blocks before a remaining shape/name context.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.wordFromKinds_boundaries {Index : Type u_1} {Edge : Type u_2} (indices : List Index) (carrier hole : Index → Edge) : wordFromKinds (List.replicate indices.length BlockKind.boundary) (List.map (fun (i : Index) => [carrier i, hole i]) indices).flatten = (List.map (fun (i : Index) => [SurfaceCellComplex.SignedDart.pos (carrier i), SurfaceCellComplex.SignedDart.pos (hole i), SurfaceCellComplex.SignedDart.neg (carrier i)]) indices).flatten

Consume a complete list of named boundary blocks.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.wordFromKinds_orientableTarget (p n : ℕ) : wordFromKinds (List.replicate p BlockKind.handle ++ List.replicate n BlockKind.boundary) (orientableTargetNames p n) = NormalForm.orientableBoundaryWord p n

The canonical orientable name spine and shape list reconstruct the existing canonical word exactly.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.wordFromKinds_nonOrientableTarget (p n : ℕ) : wordFromKinds (List.replicate p BlockKind.crosscap ++ List.replicate n BlockKind.boundary) (nonOrientableTargetNames p n) = NormalForm.nonOrientableBoundaryWord p n

The canonical nonorientable name spine and shape list reconstruct the existing canonical word exactly.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.reverseForBlocks_cons_of_mem_tail {n : ℕ} (block : CompletedBlock n) (blocks : List (CompletedBlock n)) (edge : Fin n) (hdisjoint : ∀ head ∈ block.names, ∀ tail ∈ CompletedBlock.sequenceNames blocks, head ≠ tail) (hedge : edge ∈ CompletedBlock.sequenceNames blocks) : reverseForBlocks (block :: blocks) edge = reverseForBlocks blocks edge

A name belonging to the tail is not captured by the head block's orientation lookup.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.map_sequenceWord_signedRelabeling_normalized {n : ℕ} {Edge : Type u_1} (edgeEquiv : Fin n ≃ Edge) (blocks : List (CompletedBlock n)) (hnames : (CompletedBlock.sequenceNames blocks).Nodup) : List.map (signedRelabeling edgeEquiv (reverseForBlocks blocks)).mapDart (CompletedBlock.sequenceWord blocks) = normalizedSequenceWord edgeEquiv blocks

The signed relabeling selected by the unique block-name spine positively normalizes every completed block.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.orientableOrderedResult (terminal : TerminalCompletedWord) (hcrosscap : CompletedBlock.crosscapCount terminal.blocks = 0) (hshape : blockKinds terminal.blocks = List.replicate (CompletedBlock.handleCount terminal.blocks) BlockKind.handle ++ List.replicate (CompletedBlock.boundaryCount terminal.blocks) BlockKind.boundary) : NormalizationResult terminal.validPresentation

An already ordered orientable completed word relabels exactly to the existing canonical orientable finite-cyclic presentation.

Equations

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

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.nonOrientableOrderedResult (terminal : TerminalCompletedWord) (hhandle : CompletedBlock.handleCount terminal.blocks = 0) (hcrosscap : CompletedBlock.crosscapCount terminal.blocks ≠ 0) (hshape : blockKinds terminal.blocks = List.replicate (CompletedBlock.crosscapCount terminal.blocks) BlockKind.crosscap ++ List.replicate (CompletedBlock.boundaryCount terminal.blocks) BlockKind.boundary) : NormalizationResult terminal.validPresentation

An already ordered nonorientable completed word relabels exactly to the existing canonical nonorientable finite-cyclic presentation.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.handlesToCrosscaps_sequenceNames_perm {n : ℕ} (blocks : List (CompletedBlock n)) : (CompletedBlock.sequenceNames (handlesToCrosscaps blocks)).Perm (CompletedBlock.sequenceNames blocks)

Handle conversion merely permutes the distinct edge-name spine.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.handlesToCrosscaps_sequenceEdgeWord_perm {n : ℕ} (blocks : List (CompletedBlock n)) : (List.map edgeOfDart (CompletedBlock.sequenceWord (handlesToCrosscaps blocks))).Perm (List.map edgeOfDart (CompletedBlock.sequenceWord blocks))

Handle conversion preserves the unoriented edge-occurrence multiset of the exact word.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.handleCount_handlesToCrosscaps_eq_zero {n : ℕ} (blocks : List (CompletedBlock n)) : CompletedBlock.handleCount (handlesToCrosscaps blocks) = 0

Converting all handles produces no remaining handle block.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.crosscapCount_handlesToCrosscaps {n : ℕ} (blocks : List (CompletedBlock n)) : CompletedBlock.crosscapCount (handlesToCrosscaps blocks) = CompletedBlock.crosscapCount blocks + 2 * CompletedBlock.handleCount blocks

Each converted handle contributes exactly two completed crosscaps.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.boundaryCount_handlesToCrosscaps {n : ℕ} (blocks : List (CompletedBlock n)) : CompletedBlock.boundaryCount (handlesToCrosscaps blocks) = CompletedBlock.boundaryCount blocks

Handle conversion leaves the number of boundary-loop blocks unchanged.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.exists_convertPositiveAnchorHandle {n : ℕ} (anchor first second : Fin n) (before after : List (CompletedBlock n)) (hnames : (CompletedBlock.sequenceNames (CompletedBlock.crosscap anchor false :: before ++ CompletedBlock.handle first second :: after)).Nodup) (validSource : (Dyck.oneFace (CompletedBlock.sequenceWord (CompletedBlock.crosscap anchor false :: before ++ CompletedBlock.handle first second :: after))).IsSurfaceValid) : ∃ (validTarget : (Dyck.oneFace (CompletedBlock.sequenceWord (CompletedBlock.crosscap anchor false :: before ++ CompletedBlock.crosscap second false :: CompletedBlock.crosscap first false :: after))).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace (CompletedBlock.sequenceWord (CompletedBlock.crosscap anchor false :: before ++ CompletedBlock.handle first second :: after)), valid := validSource } { presentation := Dyck.oneFace (CompletedBlock.sequenceWord (CompletedBlock.crosscap anchor false :: before ++ CompletedBlock.crosscap second false :: CompletedBlock.crosscap first false :: after)), valid := validTarget }

Convert one displayed handle in the presence of a positive anchor crosscap.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.exists_convertHandlesAfterAnchor {n : ℕ} (anchor : Fin n) (before remaining : List (CompletedBlock n)) (hnames : (CompletedBlock.sequenceNames (CompletedBlock.crosscap anchor false :: before ++ remaining)).Nodup) (validSource : (Dyck.oneFace (CompletedBlock.sequenceWord (CompletedBlock.crosscap anchor false :: before ++ remaining))).IsSurfaceValid) : ∃ (validTarget : (Dyck.oneFace (CompletedBlock.sequenceWord (CompletedBlock.crosscap anchor false :: before ++ handlesToCrosscaps remaining))).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace (CompletedBlock.sequenceWord (CompletedBlock.crosscap anchor false :: before ++ remaining)), valid := validSource } { presentation := Dyck.oneFace (CompletedBlock.sequenceWord (CompletedBlock.crosscap anchor false :: before ++ handlesToCrosscaps remaining)), valid := validTarget }

Recursively convert every handle following a fixed positive anchor crosscap.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.exists_crosscap_decomposition {n : ℕ} (blocks : List (CompletedBlock n)) (hcrosscap : CompletedBlock.crosscapCount blocks ≠ 0) : ∃ (before : List (CompletedBlock n)) (anchor : Fin n) (negative : Bool) (after : List (CompletedBlock n)), blocks = before ++ CompletedBlock.crosscap anchor negative :: after

Expose one completed crosscap whenever the recursive crosscap count is nonzero.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.negativeCrosscapHeadSignedIso {n : ℕ} (anchor : Fin n) (tail : List (CompletedBlock n)) (hanchorTail : anchor ∉ List.map edgeOfDart (CompletedBlock.sequenceWord tail)) : (Dyck.oneFace (CompletedBlock.sequenceWord (CompletedBlock.crosscap anchor true :: tail))).SignedPresentationIso (Dyck.oneFace (CompletedBlock.sequenceWord (CompletedBlock.crosscap anchor false :: tail)))

Reverse a negative crosscap at the head of a completed block sequence.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.exists_normalizeCrosscapHeadOrientation {n : ℕ} (anchor : Fin n) (negative : Bool) (tail : List (CompletedBlock n)) (hnames : (CompletedBlock.sequenceNames (CompletedBlock.crosscap anchor negative :: tail)).Nodup) (validSource : (Dyck.oneFace (CompletedBlock.sequenceWord (CompletedBlock.crosscap anchor negative :: tail))).IsSurfaceValid) : ∃ (validTarget : (Dyck.oneFace (CompletedBlock.sequenceWord (CompletedBlock.crosscap anchor false :: tail))).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace (CompletedBlock.sequenceWord (CompletedBlock.crosscap anchor negative :: tail)), valid := validSource } { presentation := Dyck.oneFace (CompletedBlock.sequenceWord (CompletedBlock.crosscap anchor false :: tail)), valid := validTarget }

Normalize the sign of a displayed head crosscap without changing the remaining block word.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.CrosscapConversionResult (terminal : TerminalCompletedWord) : Type

Result of converting every handle after choosing an existing crosscap anchor.

• target : TerminalCompletedWord

  The target declaration.

• equivalent : NormalizationEquivalent terminal.validPresentation self.target.validPresentation
• handleCount_eq_zero : CompletedBlock.handleCount self.target.blocks = 0
• crosscapCount_eq : CompletedBlock.crosscapCount self.target.blocks = CompletedBlock.crosscapCount terminal.blocks + 2 * CompletedBlock.handleCount terminal.blocks
• boundaryCount_eq : CompletedBlock.boundaryCount self.target.blocks = CompletedBlock.boundaryCount terminal.blocks

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.CrosscapDecomposition {n : ℕ} (blocks : List (CompletedBlock n)) : Type

Type-valued crosscap decomposition used by the constructive conversion result.

• before : List (CompletedBlock n)

  The before declaration.

• anchor : Fin n

  The anchor declaration.

• negative : Bool

  The negative declaration.

• after : List (CompletedBlock n)

  The after declaration.

• blocks_eq : blocks = self.before ++ CompletedBlock.crosscap self.anchor self.negative :: self.after

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.chooseCrosscapDecomposition {n : ℕ} (blocks : List (CompletedBlock n)) (hcrosscap : CompletedBlock.crosscapCount blocks ≠ 0) : CrosscapDecomposition blocks

Select one crosscap decomposition from a nonzero crosscap count.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.chooseCrosscapDecomposition blocks hcrosscap = Classical.choice ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.convertHandlesOfCrosscap (terminal : TerminalCompletedWord) (hcrosscap : CompletedBlock.crosscapCount terminal.blocks ≠ 0) : CrosscapConversionResult terminal

In the presence of a crosscap, rotate one crosscap to the head, normalize its sign, and convert every handle into two additional crosscaps.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.boundaryContextWord {n : ℕ} (before after : List (SurfaceCellComplex.SignedDart (Fin n))) (carrier hole : Fin n) (carrierNegative holeNegative : Bool) : List (SurfaceCellComplex.SignedDart (Fin n))

A raw one-face context containing one completed boundary loop.

Equations

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

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.negativeBoundaryContextSignedIso {n : ℕ} (before after : List (SurfaceCellComplex.SignedDart (Fin n))) (carrier hole : Fin n) (holeNegative : Bool) (hcarrierHole : carrier ≠ hole) (hcarrierBefore : carrier ∉ List.map edgeOfDart before) (hcarrierAfter : carrier ∉ List.map edgeOfDart after) : (Dyck.oneFace (boundaryContextWord before after carrier hole true holeNegative)).SignedPresentationIso (Dyck.oneFace (boundaryContextWord before after carrier hole false holeNegative))

Reversing only a boundary carrier identifies its negative- and positive-carrier spellings while fixing a context that avoids that carrier.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.exists_commutePositiveBoundaryAdjacent {n : ℕ} (before after : List (CompletedBlock n)) (carrier hole : Fin n) (holeNegative : Bool) (block : CompletedBlock n) (hcarrierHole : carrier ≠ hole) (hcarrierBefore : carrier ∉ List.map edgeOfDart (CompletedBlock.sequenceWord before)) (hcarrierBlock : carrier ∉ List.map edgeOfDart block.word) (hcarrierAfter : carrier ∉ List.map edgeOfDart (CompletedBlock.sequenceWord after)) (validSource : (Dyck.oneFace (CompletedBlock.sequenceWord (before ++ CompletedBlock.boundary carrier hole false holeNegative :: block :: after))).IsSurfaceValid) : ∃ (validTarget : (Dyck.oneFace (CompletedBlock.sequenceWord (before ++ block :: CompletedBlock.boundary carrier hole false holeNegative :: after))).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace (CompletedBlock.sequenceWord (before ++ CompletedBlock.boundary carrier hole false holeNegative :: block :: after)), valid := validSource } { presentation := Dyck.oneFace (CompletedBlock.sequenceWord (before ++ block :: CompletedBlock.boundary carrier hole false holeNegative :: after)), valid := validTarget }

Commute one positive-carrier boundary loop past the following completed block, in arbitrary cyclic context.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.exists_commuteBoundaryAdjacent {n : ℕ} (before after : List (CompletedBlock n)) (carrier hole : Fin n) (carrierNegative holeNegative : Bool) (block : CompletedBlock n) (hcarrierHole : carrier ≠ hole) (hcarrierBefore : carrier ∉ List.map edgeOfDart (CompletedBlock.sequenceWord before)) (hcarrierBlock : carrier ∉ List.map edgeOfDart block.word) (hcarrierAfter : carrier ∉ List.map edgeOfDart (CompletedBlock.sequenceWord after)) (validSource : (Dyck.oneFace (CompletedBlock.sequenceWord (before ++ CompletedBlock.boundary carrier hole carrierNegative holeNegative :: block :: after))).IsSurfaceValid) : ∃ (validTarget : (Dyck.oneFace (CompletedBlock.sequenceWord (before ++ block :: CompletedBlock.boundary carrier hole carrierNegative holeNegative :: after))).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace (CompletedBlock.sequenceWord (before ++ CompletedBlock.boundary carrier hole carrierNegative holeNegative :: block :: after)), valid := validSource } { presentation := Dyck.oneFace (CompletedBlock.sequenceWord (before ++ block :: CompletedBlock.boundary carrier hole carrierNegative holeNegative :: after)), valid := validTarget }

Commute a completed boundary loop of either carrier orientation past the following block.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.exists_commuteBoundaryAdjacent_of_namesNodup {n : ℕ} (before after : List (CompletedBlock n)) (carrier hole : Fin n) (carrierNegative holeNegative : Bool) (block : CompletedBlock n) (hnames : (CompletedBlock.sequenceNames (before ++ CompletedBlock.boundary carrier hole carrierNegative holeNegative :: block :: after)).Nodup) (validSource : (Dyck.oneFace (CompletedBlock.sequenceWord (before ++ CompletedBlock.boundary carrier hole carrierNegative holeNegative :: block :: after))).IsSurfaceValid) : ∃ (validTarget : (Dyck.oneFace (CompletedBlock.sequenceWord (before ++ block :: CompletedBlock.boundary carrier hole carrierNegative holeNegative :: after))).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace (CompletedBlock.sequenceWord (before ++ CompletedBlock.boundary carrier hole carrierNegative holeNegative :: block :: after)), valid := validSource } { presentation := Dyck.oneFace (CompletedBlock.sequenceWord (before ++ block :: CompletedBlock.boundary carrier hole carrierNegative holeNegative :: after)), valid := validTarget }

The duplicate-free block invariant supplies every freshness condition needed by an adjacent boundary commute.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.exists_moveBoundaryAcross {n : ℕ} (before middle after : List (CompletedBlock n)) (carrier hole : Fin n) (carrierNegative holeNegative : Bool) (hnames : (CompletedBlock.sequenceNames (before ++ CompletedBlock.boundary carrier hole carrierNegative holeNegative :: middle ++ after)).Nodup) (validSource : (Dyck.oneFace (CompletedBlock.sequenceWord (before ++ CompletedBlock.boundary carrier hole carrierNegative holeNegative :: middle ++ after))).IsSurfaceValid) : ∃ (validTarget : (Dyck.oneFace (CompletedBlock.sequenceWord (before ++ middle ++ CompletedBlock.boundary carrier hole carrierNegative holeNegative :: after))).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace (CompletedBlock.sequenceWord (before ++ CompletedBlock.boundary carrier hole carrierNegative holeNegative :: middle ++ after)), valid := validSource } { presentation := Dyck.oneFace (CompletedBlock.sequenceWord (before ++ middle ++ CompletedBlock.boundary carrier hole carrierNegative holeNegative :: after)), valid := validTarget }

Commute one completed boundary loop across an arbitrary finite block interval.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.exists_sortBoundariesInContext {n : ℕ} (before blocks after : List (CompletedBlock n)) (hnames : (CompletedBlock.sequenceNames (before ++ blocks ++ after)).Nodup) (validSource : (Dyck.oneFace (CompletedBlock.sequenceWord (before ++ blocks ++ after))).IsSurfaceValid) : ∃ (validTarget : (Dyck.oneFace (CompletedBlock.sequenceWord (before ++ boundariesLast blocks ++ after))).IsSurfaceValid), NormalizationEquivalent { presentation := Dyck.oneFace (CompletedBlock.sequenceWord (before ++ blocks ++ after)), valid := validSource } { presentation := Dyck.oneFace (CompletedBlock.sequenceWord (before ++ boundariesLast blocks ++ after)), valid := validTarget }

Stably partition every completed boundary loop behind all closed-surface blocks, in arbitrary cyclic context.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.boundariesLastWord (terminal : TerminalCompletedWord) : TerminalCompletedWord

The stable boundary partition as another completed terminal word.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.boundariesLastWord_normalForm (terminal : TerminalCompletedWord) : (boundariesLastWord terminal).normalForm = terminal.normalForm

Boundary sorting preserves the exact normal form selected by block counts.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.normalizationEquivalent_boundariesLastWord (terminal : TerminalCompletedWord) : NormalizationEquivalent terminal.validPresentation (boundariesLastWord terminal).validPresentation

Every completed terminal word is normalization-equivalent to its stable boundary partition.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.crosscapConversionResult_normalForm_eq (terminal : TerminalCompletedWord) (hcrosscap : CompletedBlock.crosscapCount terminal.blocks ≠ 0) (conversion : CrosscapConversionResult terminal) : conversion.target.normalForm = terminal.normalForm

Handle conversion preserves the exact normal form selected by the original nonorientable completed word.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.terminalCompletedNormalizer : TerminalCompletedNormalizer

The completed-block terminal seam: stable-sort boundary blocks, convert all handles when a crosscap is present, normalize every edge orientation, and relabel positionally to the single canonical finite-cyclic presentation selected by TerminalCompletedWord.normalForm.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.terminalMarkedNormalizer : TerminalMarkedNormalizer

The fully discharged token-level terminal normalizer consumed by the terminating marked-word recursion.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.WordReduction.Pairing.TerminalNormalization.terminalMarkedNormalizer = ⋯.toTerminalMarkedNormalizer

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.normalizeConnectedToCanonical (P : ValidPresentation) (connectedP : P.presentation.IsConnected) : NormalizationResult P

Normalize any valid connected finite-cyclic surface presentation to the one canonical presentation selected by an admissible NormalForm.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.exists_admissible_normalForm_polygonallyEquivalent (P : FiniteCyclicPresentation) (validP : P.IsSurfaceValid) (connectedP : P.IsConnected) : ∃ (N : NormalForm) (hN : N.IsEvalAdmissible), P.PolygonallyEquivalent N.canonicalPresentation validP ⋯

Universal Gallier--Xu normalization theorem at the faithful polygonal-realization interface: every surface-valid connected finite-cyclic presentation is polygonally equivalent to the existing canonical presentation of an Eval-admissible normal form.