Faithful normal-form classification

This file composes the Gallier--Xu normalization of a valid connected finite-cyclic presentation with the exact realization homeomorphisms for the three canonical endpoints. Every type in this chain is a faithful polygonal quotient.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.hasEvalRepresentative (P : FiniteCyclicPresentation) (validP : P.IsSurfaceValid) (connectedP : P.IsConnected) : Nonempty (P.PolygonalRealization validP ≃ₜ SphereRepresentative) ∨ ∃ (p : ℕ) (n : ℕ), (1 ≤ p ∨ 1 ≤ n) ∧ Nonempty (P.PolygonalRealization validP ≃ₜ Quot (OrientableRel p n)) ∨ 1 ≤ p ∧ Nonempty (P.PolygonalRealization validP ≃ₜ Quot (NonOrientableRel p n))

A valid connected finite-cyclic presentation has one of the exact Eval representatives.

The proof first normalizes to NormalForm.canonicalPresentation, preserving the polygonal realization, and then uses the corresponding sphere, orientable, or nonorientable endpoint homeomorphism.