Documentation

LeanPool.ClassificationOfSurfaces.API

Public API map #

This file is the preferred first Lean file to read. It re-exports the completed proof and documents its main interfaces.

Eval input #

Moise--Radó triangulation route #

The triangulation route uses the faithful geometric and intrinsic-complex APIs above. Superseded experimental APIs are not part of the public surface; git history remains available for historical implementations.

Shared triangulation and cell-complex boundary #

The cell-complex adapter preserves the certified triangle-boundary incidence. The faithful finite-cyclic handoff enumerates that incidence directly and identifies its polygonal quotient with the geometric triangulation.

Shared finite surface cell complexes #

SurfaceCellComplex contains only finite incidence data. Its topology is the faithful occurrence-indexed PolygonalRealization described below.

Finite cyclic presentation layer #

This packed layer retains only finite signed face words. A signed presentation isomorphism may relabel faces, rotate individual face boundaries, and independently reverse the chosen orientation of every renamed edge. Reversal bits compose by exclusive-or. Validity, edge multiplicities, and connectivity are invariant under these operations. Each stored face also has two non-mutating oriented views: the negative view reverses the word and flips every dart, and signed presentation isomorphisms transport either view up to cyclic rotation. The original orientation-preserving PresentationIso embeds into this general layer.

The Gallier--Xu normalization recursion is complete at this interface. Every valid connected finite-cyclic presentation reaches the single existing NormalForm.canonicalPresentation for an Eval-admissible normal form, through a NormalizationEquivalent chain and hence a PolygonallyEquivalent proof. The terminal argument orders boundary blocks, converts handles to crosscaps exactly when a crosscap is present, normalizes edge orientations, and positionally relabels the result to the existing canonical words.

Gallier--Xu's exceptional one-face, zero-edge, empty-boundary sphere is represented explicitly by emptyWordSphere, without weakening ordinary IsSurfaceValid. IsGallierValid adds exactly its signed-isomorphism class as a disjunct. The P2-expanded twoMonogonSphere, with boundaries d and d⁻¹, satisfies ordinary validity and connectivity.

P1.expand implements Gallier--Xu's global edge subdivision exactly: the canonical positive occurrence becomes b c, while its negative occurrence becomes c⁻¹ b⁻¹. Contraction is a left inverse and expansion preserves and reflects cyclic rotation. Face positions are unchanged, and both subdivided edges inherit the old edge multiplicity. The construction conditionally preserves ordinary validity, connectivity, and IsGallierValid; these hypotheses are not bundled into the syntactic P1Subdivision relation. The positive orientation is canonical, while the relation's signed target isomorphism supports renamed and reoriented target edges. The finite cyclic quotient adapter realizes those face words directly as a disjoint union of standard polygonal disks modulo occurrence-level side pairings.

P2.split implements Gallier--Xu's cyclic oriented face-cut formula. Its raw cut pieces may be empty so the same construction expresses the exceptional empty-word-sphere conversion. The selected child has displayed boundary left d, the appended child has displayed boundary d⁻¹ right, and both are stored in the cut's chosen traversal orientation. Flipping the cut reverses its selected traversal and swaps its two pieces. The fresh edge has multiplicity two, old edge multiplicities are preserved, and validity, connectivity, and Gallier validity survive. The exceptional empty-word sphere presentation splits definitionally to the twoMonogonSphere presentation. P2Subdivision is the corresponding syntactic relation for nondegenerate ordinary face cuts, together with that exceptional sphere conversion, up to signed presentation isomorphism of the target.

The generic Gallier--Xu Dyck rewrite a U V a⁻¹ X ~ b V U b⁻¹ X is now an explicit common-subdivision theorem. Its two P2 splits are related by a signed isomorphism exchanging the retained distinguished edge with the fresh cutting edge. Consequently the rewrite preserves faithful polygonal realizations for ordinary-valid source and target presentations.

Gallier--Xu's cross-cap rewrite a X a Y ~ b b Y⁻¹ X reverses one child face before the second P2 merge. UnorientedPresentationIso records that independent face-traversal choice explicitly, and realizes it by cyclic disk rotations and reflections. Because the current IsSurfaceValid face-uniqueness clause is intentionally stated for stored orientations, this broader comparison takes ordinary-validity proofs for both endpoints rather than claiming to transport validity automatically.

NormalizationEquivalent is the stable chain API over validity-bundled presentations. Its primitive steps are common subdivisions, unoriented comparisons in either direction, and the proved one-sided-degenerate P2 comparison; every chain produces a faithful polygonal-realization homeomorphism. Both generic pseudo-rewrites are available as nodes in this closure. The derived-chain layer also exposes the opposite-orientation Dyck and crosscap rules, the full three-Dyck handle extraction, the four-rewrite conversion of a handle plus a crosscap into three crosscaps, and the loop-grouping specialization; all intermediate validity witnesses are constructed internally. Exact inverse-pair cancellation and two-face merging are available both as isolated word rules and in multi-face contexts with untouched faces. Their transported forms isolate arbitrary edge naming, face order, traversal orientation, and cyclic starting points behind signed presentation isomorphisms. Validity-safe marked merging now gives a total face-count recursion from every connected valid presentation to one face. A second well-founded recursion cancels all cyclic adjacent inverse pairs—including the retained merge markers—and lands either at the exact canonical sphere node or at a pair-reduced valid one-face word.

Polygonal quotient foundation #

This generic layer supports disk cells with any number of marked sides and generated side identifications. The additive cell-complex adapter now maps boundary occurrences to polygon sides and, given incidence validity plus nonempty face boundaries, generates all compatible internal pairings. Edge-orbit counts and inverse-invariance of boundary status are derived from IsSurfaceValid, not repeated as adapter assumptions. The standard one-face examples have incidence- and occurrence-validity witnesses, including the corrected length-six annulus word. The representative-carrier bridge identifies each indexed disk, and hence every one-face pre-realization, with the exact vendored closed unit disk. It records the side-coordinate formula, integral-period boundary invariance, and closure-aware quotient congruence from the polygonal generated setoid to a raw relation quotient. The one-face membership theorem characterizes compatible ordered pairings by two distinct boundary-word positions with the required status and dart equalities. Forward canonical block positions and exhaustive raw-pairing classifications for both canonical families are complete. Exact carrier coordinates, including the reversed boundary index, send all five canonical pairing families into the corresponding trusted equivalence closures. Exhaustive forward maps and constructor-by-constructor reverse maps therefore identify both generated relations, and the carrier descends to homeomorphisms from the canonical polygonal realizations to the exact trusted Eval quotients. For the sphere branch, the compatible upper/lower hemisphere map descends from the two monogons; its kernel is exactly the generated side-gluing relation, and compact-to-Hausdorff upgrades the resulting bijection to a homeomorphism with SphereRepresentative.

Gallier-Xu tail #

The canonical word families match the exact commutator, crosscap, and boundary-block patterns in the vendored relations. Their lengths, edge multiplicities, incidence validity, connectivity, and Eval-admissible occurrence pairings are certified combinatorially. Forward block-position maps and exact List.get lemmas locate every signed entry of each named handle, crosscap, and boundary block. Polygonal identifications in both families are classified exhaustively as the two directed forms of the expected handle, crosscap, or boundary-seam pairings, with singleton free-boundary darts excluded. Exact coordinate theorems transport every explicit pairing family into the trusted closures; boundary blocks use Fin.rev and integral periodicity to reconcile the benchmark's negative angles. The exhaustive classifications package those facts for arbitrary polygon generators, while the trusted relation constructors map back to named polygon pairings. The resulting bidirectional closure comparisons descend to homeomorphisms with Quot (OrientableRel p n) and Quot (NonOrientableRel p n).

The public classification theorem uses the faithful replacement route: it normalizes finite cyclic presentations, proves their polygonal realizations match the vendored quotient relations, and transports that result across the geometric-triangulation realization bridge. The combinatorial normalization layer does not mention manifold chart machinery.

Eval representatives and final theorem #

The final theorem is a short assembly proof from a geometric triangulation, through a finite cyclic presentation and Gallier-Xu normalization, to separately certified polygonal realization homeomorphisms for the vendored quotients. The C0 ChartBoundaryInvariant interface is discharged unconditionally by planar no-retraction, Brouwer's fixed-point theorem, and invariance of domain. LeanEval/SpecAudit.lean checks that the current public theorem's conclusion is the exact published Lean-Eval type over the vendored disc relations.