Realization invariance for finite cyclic move closures

This file closes the geometric proof obligations parameterizing FiniteCyclicMoves. Signed presentation isomorphisms, P1 subdivisions, and genuine P2 face subdivisions all preserve the faithful polygonal quotient. Consequently, clients of directed chains and common-subdivision certificates do not need to pass the primitive invariance proofs explicitly.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.subdivisionStep_preservesPolygonalRealization : SubdivisionStep.PreservesPolygonalRealization

Every elementary directed subdivision step preserves the faithful polygonal realization.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.Subdivides.toPolygonallyEquivalent {P Q : FiniteCyclicPresentation} (hPQ : P.Subdivides Q) (validP : P.IsSurfaceValid) (validQ : Q.IsSurfaceValid) : P.PolygonallyEquivalent Q validP validQ

A directed chain of signed isomorphisms and P1/P2 subdivisions preserves the faithful polygonal realization.

theorem LeanEval.Topology.ClassificationOfSurfaces.FiniteCyclicPresentation.HasCommonSubdivision.toPolygonallyEquivalent {P Q : FiniteCyclicPresentation} (hPQ : P.HasCommonSubdivision Q) (validP : P.IsSurfaceValid) (validQ : Q.IsSurfaceValid) : P.PolygonallyEquivalent Q validP validQ

A common directed subdivision gives a homeomorphism of the two faithful polygonal realizations.