Stable closure for Gallier--Xu normalization chains

Directed P1/P2 chains and common subdivisions preserve ordinary validity internally. The cross-cap rewrite additionally reads one refined face backwards, and the current orientation-sensitive validity predicate is not invariant under arbitrary face reversal.

ValidPresentation therefore bundles the ordinary-validity witness at every node of a normalization chain. NormalizationStep has exactly two proof-producing seams:

• a common directed P1/P2/signed-isomorphism subdivision;
• an unoriented presentation isomorphism in either direction.

The equivalence closure composes these seams, and its realization theorem needs no extra intermediate validity arguments. This is the stable target for the remaining derived normalization chains.

structure LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ValidPresentation : Type

An ordinary-valid finite cyclic presentation, used as a node in a normalization chain.

• presentation : FiniteCyclicPresentation

  The presentation declaration.

• valid : self.presentation.IsSurfaceValid

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ValidPresentation.instCoe : Coe ValidPresentation FiniteCyclicPresentation

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ValidPresentation.ext {P Q : ValidPresentation} (h : P.presentation = Q.presentation) : P = Q

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ValidPresentation.ext_iff {P Q : ValidPresentation} : P = Q ↔ P.presentation = Q.presentation

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ValidPresentation.mk' (P : FiniteCyclicPresentation) (validP : P.IsSurfaceValid) : ValidPresentation

Package an ordinary-valid presentation.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.ValidPresentation.mk' P validP = { presentation := P, valid := validP }

inductive LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationStep : ValidPresentation → ValidPresentation → Prop

One validity-safe normalization comparison. Common subdivisions cover the P1/P2/signed closure; the second constructor covers an independent choice of face traversal in either direction.

• commonSubdivision {P Q : ValidPresentation} (h : P.presentation.HasCommonSubdivision Q.presentation) : NormalizationStep P Q
• unoriented {P Q : ValidPresentation} (h : Nonempty (P.presentation.UnorientedPresentationIso Q.presentation) ∨ Nonempty (Q.presentation.UnorientedPresentationIso P.presentation)) : NormalizationStep P Q
• oneSidedP2 {P : ValidPresentation} (cut : P.presentation.P2Cut) (honeSided : cut.left = [] ∧ 0 < cut.right.length ∨ 0 < cut.left.length ∧ cut.right = []) : NormalizationStep P { presentation := P2.split P.presentation cut, valid := ⋯ }

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationStep.ofUnorientedIso {P Q : ValidPresentation} (e : P.presentation.UnorientedPresentationIso Q.presentation) : NormalizationStep P Q

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationStep.ofUnorientedIsoSymm {P Q : ValidPresentation} (e : Q.presentation.UnorientedPresentationIso P.presentation) : NormalizationStep P Q

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationStep.ofOneSidedP2 {P : ValidPresentation} (cut : P.presentation.P2Cut) (honeSided : cut.left = [] ∧ 0 < cut.right.length ∨ 0 < cut.left.length ∧ cut.right = []) : NormalizationStep P { presentation := P2.split P.presentation cut, valid := ⋯ }

A one-sided-degenerate P2 split is a normalization step.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationStep.polygonallyEquivalent {P Q : ValidPresentation} (h : NormalizationStep P Q) : P.presentation.PolygonallyEquivalent Q.presentation ⋯ ⋯

Every normalization step preserves the faithful polygonal realization of its bundled valid endpoints.

def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationEquivalent (P Q : ValidPresentation) : Prop

Equivalence closure of validity-safe normalization comparisons.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationEquivalent.refl (P : ValidPresentation) : NormalizationEquivalent P P

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationEquivalent.ofStep {P Q : ValidPresentation} (h : NormalizationStep P Q) : NormalizationEquivalent P Q

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationEquivalent.ofCommonSubdivision {P Q : ValidPresentation} (h : P.presentation.HasCommonSubdivision Q.presentation) : NormalizationEquivalent P Q

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationEquivalent.ofSubdivides {P Q : ValidPresentation} (h : P.presentation.Subdivides Q.presentation) : NormalizationEquivalent P Q

A directed subdivision is a normalization equivalence, using its target as the common subdivision.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationEquivalent.ofSignedIso {P Q : ValidPresentation} (e : P.presentation.SignedPresentationIso Q.presentation) : NormalizationEquivalent P Q

A signed presentation isomorphism is a normalization equivalence.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationEquivalent.ofP1 {P Q : ValidPresentation} (h : P.presentation.P1Subdivision Q.presentation) : NormalizationEquivalent P Q

A P1 subdivision is a normalization equivalence.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationEquivalent.ofP2 {P Q : ValidPresentation} (h : P.presentation.P2Subdivision Q.presentation) : NormalizationEquivalent P Q

A P2 subdivision is a normalization equivalence.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationEquivalent.ofUnorientedIso {P Q : ValidPresentation} (e : P.presentation.UnorientedPresentationIso Q.presentation) : NormalizationEquivalent P Q

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationEquivalent.ofUnorientedIsoSymm {P Q : ValidPresentation} (e : Q.presentation.UnorientedPresentationIso P.presentation) : NormalizationEquivalent P Q

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationEquivalent.ofOneSidedP2 {P : ValidPresentation} (cut : P.presentation.P2Cut) (honeSided : cut.left = [] ∧ 0 < cut.right.length ∨ 0 < cut.left.length ∧ cut.right = []) : NormalizationEquivalent P { presentation := P2.split P.presentation cut, valid := ⋯ }

A one-sided-degenerate P2 split is a normalization equivalence.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationEquivalent.symm {P Q : ValidPresentation} (h : NormalizationEquivalent P Q) : NormalizationEquivalent Q P

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationEquivalent.trans {P Q R : ValidPresentation} (hPQ : NormalizationEquivalent P Q) (hQR : NormalizationEquivalent Q R) : NormalizationEquivalent P R

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationEquivalent.polygonallyEquivalent {P Q : ValidPresentation} (h : NormalizationEquivalent P Q) : P.presentation.PolygonallyEquivalent Q.presentation ⋯ ⋯

A normalization chain yields a homeomorphism of the faithful polygonal realizations of its endpoints.

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

The generic Dyck rewrite as a node in the stable normalization closure.

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

The generic cross-cap rewrite as a three-step normalization chain: split the source, reverse the right refined face, and merge to the target.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P1.contractionNormalizationEquivalent (P : FiniteCyclicPresentation) (a : P.Edge) (validP : P.IsSurfaceValid) : NormalizationEquivalent { presentation := expand P a, valid := ⋯ } { presentation := P, valid := validP }

Contract a canonical P1 expansion inside the normalization closure.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.mergeNormalizationEquivalent (P : FiniteCyclicPresentation) (cut : P.P2Cut) (hcut : cut.IsNondegenerate) (validP : P.IsSurfaceValid) : NormalizationEquivalent { presentation := split P cut, valid := ⋯ } { presentation := P, valid := validP }

Merge the two children of a nondegenerate canonical P2 split inside the normalization closure.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.oneSidedMergeNormalizationEquivalent (P : FiniteCyclicPresentation) (cut : P.P2Cut) (honeSided : cut.left = [] ∧ 0 < cut.right.length ∨ 0 < cut.left.length ∧ cut.right = []) (validP : P.IsSurfaceValid) : NormalizationEquivalent { presentation := split P cut, valid := ⋯ } { presentation := P, valid := validP }

Merge the two children of a one-sided-degenerate P2 split. This is the inverse form needed by cancellation chains, where one child is a monogon.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.P2.ordinaryMergeNormalizationEquivalent (P : FiniteCyclicPresentation) (cut : P.P2Cut) (hcut : cut.IsNondegenerate ∨ cut.left = [] ∧ 0 < cut.right.length ∨ 0 < cut.left.length ∧ cut.right = []) (validP : P.IsSurfaceValid) : NormalizationEquivalent { presentation := split P cut, valid := ⋯ } { presentation := P, valid := validP }

Merge any ordinary-valid canonical P2 split whose cut is either nondegenerate or one-sided-degenerate.