Canonical output of finite-cyclic normalization

This file fixes the output type of the Gallier--Xu recursion before that recursion is assembled. A result lands only at the existing NormalForm.canonicalPresentation; it cannot introduce a second project-owned spelling of the Eval representatives.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.canonicalValidPresentation (N : NormalForm) (hN : N.IsEvalAdmissible) : ValidPresentation

The validity-bundled canonical presentation selected by an admissible normal form.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.canonicalValidPresentation N hN = { presentation := N.canonicalPresentation, valid := ⋯ }

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.canonicalValidPresentation_presentation (N : NormalForm) (hN : N.IsEvalAdmissible) : (canonicalValidPresentation N hN).presentation = N.canonicalPresentation

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

Certified output of the finite-cyclic Gallier--Xu normalization.

The dependent admissibility field supplies ordinary validity for the canonical endpoint, and the equivalence field records the entire validity-safe move chain.

• normalForm : NormalForm

  The normalForm declaration.

• admissible : self.normalForm.IsEvalAdmissible
• equivalent : NormalizationEquivalent P (canonicalValidPresentation self.normalForm ⋯)

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationResult.canonical (N : NormalForm) (hN : N.IsEvalAdmissible) : NormalizationResult (canonicalValidPresentation N hN)

A canonical presentation is already normalized.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationResult.canonical N hN = { normalForm := N, admissible := hN, equivalent := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationResult.ofEquivalent {P Q : ValidPresentation} (hPQ : NormalizationEquivalent P Q) (result : NormalizationResult Q) : NormalizationResult P

Transport a normalization result backward through a normalization equivalence.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationResult.ofEquivalent hPQ result = { normalForm := result.normalForm, admissible := ⋯, equivalent := ⋯ }

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationResult.ofSignedIso {P Q : ValidPresentation} (e : P.presentation.SignedPresentationIso Q.presentation) (result : NormalizationResult Q) : NormalizationResult P

Transport a normalization result across a signed presentation isomorphism.

Equations

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

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationResult.polygonallyEquivalent {P : ValidPresentation} (result : NormalizationResult P) : P.presentation.PolygonallyEquivalent result.normalForm.canonicalPresentation ⋯ ⋯

A normalization result gives the faithful polygonal realization equivalence to its exact canonical finite-cyclic endpoint.

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.NormalizationResult.realizationHomeomorph {P : ValidPresentation} (result : NormalizationResult P) : P.presentation.PolygonalRealization ⋯ ≃ₜ result.normalForm.canonicalPresentation.PolygonalRealization ⋯

Homeomorphism from a normalized input's faithful polygonal realization to the exact canonical finite-cyclic realization.

Equations

• result.realizationHomeomorph = Classical.choice ⋯

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Cancellation.sphereNormalizationResult (validSource : (source []).IsSurfaceValid) : NormalizationResult { presentation := source [], valid := validSource }

The terminal inverse-pair cancellation with no remaining darts yields the agreed canonical sphere presentation.

Equations

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