diff --git a/TauCetiRoadmap/ConformalMapping/README.md b/TauCetiRoadmap/ConformalMapping/README.md index b7201f48..2f2f780e 100644 --- a/TauCetiRoadmap/ConformalMapping/README.md +++ b/TauCetiRoadmap/ConformalMapping/README.md @@ -137,6 +137,7 @@ deliberately scoped to the conformal-mapping spine that none of them build: - **Below — `ContourIntegration` (PR #35).** Provides residues, winding numbers, the argument principle, and the global Cauchy theorem (Dixon). **L0 consumes it.** +- **Beside — `PlanarTopology`** Owns the plane topology of Jordan curves: separation, the crosscut theorem, accessibility, invariance of domain in dimension two, and the Schoenflies theorem. L2 provides that the inside of a Jordan curve is a Jordan domain - **Above — `ModularForms` (PR #47).** A 13-layer entry targeting the complex modular curves `Y(Γ)(ℂ) ≅ Γ\ℍ` (the complex-analytic versions, not the moduli-space framing). The **modular & elliptic uniformization** — including the diff --git a/TauCetiRoadmap/GeometricTopology/README.md b/TauCetiRoadmap/GeometricTopology/README.md index fd4e3252..15e4a93a 100644 --- a/TauCetiRoadmap/GeometricTopology/README.md +++ b/TauCetiRoadmap/GeometricTopology/README.md @@ -745,7 +745,7 @@ the disproof needs the genus and the rank side by side. **From Mathlib / earlier layers.** Layer 1's handlebodies (a handlebody is a boundary-sum of solid tori, built from layer 1's gluing) and boundary-gluing; `FundamentalGroup` (`Mathlib/AlgebraicTopology/FundamentalGroupoid/`) and `Group.rank` for the rank side; the -surface (closed orientable 2-manifold) classification for the splitting surface. +surface (closed orientable 2-manifold) classification for the splitting surface from [Surface Topology](../SurfaceTopology/README.md). **What to build.** - **Handlebodies** of each genus and the **Heegaard splitting** of a closed 3-manifold as @@ -845,7 +845,7 @@ groupoid. - **Triangulation of a space** in the general sense: `IsTriangulable M := ∃ K, Nonempty (|K| ≃ₜ M)`. This is the notion in Manolescu's theorem, and it is *weaker* than asking for a combinatorial or PL structure. (Moise, *Geometric Topology in Dimensions 2 and 3*, treats - the dimension-3 existence, [extract](references/moise-triangulation-dim3.md).) + the dimension-3 existence, [extract](references/moise-triangulation-dim3.md).) The dimension 2 case, Rado's theorem, is handled by the [Planar Topology](../PlanarGeometry/README.md) roadmap. - **Combinatorial manifolds via the link condition** (Kim's point, the simplicial side of PL topology). Define, recursively in dimension, a **combinatorial `n`-sphere** and **combinatorial `n`-ball** (a complex PL-homeomorphic, after subdivision, to the boundary @@ -853,7 +853,7 @@ groupoid. the combinatorial `0`-sphere (two points) and `0`-ball (one point). Then `K` is a **combinatorial `n`-manifold** if the link of every vertex is a combinatorial `(n-1)`-sphere (interior point) or `(n-1)`-ball (boundary point). This is the definition - that "has the correct links to be a manifold". + that "has the correct links to be a manifold". The generalized maps of the [Surface Topology](../SurfaceTopology/README.md) roadmap give a complementary, dart-based encoding of local manifold structure. In dimension 2 the condition is decidable and recursion is unecessary. - **The reconciliation with layer 1.** Prove that the polyhedron of a combinatorial `n`-manifold is a PL `n`-manifold in the sense of layer 1's `PLGroupoid`, and conversely that every PL manifold admits a combinatorial triangulation (Whitehead). This is the diff --git a/TauCetiRoadmap/PlanarTopology/README.md b/TauCetiRoadmap/PlanarTopology/README.md new file mode 100644 index 00000000..688bba8d --- /dev/null +++ b/TauCetiRoadmap/PlanarTopology/README.md @@ -0,0 +1,701 @@ +# Roadmap: Planar topology and the piecewise-linear structure of surfaces + +Two-dimensional topology is the last dimension in which several kinds of structure coincide without additional hypotheses. Every surface is triangulable; topological homeomorphisms between triangulated surfaces can be replaced by piecewise-linear ones; embedded arcs and simple closed curves are tame; and every topological surface has essentially unique piecewise-linear and smooth structures. The corresponding statements separate in higher dimensions: triangulations and the Hauptvermutung can fail, and wild embeddings make local flatness a genuine condition. This roadmap develops the specifically two-dimensional theorems behind that coincidence. + +That framing matters for how the results are used. These theorems are not obtained by specializing a dimension-independent theory: their proofs use planar separation, polygonal approximation, and the combinatorics of two-dimensional links. Some individual conclusions also hold in dimension three, but the full package—especially automatic tameness—is specifically two-dimensional. The *definitions* are shared with `GeometricTopology`; see the interface table below. + +The summits, in order of construction: + +1. **The Jordan curve theorem and the crosscut theorem**, with the frontier and + accessibility API that feeds into `ConformalMapping`. +2. **Radó's theorem**: every compact surface is triangulable. +3. **The two-dimensional Hauptvermutung**: homeomorphic triangulated surfaces admit + isomorphic subdivisions. Together with Radó's theorem, this makes the piecewise-linear + structure of a compact surface well defined up to PL isomorphism. +4. **The Euler characteristic** of a compact surface, well defined and a homeomorphism + invariant. +5. **The Schoenflies theorem** in its polygonal, planar, spherical, and relative forms, and + tameness of arcs and simple closed curves in a surface. +6. **Uniqueness of the piecewise-linear and smooth structures** on a compact surface. + +The companion roadmap +[SurfaceTopology](../SurfaceTopology/README.md) consumes items 2, 3, and 4 and proves the classification of compact surfaces. This roadmap is simplicial only: generalized maps, hypermaps, cellulations, and polygon words appear nowhere in it. + +Each layer below is organized around a theorem, its mathematical dependencies, and a proof route. The displayed Lean declarations are representative interfaces rather than part of the mathematical statement; they remain useful for exposing how the layers fit into Tau Ceti. + +--- + +## Relationship to other roadmaps + +### This roadmap supplies + +| Consumer | What it needs | Status there today | +|---|---|---| +| `ConformalMapping` layer 5 | plane separation for Jordan curves; `J ⊆ closure (filledHull J \ J)` | named as an open frontier item in `ConformalMapping/STATUS.md` and in the roadmap role of `TauCeti/Topology/FilledHull.lean` | +| `GeometricTopology` layer 11 | `IsTriangulable` is unconditional in dimension two; the two-dimensional Hauptvermutung | the layer states that triangulability fails in dimension five and that the Hauptvermutung is false in general, but does not currently claim dimension two | +| `GeometricTopology` layer 2 | `IsLocallyFlat` is automatic for arcs and simple closed curves in a surface | the predicate exists; the two-dimensional discharge does not | +| `GeometricTopology` layer 1 | invariance of domain in dimension two, hence chart-independence of the manifold boundary in the topological (`k = 0`) case | `isBoundaryPoint_iff_mem_frontier_range` carries the hypothesis `hk : k ≠ 0` | +| `SurfaceTopology` | Radó, the Hauptvermutung, Euler characteristic, Schoenflies, tameness | not built | + +### This roadmap consumes + +The mathematical development is intended to use the following existing definitions and +theorems rather than introduce parallel versions. + +| Item | Location | Owner | +|---|---|---| +| `Isotopy`, `Isotopic` | `TauCeti/Topology/Homotopy/Isotopy/{Basic,Comp,Prod}.lean` | `GeometricTopology` layer 1 | +| `AmbientIsotopy`, `AmbientIsotopic` | `TauCeti/Topology/Homotopy/AmbientIsotopic/{Basic,Complement,Naturality}.lean` | `GeometricTopology` layer 1 | +| `Realization`, `Face`, `faceInclusion`, `StandardSimplex` | `TauCeti/AlgebraicTopology/SimplicialComplex/Realization.lean` | `GeometricTopology` layer 11 | +| `link`, `closedStar`, `deletion` | `TauCeti/AlgebraicTopology/SimplicialComplex/LinkStar.lean` | `GeometricTopology` layer 11 | +| barycentric subdivision, `barycentricSubdivisionMap` | `TauCeti/AlgebraicTopology/SimplicialComplex/Subdivision/{Basic,Realization}.lean` | `GeometricTopology` layer 11 | +| `SimplicialMap`, `domainRestrict` | `TauCeti/AlgebraicTopology/SimplicialComplex/Maps.lean` | `GeometricTopology` layer 11 | +| `dimension` | `TauCeti/AlgebraicTopology/SimplicialComplex/Dimension.lean` | `GeometricTopology` layer 11 | +| the collapse API | `TauCeti/AlgebraicTopology/SimplicialComplex/Collapse/`, `ElementaryCollapse.lean` | `GeometricTopology` layer 11 | +| `IsTriangulable` | `TauCeti/Topology/Triangulable.lean` | `GeometricTopology` layer 11 | +| `IsLocallyFlat`, `IsSliceChart`, `IsSliceEmbedding` | `TauCeti/Geometry/Manifold/LocallyFlat/{Basic,Smooth}.lean` | `GeometricTopology` layer 2 | +| half-space boundary model, boundary charts, collars | `TauCeti/Geometry/Manifold/Boundary/{Basic,Charts,Model}.lean`, `Boundary/Collar/{Basic,Chart}.lean` | `GeometricTopology` layer 1 | +| `IsJordanCurve` and the arc theory | `TauCeti/Topology/JordanCurve/{Basic,Path,Separation,SmallArc,Subcontinuum}.lean` | `ConformalMapping` | +| `filledHull` | `TauCeti/Topology/FilledHull.lean` | `ConformalMapping` | +| `IsJordanDomain` | `TauCeti/Analysis/Complex/Conformal/JordanDomain.lean` | `ConformalMapping` | +| winding numbers for contours | `TauCeti/Analysis/Contour/Winding/` | `ContourIntegration` | +| `Circle` arc and metric API | `TauCeti/Topology/Circle/{Basic,Arc,Metric}.lean` | `ConformalMapping` | +| continua, local connectedness | `TauCeti/Topology/{Continuum,LocallyConnected,UniformlyLocallyConnected}.lean` | `ConformalMapping` | + +### Shared formal infrastructure needed + +- **Relative and supported isotopy** (`IsotopicRel`, ambient isotopy with prescribed support) into `TauCeti/Topology/Homotopy/`. +- **General subdivision** (a complex refining another with the same realization), stellar subdivision, and the common-subdivision theorem, into `TauCeti/AlgebraicTopology/SimplicialComplex/Subdivision/`. +- **Purity, facets, and skeleta** into `TauCeti/AlgebraicTopology/SimplicialComplex/`. +- **`IsPLMap`** in the same directory, defined by quantification over subdivisions. + + +--- + +## Mathematical objects and formalization conventions + +The following choices fix the mathematical models used in statements and keep the formal development interoperable with the surrounding Tau Ceti libraries. + +### The plane + +**Planar topology is stated over `ℂ`.** `ConformalMapping` works over `ℂ`, `Circle` lives in `ℂ`, the normal to a directed segment is `I * u`, and the exterior is handled by `z ↦ z⁻¹`. + +**Chart-level results are stated over `EuclideanSpace ℝ (Fin 2)` and `EuclideanHalfSpace 2`**, because that is Mathlib's `ModelWithCorners` vocabulary and there is no alternative. + +Layer 0 fixes one named linear isometry equivalence `ℂ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 2)`, obtained from `Complex.orthonormalBasisOneI.repr`. It is an isometry, not merely a homeomorphism, so every metric, diameter, and convexity statement transports for free. Headline theorems should be proved in one model and transported to the other, rather than developed independently twice. + +Layer 0 also fixes the sup-norm comparison `‖x‖_∞ ≤ ‖x‖ ≤ √2 · ‖x‖_∞`, which is what square-mesh arguments run on. + +### The circle + +`Circle`, the unit circle of `ℂ`, is the statement-level circle, because `TauCeti.IsJordanCurve C` is defined as `Nonempty (C ≃ₜ Circle)`. Its group structure is used when gluing two Schoenflies discs along a curve. + +`AddCircle (1 : ℝ)` is the parametrization used whenever lifting, degree, or a linear order on a lift is needed. `AddCircle.homeomorphCircle`, `Circle.exp`, and `sphereCircleHomeomorph` are the bridges; layer 0 states the round trips. + +⚠ `CircularOrder` on the topological circle has nothing to do with cyclic words. Keep them in separate namespaces with no coercion between them. + +### Surfaces + +A **topological surface** is a `ChartedSpace (EuclideanSpace ℝ (Fin 2)) M` with `T2Space M`, plus second countability where needed; a **surface with boundary** charts to `EuclideanHalfSpace 2`. Compactness plus Hausdorff plus locally Euclidean gives second countability, and layer 0 proves that rather than assuming it. + +Manifold boundary `∂M` is the set of points that are boundary points in some chart. ⚠ Chart-independence in the topological case is **not** available from `isBoundaryPoint_iff_mem_frontier_range`, which requires `k ≠ 0`. It follows from invariance of domain, proved in layer 2. Nothing in this roadmap may use `∂M` before layer 2. + +### Simplicial and PL + +Abstract simplicial complexes are Tau Ceti's (`PreAbstractSimplicialComplex` / `AbstractSimplicialComplex`, `SetLike`, `Face K := {σ : Finset ι // σ ∈ K}`, realization into `ι →₀ ℝ`). No private complex type. + +A **PL map** is defined by existential quantification over subdivisions of the domain complex, not by a triangulation. Composability then depends on the common-subdivision theorem, which is a layer 3 target. + +`IsCombinatorialSurface` is defined concretely by the link condition: every vertex link is a combinatorial circle or a combinatorial arc, and every edge lies in one or two triangles. It is *not* defined by instantiating a dimension-general recursion. If `GeometricTopology` later builds `IsCombinatorialManifold`, then equality at `n = 2` is a compatibility theorem, listed in layer 3's targets. + +### Bundled index types + +Every finite combinatorial object bundles its own index type, and every move relation is closed under isomorphism of that type before `Relation.ReflTransGen` is applied. This is stated here because it is shared with `SurfaceTopology`. + +--- + +## Layer Dependency Chart + +``` +L0 conventions + | +L1 polygonal engine + |\ + | \__ Track I (approximation and separation) + | L2 separation, crosscuts, invariance of domain + | L7 topological Schoenflies and tameness + | + \____ Track II (piecewise-linear) + L3 simplicial and PL toolkit in dimension two + L4 the PL approximation theorem + L5 Rado and the two-dimensional Hauptvermutung + L6 Euler characteristic + | + L8 uniqueness of PL and smooth structure (joins I and II) +``` + +--- + +## Layer 0: Conventions, transport, and plane pathologies + +This preliminary layer fixes the ambient models and transport lemmas used throughout the roadmap. It also contains two classical constructions showing that the hypotheses in later separation theorems are necessary. It also describes Alexander's trick. + +**From Mathlib and Tau Ceti.** `Complex.orthonormalBasisOneI`, `OrthonormalBasis.repr`, `Circle`, `AddCircle`, `AddCircle.homeomorphCircle`, `Circle.exp`, `sphereCircleHomeomorph`, `Isotopy`, `Isotopic`, `AmbientIsotopic`, `Continuum`, `LocallyConnected`. + +**Representative formal statements.** + +```lean +/-- The plane transport. An isometry, so metric statements move for free. -/ +noncomputable def planeEquiv : ℂ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 2) := + Complex.orthonormalBasisOneI.repr + +def perp (u : ℂ) : ℂ := Complex.I * u +def det (u v : ℂ) : ℝ := (starRingEnd ℂ u * v).im + +theorem det_eq_inner_perp (u v : ℂ) : det u v = inner ℝ (perp u) v +theorem norm_inf_le_norm (z : ℂ) : ‖z‖_∞ ≤ ‖z‖ +theorem norm_le_sqrt_two_norm_inf (z : ℂ) : ‖z‖ ≤ Real.sqrt 2 * ‖z‖_∞ + +/-- Compact plus Hausdorff plus locally Euclidean gives second countable. -/ +instance (priority := low) {M : Type*} [TopologicalSpace M] [CompactSpace M] [T2Space M] + [ChartedSpace (EuclideanSpace ℝ (Fin 2)) M] : SecondCountableTopology M + +/-- Isotopy relative to a subset; intended for the shared isotopy API. -/ +def IsotopicRel (A : Set X) (f g : C(X, Y)) : Prop + + +/-- Alexander's trick, extension form. A homeomorphism of the boundary sphere cones radially to a homeomorphism of the closed ball. Stated dimension-generally; only + `n = 1` is used here. -/ +noncomputable def coneExtend {n : ℕ} (h : Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1 ≃ₜ + Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1) : + Metric.closedBall (0 : EuclideanSpace ℝ (Fin n)) 1 ≃ₜ + Metric.closedBall (0 : EuclideanSpace ℝ (Fin n)) 1 + +theorem norm_coneExtend (h) (z) : ‖(coneExtend h z : _)‖ = ‖(z : _)‖ +theorem coneExtend_eqOn_sphere (h) : ∀ z ∈ Metric.sphere 0 1, coneExtend h z = h z + +/-- Alexander's trick, isotopy form. Two self-homeomorphisms of the ball that agree on the boundary are isotopic rel boundary. -/ +theorem isotopicRel_of_eqOn_sphere {n : ℕ} (f g : Metric.closedBall (0 : EuclideanSpace ℝ (Fin n)) 1 ≃ₜ + Metric.closedBall (0 : EuclideanSpace ℝ (Fin n)) 1) + (h : Set.EqOn f g (Metric.sphere 0 1)) : + IsotopicRel (Metric.sphere 0 1) f g + +/-- The PL flavor, which is what layer 4 spends: coning a PL homeomorphism of a polygon boundary over the polygon. -/ +theorem isPLMap_coneExtend (h) (hPL : IsPLMap h) : IsPLMap (coneExtend h) + + +/-- Plane pathologies: these certify that later hypotheses cannot be weakened. -/ +theorem exists_spaceFillingCurve : + ∃ f : C(unitInterval, Metric.closedBall (0 : ℂ) 1), Surjective f + +theorem exists_jordanCurve_not_rectifiable : + ∃ J : Set ℂ, IsJordanCurve J ∧ ¬ IsRectifiable J + +theorem exists_jordanCurve_volume_pos : ∃ J : Set ℂ, IsJordanCurve J ∧ 0 < volume J + + +``` +**Mathematical route and formalization notes.** + +- Alexander's trick is short but needed in three places. L4 uses the PL version to correct the 2-skeleton and fills each triangle. L7 uses the topological version when it glues the two Schoenflies discs along the curve. L8 uses the isotopy form in exists_isotopic_plHomeomorph. + +- The space-filling curve is why the Jordan curve theorem needs injectivity, and the non rectifiable curve (Koch snowflake) shows why one may not assume a curve is rectifiable. The positive measure Osgood curve is why one may not assume the curve is measure 0. +- ⚠ The Osgood construction may be deferred to layer 7 without blocking anything, if its difficult to formalize + +**Examples and mathematical checks.** The round trips for `planeEquiv`, `Circle`, and `AddCircle` are proved explicitly, and at least one metric theorem is transported through the plane equivalence. The space-filling curve is given by a concrete construction rather than by an unstructured existence assertion. + +**Natural intermediate results.** (i) plane transport and the `perp`/`det` API; (ii) circle transport; (iii) second countability and surface conventions; (iv) Alexander's trick: coneExtend, the norm identity, the isotopy form, and the PL flavour. (v) relative and supported isotopy, in the shared isotopy library; (vi) the space-filling curve; (vii) the Osgood curve. + +--- + +## Layer 1: Polygonal Foundations + +This layer includes dimension two results that are true for elementary reasons. This layer is entirely finite and produces the identity that both tracks run on. + +The organizing object is the **crossing parity** of a point against a closed polygon. The additive identity that makes the theory work is: cutting a polygonal Jordan curve by a polygonal crosscut splits it into two polygonal Jordan curves whose parities add. + +**From layer 0.** The plane, `perp`, `det`, the sup-norm comparison. +**From Tau Ceti.** `TauCeti/Analysis/Contour/Winding/` for the comparison with the analytic winding number; `Combinatorics/SimpleGraph/Acyclic` for the graph-theoretic pieces. + +**Representative formal statements.** + +```lean +structure PolygonalPath where + vertices : List ℂ + ne_nil : vertices ≠ [] + +def PolygonalPath.IsSimpleClosed (P : PolygonalPath) : Prop +def crossingParity (P : PolygonalPath) (q : ℂ) : ZMod 2 +def polygonalWinding (P : PolygonalPath) (q : ℂ) : ℤ + +theorem crossingParity_locallyConstant (P : PolygonalPath) (hP : P.IsSimpleClosed) : + IsLocallyConstant (fun q : (P.carrier)ᶜ => crossingParity P q) + +/-- Polygonal Jordan separation. -/ +theorem polygonal_jordan (P : PolygonalPath) (hP : P.IsSimpleClosed) : + Nat.card (ConnectedComponents ((P.carrier)ᶜ : Set ℂ)) = 2 + +/-- The identity everything runs on. -/ +theorem polygonal_crosscut_parity (P : PolygonalPath) (hP : P.IsSimpleClosed) + (Q : PolygonalCrosscut P) : + crossingParity P = crossingParity (P.splitLeft Q) + crossingParity (P.splitRight Q) + +/-- Two ears. -/ +theorem exists_ear (P : PolygonalPath) (hP : P.IsSimpleClosed) (h : 3 < P.vertices.length) : + ∃ i, IsEar P i + +/-- Polygonal Schoenflies. The closed inside of a simple polygon is PL-homeomorphic to a triangle, and the homeomorphism extends to the plane. -/ +theorem polygonal_schoenflies (P : PolygonalPath) (hP : P.IsSimpleClosed) : + ∃ h : ℂ ≃ₜ ℂ, IsPLHomeomorph h ∧ h '' P.carrier = standardTriangle.boundary + +/-- The lever for layer 2. -/ +theorem not_planar_K33 : ¬ Nonempty (PlanarEmbedding (completeBipartiteGraph 3 3)) +``` + +**Mathematical route and formalization notes.** + +- Crossing parity, not the winding number, is the primitive. It is `ZMod 2`-valued, it is decidable, and the crosscut identity is additive in it. The integer winding number and the comparison with `TauCeti/Analysis/Contour/Winding/` are corollaries. +- ⚠ Do not restrict to lattice polygons. You cannot inscribe a lattice polygon in an arbitrary Jordan curve, so the lattice version cannot serve layer 2. Re-derive at general-vertex generality. (contrast with `rkirov/jordan_pick`) +- Nonplanarity of `K₃,₃` is a **finite** statement provable from the polygonal crosscut theorem alone. This let's us bootstrap from polygons to arbitrary curves, and it is also consumed by `SurfaceTopology` layer 10. +- Ear-clipping is the engine of polygonal Schoenflies: triangulate a simple polygon by diagonals, then induct. + +**Examples and mathematical checks.** The crossing parity is computed in an exact worked example for a non-convex polygon and a point in a re-entrant pocket. A figure-eight polygonal loop shows that simplicity is essential in polygonal Jordan separation. The strict size hypothesis in the ear theorem is tested on a triangle, and a polygon with exactly two ears provides a sharp positive example. + +**Natural intermediate results.** (i) polygonal paths, carriers, and simplicity; (ii) strips and the two-sidedness lemma; (iii) crossing parity, local constancy, and the integer winding number; (iv) polygonal Jordan separation; (v) the polygonal crosscut theorem; (vi) two ears and polygon triangulation; (vii) polygonal Schoenflies; (viii) nonplanarity of `K₃,₃`. + +**Consequences.** Both tracks depend on this. Unit (viii) also unlocks `SurfaceTopology` layer 10. + +--- + +## Layer 2: Separation, crosscuts, and invariance of domain + +The milestone of this layer is the crosscut theorem. + +⚠ Component count is a corollary of separation, but not the primary objective. The statement `Nat.card (ConnectedComponents Jᶜ) = 2` is not sufficient for `ConformalMapping`'s length-area argument or roadmap's layer 7. + +**From Tau Ceti.** `IsJordanCurve` and the arc theory in `TauCeti/Topology/JordanCurve/`; `filledHull`; `IsJordanDomain`; `TauCeti/Topology/{Continuum,LocallyConnected}.lean`. + +**Representative formal statements.** + +```lean +namespace IsJordanCurve +variable {J : Set ℂ} (hJ : IsJordanCurve J) + +def inside : Set ℂ := filledHull J \ J +def outside : Set ℂ := (filledHull J)ᶜ + +theorem isConnected_inside : IsConnected hJ.inside +theorem isConnected_outside : IsConnected hJ.outside +theorem isBounded_inside : Bornology.IsBounded hJ.inside +theorem not_isBounded_outside : ¬ Bornology.IsBounded hJ.outside +theorem frontier_inside : frontier hJ.inside = J +theorem frontier_outside : frontier hJ.outside = J + +/-- The statement named in the roadmap role of `TauCeti/Topology/FilledHull.lean` and in `ConformalMapping/STATUS.md`. -/ +theorem subset_closure_inside : J ⊆ closure (filledHull J \ J) + +theorem dense_accessible : Dense {p ∈ J | hJ.Accessible p} + +/-- The workhorse. -/ +theorem crosscut (P : Set ℂ) (hP : hJ.IsCrosscut P) : + ∃ J₁ J₂, IsJordanCurve J₁ ∧ IsJordanCurve J₂ ∧ + J₁ ∩ J₂ = P ∧ J₁ ∪ J₂ = J ∪ P ∧ + hJ.inside \ P = insideOf J₁ ∪ insideOf J₂ ∧ Disjoint (insideOf J₁) (insideOf J₂) + +/-- The corollary, including the shape used by lean-eval. -/ +theorem card_connectedComponents : Nat.card (ConnectedComponents ((J : Set ℂ)ᶜ)) = 2 +end IsJordanCurve + +/-- An arc does not separate. -/ +theorem arc_not_separates (A : Set ℂ) (hA : IsArc A) : IsConnected (Aᶜ) + +/-- Not currently in Mathlib -/ +theorem invarianceOfDomain₂ {U : Set ℂ} (hU : IsOpen U) (f : C(U, ℂ)) (hf : Injective f) : + IsOpen (Set.range f) ∧ IsOpenMap f +``` + +**Mathematical route and formalization notes.** + +- The order of development follows Thomassen. Approximate the paths that would have to cross the curve, not the curve itself, because Osgood gives an obstruction to curve approximation. A curve can have positive measure (layer 0) whereas the crossing paths are compact arcs in an open set and are cheap to control. A hypothetical failure separation, or a third complementary component, would result in a plane drawing of `K₃,₃`. +- Arc non-separation is proved by the chain-of-small-squares argument using the small-arc diameter bounds in `TauCeti/Topology/JordanCurve/SmallArc.lean`. +- ⚠ `invarianceOfDomain₂` is key. Without it `∂M` is not known to be chart-independent for a topological surface. Mathlib has neither invariance of domain nor degree theory for $C^0$ manifolds. +- Proving Jorden from Brouwer (as in `rkirov/jordan_pick`) is an independent second derivation of the component count. It is not the primary route. Proving Brouwer is independently worthwhile. + +**Examples and mathematical checks.** `subset_closure_inside` is stated in the same form as `TauCeti/Topology/FilledHull.lean`. An `IsJordanDomain` is constructed from an arbitrary `IsJordanCurve`. Currently this is impossible: the only constructors are from a ball, from a convex set, and by transport along a map. The component count is derived by both the Thomassen and Maehara routes without using one proof inside the other. `crosscut` is checked on a worked example where the two pieces are visibly different (an off-centre chord of a disc). + +**Natural intermediate results.** (i) `inside`, `outside`, boundedness, and connectedness; (ii) the common frontier; (iii) arc non-separation; (iv) accessibility and its density; (v) the crosscut theorem; (vi) the component count and the Maehara cross-check; (vii) `invarianceOfDomain₂` and chart-independence of `∂M`. + +**Consequences.** `ConformalMapping` layer 5. Layer 7. `∂M` for the rest of this roadmap. + +--- + +## Layer 3: The simplicial and piecewise-linear toolkit in dimension two + +This layer developes everything the approximation theorem needs, built on Tau Ceti's existing API. + +**From Tau Ceti.** `AbstractSimplicialComplex`, `Realization`, `link`, `closedStar`, `deletion`, barycentric subdivision, `SimplicialMap`, `dimension`, the collapse API, `IsTriangulable`. + +**Representative formal statements.** + +```lean +/-- General subdivision, heterogeneous in the vertex types. The eventual API may bundle the subdividing complex instead of exposing these parameters. -/ +def Subdivides {ι' ι : Type*} + (K' : AbstractSimplicialComplex ι') (K : AbstractSimplicialComplex ι) : Prop + +theorem Subdivides.realization_homeomorph (h : Subdivides K' K) : + Realization K' ≃ₜ Realization K + +def stellarSubdivision (K : AbstractSimplicialComplex ι) (σ : K.Face) : + AbstractSimplicialComplex (Option ι) + +def IsPLMap {K : AbstractSimplicialComplex ι} {L : AbstractSimplicialComplex κ} + (f : Realization K → Realization L) : Prop := + ∃ (ι' κ' : Type) (K' : AbstractSimplicialComplex ι') + (L' : AbstractSimplicialComplex κ'), + Subdivides K' K ∧ Subdivides L' L ∧ + ∃ g : SimplicialMap K' L', SimplicialRealizes g f + +theorem IsPLMap.comp : IsPLMap f → IsPLMap g → IsPLMap (g ∘ f) + +/-- A PL homeomorphism becomes simplicial after subdividing source and target. -/ +theorem exists_isomorphic_subdivisions + (h : Realization K ≃ₜ Realization L) (hPL : IsPLMap h) : + ∃ (ι' κ' : Type) (K' : AbstractSimplicialComplex ι') + (L' : AbstractSimplicialComplex κ'), + Subdivides K' K ∧ Subdivides L' L ∧ Nonempty (K' ≃ₛ L') + +/-- Concrete, not an instance of a dimension-general recursion. -/ +def IsCombinatorialSurface (K : AbstractSimplicialComplex ι) : Prop := + K.dimension = 2 ∧ K.IsPure ∧ + (∀ e ∈ K.faces, e.card = 2 → 1 ≤ (K.trianglesContaining e).card ∧ + (K.trianglesContaining e).card ≤ 2) ∧ + (∀ v ∈ K.vertices, IsCombinatorialCircle (K.link v) ∨ IsCombinatorialArc (K.link v)) + +def IsClosedCombinatorialSurface (K : AbstractSimplicialComplex ι) : Prop := + IsCombinatorialSurface K ∧ ∀ v ∈ K.vertices, IsCombinatorialCircle (K.link v) + +theorem IsCombinatorialSurface.realization_isSurface (h : IsCombinatorialSurface K) : + IsTopologicalSurfaceWithBoundary (Realization K) + +/-- Compatibility, for when `GeometricTopology` builds the general recursion. -/ +theorem isCombinatorialSurface_iff_isCombinatorialManifold_two : + IsCombinatorialSurface K ↔ IsCombinatorialManifold 2 K +``` + +**Mathematical route and formalization notes.** + +- A subdivision may introduce vertices, so its vertex type cannot be fixed in advance. The shared API must therefore be heterogeneous or bundle the subdividing complex. A similar issue affects combinatorial surface move relations, and is solved by bundling index types. +- The common-subdivision theorem in this layer starts with a **PL** homeomorphism (or, equivalently, two PL triangulations of one polyhedron). Its conclusion is best stated as subdivisions of the two complexes together with a simplicial isomorphism. The two-dimensional Hauptvermutung in layer 5 is the deeper theorem that starts with an arbitrary topological homeomorphism and produces such a PL comparison. Keeping these two statements separate exposes a genuine mathematical distinction which could be hidden by a convenient choice of vertex types. +- The compatibility theorem is deferred until the general dimension manifold predicate exists. None of the dimension-two results should depend on that comparison. +- Combinatorial circles and arcs in dimension one are concrete: a combinatorial circle is a connected 1-complex in which every vertex has exactly two neighbours; a combinatorial arc is one in which exactly two vertices have one neighbour and the rest have two. These should not be based on a general sphere-recognition recursion. + +**Examples and mathematical checks.** `IsCombinatorialSurface` is **false** for each of: two triangles sharing exactly one vertex; three triangles sharing an edge; the dunce hat; the cone on a theta graph. It is **true** for: the boundary of the tetrahedron; a triangulated disc; a triangulated Möbius band. Every one of these is a concrete finite complex checked by `decide`. ⚠ This is the layer where vacuity is a risk, because pinch points are possible for abstract complexes. + +**Natural intermediate results.** (i) general subdivision and realization invariance in the shared simplicial-complex library; (ii) stellar subdivision; (iii) purity, facets, and skeleta; (iv) isomorphic subdivisions for PL-homeomorphic complexes; (v) `IsPLMap` and its closure properties; (vi) combinatorial circles and arcs; (vii) `IsCombinatorialSurface` and the counter-witness battery; (viii) the realization theorem. + +**Consequences.** Layers 4, 5, 6. `SurfaceTopology` layer 3. + +--- + +## Layer 4: The piecewise-linear approximation theorem + +Moise's PL approximation theorem is the central theorem of the piecewise-linear. In its local form, a homeomorphism from an open polyhedron in a triangulated surface into the plane or another triangulated surface admits an arbitrarily close PL-homeomorphic approximation. The familiar compact statement for a homeomorphism between triangulated surfaces is a corollary. + +This is the main technical engine for both Radó's theorem and the Hauptvermutung. + +**From layers 1 and 3.** Polygonal Schoenflies, general position for polygonal arcs, subdivision, `IsPLMap`. + +**Representative formal statements.** + +```lean +/-- Moise's local form. Here `U` and `V` are open polyhedra and `φ` is strongly positive; the exact subtype packaging is schematic. -/ +theorem exists_pl_approximation_open + (f : U ≃ₜ V) (φ : U → ℝ) (hφ : StronglyPositive φ) : + ∃ g : U ≃ₜ V, IsPLMap g ∧ ∀ x, dist (f x) (g x) < φ x + +/-- Compact global form. -/ +theorem exists_pl_approximation {K : AbstractSimplicialComplex ι} + {L : AbstractSimplicialComplex κ} + (hK : IsCombinatorialSurface K) (hL : IsCombinatorialSurface L) + (f : Realization K ≃ₜ Realization L) (ε : ℝ) (hε : 0 < ε) : + ∃ g : Realization K ≃ₜ Realization L, IsPLMap g ∧ ∀ x, dist (f x) (g x) < ε + +/-- Relative form, agreeing with `f` on a subcomplex. -/ +theorem exists_pl_approximation_rel {A : Set (Realization K)} + (hA : IsSubcomplexCarrier A) (hf : IsPLMap (f.restrict A)) (ε : ℝ) (hε : 0 < ε) : + ∃ g, IsPLMap g ∧ g.restrict A = f.restrict A ∧ ∀ x, dist (f x) (g x) < ε +``` + +**Mathematical route and formalization notes.** + +- The proof first approximates the image of the 1-skeleton by a polygonal embedding and then extends across each 2-simplex by polygonal Schoenflies. The control function is strongly positive rather than globally constant so that the theorem applies on noncompact open subsets, as required in Radó's inductive construction. +- The relative form is needed for surfaces with boundary and for the isotopy statement in layer 8. +- The argument uses polygonal Schoenflies, but it does not need the topological Schoenflies theorem or the tameness results of layer 7. + +**Examples and mathematical checks.** The approximation is exhibited on a worked example where the original homeomorphism is not piecewise linear (a radial map with a non-linear radial profile). The epsilon is checked to be achievable for arbitrarily small values, that is, the statement is not accidentally vacuous by allowing `g = f`. + +**Natural intermediate results.** (i) the local open-set approximation theorem; (ii) general position and polygonal approximation of the 1-skeleton; (iii) the mesh-refinement construction; (iv) correction on the 1-skeleton; (v) filling triangles by polygonal Schoenflies; (vi) the compact and relative forms. + +--- + +## Layer 5: Radó's theorem and the two-dimensional Hauptvermutung + +This layer shows combinatorial invariants are topological. + +⚠ **Neither of these depends on the Schoenflies theorem.** Moise makes this point immediately after his triangulation theorem. The usual derivation from Schoenflies "is in a way misleading", since in dimension three Schoenflies fails and triangulation still holds. + +**Representative formal statements.** + +```lean +/-- Rado. -/ +theorem compact_surface_isTriangulable (M : Type*) [TopologicalSpace M] [CompactSpace M] + [T2Space M] [ChartedSpace (EuclideanSpace ℝ (Fin 2)) M] : IsTriangulable M + +theorem compact_surfaceWithBoundary_isTriangulable (M : Type*) [TopologicalSpace M] + [CompactSpace M] [T2Space M] [ChartedSpace (EuclideanHalfSpace 2) M] : + ∃ K, IsCombinatorialSurface K ∧ Nonempty (Realization K ≃ₜ M) + +/-- The two-dimensional Hauptvermutung. -/ +theorem hauptvermutung₂ {K : AbstractSimplicialComplex ι} + {L : AbstractSimplicialComplex κ} + (hK : IsCombinatorialSurface K) (hL : IsCombinatorialSurface L) + (h : Realization K ≃ₜ Realization L) : + ∃ (ι' κ' : Type) (K' : AbstractSimplicialComplex ι') + (L' : AbstractSimplicialComplex κ'), + Subdivides K' K ∧ Subdivides L' L ∧ Nonempty (K' ≃ₛ L') + +/-- The consequence that makes it useful. -/ +theorem hauptvermutung₂_isPL {K L} (hK : IsCombinatorialSurface K) + (hL : IsCombinatorialSurface L) (h : Realization K ≃ₜ Realization L) : + ∃ g : Realization K ≃ₜ Realization L, IsPLMap g ∧ IsPLMap g.symm +``` + +**Mathematical route and formalization notes.** + +- Radó's construction grows an already triangulated region across a countable chart cover. On each overlap, the **local** form of the approximation theorem replaces a topological coordinate change by a controlled PL homeomorphism; this is the point at which the approximation theorem enters the triangulation proof. +- The collar theorem is the lever for the boundary case: push `∂M` inward along a collar, triangulate the interior, and extend combinatorially. If `TauCeti/Geometry/Manifold/Boundary/Collar/` is usable at the topological level; if not, the topological two-dimensional collar is a target here and a contribution back to `GeometricTopology` layer 1. +- Locally finite triangulations of second-countable noncompact surfaces are built only insofar as the compact proof needs them, and the general noncompact Radó is out of scope. + +**Examples and mathematical checks.** A triangulation is produced for a surface presented only by charts, with no combinatorial data supplied. For the Hauptvermutung, the tetrahedral and octahedral triangulations of the sphere are refined to isomorphic subdivisions; the example is stated in the same two-subdivision form as the theorem. + +**Natural intermediate results.** (i) finite chart covers and shrinking; (ii) polygonal replacement of chart boundaries; (iii) assembly and Radó, closed case; (iv) the topological collar in dimension two; (v) Radó with boundary; (vi) the Hauptvermutung. + +**Consequences.** `GeometricTopology` layer 11. + +--- + +## Layer 6: The Euler characteristic + +Definition of the invariant that much of `SurfaceTopology` runs on. Euler characteristic here is only defined on simplicial complexes. + +**Representative formal statements.** + +```lean +def AbstractSimplicialComplex.eulerChar (K : AbstractSimplicialComplex ι) [Finite K.faces] : ℤ := + ∑ i, (-1 : ℤ) ^ i * (K.facesOfDim i).card + +theorem eulerChar_subdivision (h : Subdivides K' K) : K'.eulerChar = K.eulerChar +theorem eulerChar_simplicialIso (h : K ≃ₛ L) : K.eulerChar = L.eulerChar + +/-- Well defined by Rado, invariant by the Hauptvermutung. -/ +noncomputable def Surface.eulerChar (M : Type*) [CompactSurface M] : ℤ + +theorem Surface.eulerChar_congr {M N} [CompactSurface M] [CompactSurface N] (h : M ≃ₜ N) : + Surface.eulerChar M = Surface.eulerChar N + +theorem eulerChar_sphere : Surface.eulerChar (Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1) = 2 +theorem eulerChar_disc : Surface.eulerChar (Metric.closedBall (0 : ℂ) 1) = 1 +``` + +**Mathematical route and formalization notes.** + +- ⚠ Classification of surfaces is downstream of this, so we do not prove topological invariance of the cell count by appealing to that. Invariance comes from subdivision invariance and the Hauptvermutung. +- Define `eulerChar` on complexes first, then transport. The surface-level definition is `Classical.choice` over triangulations plus the invariance theorem. +- **General principle of both roadmaps.** Every invariant is defined on a finite presentation, proved invariant under the elementary moves, and upgraded to a homeomorphism invariant by the Hauptvermutung. There is no comparison theorem with Mathlib's singular homology or fundamental group here or in `SurfaceTopology`. Mathlib's singular homology has no excision and no Mayer–Vietoris. + +**Examples and mathematical checks.** On concrete finite complexes, `eulerChar` reduces to an explicit alternating sum. It computes 2 for the tetrahedron boundary, 2 for the octahedron boundary, 1 for a triangulated disc, 0 for a triangulated annulus, 0 for a triangulated Möbius band. `eulerChar_subdivision` is checked against a barycentric subdivision of the tetrahedron boundary, where the face counts change and the alternating sum does not. + +**Natural intermediate results.** (i) `eulerChar` on finite complexes and its effective computation; (ii) subdivision invariance; (iii) isomorphism invariance; (iv) the surface-level definition and transport; (v) the worked example table. + +--- + +## Layer 7: The Schoenflies theorem and tameness + +Schoenflies is one of the pinnicles of this roadmap. It's why `GeometricTopology` layer 2's local flatness hypothesis is always true in dimension two. + +**Representative formal statements.** + +```lean +theorem schoenflies {J : Set ℂ} (hJ : IsJordanCurve J) : + ∃ h : ℂ ≃ₜ ℂ, h '' J = Metric.sphere 0 1 + +theorem schoenflies_closure {J : Set ℂ} (hJ : IsJordanCurve J) : + Nonempty (closure hJ.inside ≃ₜ Metric.closedBall (0 : ℂ) 1) + +theorem schoenflies_sphere {S : Type*} [Sphere2 S] {J : Set S} (hJ : IsJordanCurve J) : + ∃ h : S ≃ₜ S, h '' J = equator + +/-- Tameness. The discharge of `GeometricTopology` layer 2's hypothesis. -/ +theorem isLocallyFlat_of_isArc_surface {M} [Surface M] {A : Set M} (hA : IsArc A) : + IsLocallyFlat A +theorem isLocallyFlat_of_isJordanCurve_surface {M} [Surface M] {J : Set M} + (hJ : IsJordanCurve J) : IsLocallyFlat J + +/-- A two-sided simple closed curve has an annular collar. The homeomorphism carries the zero section to `J`; the exact subtype packaging is schematic. -/ +theorem exists_collar_of_twoSided_isJordanCurve {M} [Surface M] {J : Set M} + (hJ : IsJordanCurve J) (h₂ : IsTwoSided J) : + ∃ (U : Set M), IsOpen U ∧ J ⊆ U ∧ + ∃ e : J × Ioo (-1 : ℝ) 1 ≃ₜ U, + ∀ p : J, (e (p, ⟨0, by norm_num⟩) : M) = p + +/-- A tame simple closed curve has an annular or Möbius-band regular neighbourhood, according as it is two-sided or one-sided. -/ +theorem jordanCurve_neighborhood_dichotomy {M} [Surface M] {J : Set M} + (hJ : IsJordanCurve J) : + (IsTwoSided J ∧ HasAnnularNeighborhood J) ∨ + (¬ IsTwoSided J ∧ HasMobiusNeighborhood J) +``` + +**Mathematical route and formalization notes.** + +- No homeomorphism is built directly. Instead this approach builds two matched finite cell decompositions, one of the closed interior and one of the closed square, isomorphic as cellulations and agreeing with a chosen boundary correspondencs. It refines them alternately so that cells become small on both sides and constructs the homeomorphism off the nested closed stars. Every finite stage is a plane graph governed by layer 2's crosscut theorem. No polygonal approximation of the curve appears anywhere. +- The matched cellulations here are finite approximating devices internal to this proof. They need not be identified with the realized `Cellulation2` objects of `SurfaceTopology`: the two constructions have different mathematical purposes. +- An alternative derivation gives an independent cross-check: once `ConformalMapping` Carathéodory's theorem gives `closure hJ.inside ≃ₜ closed disc` from `riemannMapping`, and gluing the inside and outside discs along `J` gives `schoenflies` again. + +**Examples and mathematical checks.** `schoenflies_closure` is instantiated on a curve that is not rectifiable. `isLocallyFlat_of_isArc_surface` is checked against `GeometricTopology`'s actual `IsLocallyFlat` predicate, not a local restatement. The core circle of a Möbius band is the essential counterexample to an unconditional product collar: it is tame and locally flat but one-sided. A note also records that automatic tameness fails in dimension three, where wild embeddings occur. + +**Natural intermediate results.** (i) `IsCrosscut` and finite cellulations of a Jordan domain; (ii) matching and refinement transfer; (iii) alternation and the small-cell estimate; (iv) the nested-star limit and `schoenflies_closure`; (v) the ambient and spherical forms; (vi) tameness of arcs; (vii) tameness of simple closed curves; (viii) the annulus/Möbius regular-neighbourhood dichotomy and the two-sided collar corollary. + +**Consequences.** `GeometricTopology` layer 2. + +--- + +## Layer 8: Uniqueness of the piecewise-linear and smooth structures + + +**Representative formal statements.** + +```lean +/-- Any two PL structures on a compact surface are PL-isomorphic. + The precise structure and isomorphism types come from `GeometricTopology`. -/ +theorem plStructure_unique_up_to_isomorphism {M} [CompactSurface M] + (s₁ s₂ : PLStructure M) : Nonempty (PLStructureIso s₁ s₂) + +/-- Every homeomorphism of compact surfaces is isotopic to a PL homeomorphism. -/ +theorem exists_isotopic_plHomeomorph {M N} [CompactSurface M] [CompactSurface N] + (f : M ≃ₜ N) : ∃ g : M ≃ₜ N, IsPLMap g ∧ Isotopic f g + +/-- Topological and PL homeomorphism classes agree. -/ +theorem homeomorph_iff_plHomeomorph {K L} (hK : IsCombinatorialSurface K) + (hL : IsCombinatorialSurface L) : + Nonempty (Realization K ≃ₜ Realization L) ↔ + Nonempty (Realization K ≃ₚₗ Realization L) + +/-- Every PL surface carries a compatible smooth structure, unique up to diffeomorphism. -/ +theorem exists_unique_smoothing {K} (hK : IsCombinatorialSurface K) : ... +``` + +**Mathematical route and formalization notes.** + +- Smoothing in dimension two is Whitehead's theorem, and the proof strategy is corner-rounding on a triangulation. The uniqueness half needs the relative approximation theorem from layer 4. +- ⚠ The mapping class group comparison (topological, PL, and smooth mapping class groups agree) is owned by `SurfaceTopology` layer 9, because that is where the groups are defined. This layer supplies the isotopy statement. +- “Essentially unique” means uniqueness up to the relevant notion of isomorphism, not literal equality of structures. On the PL side, homeomorphic triangulated surfaces admit isomorphic subdivisions. On the smooth side, compatible smoothings are related by a diffeomorphism; relative and isotopy refinements should be stated separately where used. + +**Examples and mathematical checks.** The statement is checked to be non-vacuous by exhibiting two genuinely different triangulations of the same surface and producing the PL homeomorphism. A note records that uniqueness of smooth structure fails in dimension four, so the surface theorem is visibly dimension-specific. + +**Natural intermediate results.** (i) uniqueness of the PL structure; (ii) isotopy to a PL homeomorphism; (iii) the Top/PL classification agreement; (iv) corner rounding and existence of a smoothing; (v) uniqueness of the smoothing. + +--- + +## Alternative routes and why they are not primary + +These alternatives clarify the mathematical choices made in the dependency graph. + +**The homological route to the Jordan curve theorem** (Cannon chapter 7: singular homology +of sphere complements, then arc non-separation and Jordan). **Closed.** At the pinned +commit Mathlib's singular homology consists of `Basic`, `HomologyZero`, and +`HomotopyInvariance` only. There is no excision, no Mayer–Vietoris for singular homology, +and no homology of spheres. Taking this route would require building a substantial piece of +algebraic topology first, which is outside this roadmap and outside `GeometricTopology`. + +**The Kline sphere characterization route to Schoenflies** (Cannon chapter 8: Schoenflies as +a corollary of a topological recognition theorem for the 2-sphere). **Rejected on cost.** +It is the more illuminating route and it is substantially more expensive, requiring Peano +continua, upper semicontinuous decompositions, and Bing's proof. See the +roadmap-for-a-roadmap below. + +**Maehara's route to the Jordan curve theorem** (Jordan from the Brouwer fixed point +theorem). **Retained as a second proof, not as the primary route.** It is the shortest proof +of the component count that exists, and `rkirov/jordan_pick` closes it in roughly 2,600 +lines. It supplies no frontier statement, no accessibility, and no crosscut theorem, so it +discharges nothing downstream. + +**Deriving Schoenflies from Carathéodory.** **Recorded as a cross-check.** It creates a +roadmap-level cycle through `ConformalMapping` and would make a headline theorem hostage to +another roadmap's schedule. + +--- + +## Roadmap-for-a-roadmap: continuum theory and wild plane topology + +This section motivates a separate future roadmap. Its theorems lie outside the scope of the present one. + +The point-set topology of compact connected metric spaces is a subject in its own right, with named theorems and essentially no Lean prior art, and it is the natural home for the *wild* side of plane topology that `GeometricTopology` layer 2 quantifies over. A roadmap for it would build: continua and Peano continua; the boundary-bumping lemma; **Hahn–Mazurkiewicz** (a space is a continuous image of the interval exactly when it is a Peano continuum); characterizations of the arc and the simple closed curve; **Brouwer's characterization of the Cantor set**; upper semicontinuous decompositions and decomposition spaces; **R. L. Moore's decomposition theorem**; the **Kline sphere characterization** (conjectured by Kline, proved by Bing); and **tameness of Cantor sets in the plane**, against Antoine's necklace as the dimension-three counterexample. + +The principal reference is Cannon, *Topology as Fluid Geometry*, volume 2, chapters 5, 6, 8, 10, and 11. + +Moore's decomposition theorem is the two-dimensional ancestor of the cell-like approximation theorems, and it is what makes Douady's pinched-disc model of the Mandelbrot set a disc; locally connected models of the Mandelbrot set are standard objects in complex dynamics. Brouwer's characterization of the Cantor set is used throughout descriptive set theory and one-dimensional dynamics. + + +--- + +## Out of scope + +- Anything in dimension three or higher is owned by `GeometricTopology`. +- The general (chart-based) `PLGroupoid` is owned by `GeometricTopology` layer 1. This roadmap's PL language is subdivisions and simplicial maps. +- Combinatorial maps, hypermaps, generalized maps, cellulations, polygon words, the classification of surfaces, mapping class groups, graph embeddings. [SurfaceTopology](../SurfaceTopology/README.md) develops all of this. +- Riemann surfaces, conformal structure, uniformization, Carathéodory's theorem. `ConformalMapping` owns it. This roadmap supplies its missing input and consumes nothing analytic in return. +- Singular homology, Mayer–Vietoris, excision, van Kampen, cohomology, duality. +- Continuum theory beyond the local-connectedness lemmas actually consumed. See the roadmap-for-a-roadmap above. +- Noncompact surfaces beyond what the compact proofs require. The classification of noncompact surfaces (Kerékjártó) is a natural follow-on roadmap. +- Measure-theoretic properties of curves beyond the single Osgood example in layer 0. + +--- + +## Provenance and prior art + +| Development | Licence | Coordination | What it evidences | +|---|---|---|---| +| `mccorvie/classification-of-surfaces` | Apache-2.0 | authored by this roadmap's author | that the Moise route to Radó and the Hauptvermutung closes, at roughly 90k lines of PL infrastructure plus 70k for Schoenflies | +| `alonamaloh/schoenflies-lean`, blueprint `alonamaloh/jordan-schoenflies` | Apache-2.0 code, CC BY 4.0 blueprint | | that follows Thomassen to prove Schoenflies | +| `rkirov/jordan_pick` | Apache-2.0 | | Follows Maehara's route to the component count. Also proves Brouwer, lattice-polygon crossing parity and ear-clipping | + +**Lessons from prior art.** Previous experience from formalizing the classification of surfaces underscored the importance of treating positive and negative examples as part of every validity definition, and treating realization as a construction followed by a comparison theorem rather than as an unconstrained structure field. + +**Integration.** Where existing code is adapted it will be re-derived against Tau Ceti's +vocabulary: `TauCeti.IsJordanCurve` rather than a parametrized definition, `ℂ` rather than +`EuclideanSpace ℝ (Fin 2)` for planar statements, and +`TauCeti/AlgebraicTopology/SimplicialComplex/` rather than a private complex type. + + +--- + +## References + +- C. Thomassen, *The Jordan–Schönflies theorem and the classification of surfaces*, + Amer. Math. Monthly **99** (1992), 116–130. The route for layers 1, 2, and 7. +- `alonamaloh/jordan-schoenflies`, the blueprint. The only source cited here written at + formalization granularity, with a statement-level index and a suggested module order. + Treat it as the primary route document for layers 1, 2, and 7. +- E. Moise, *Geometric Topology in Dimensions 2 and 3*, chapters 1–9. The route for layers 3, + 4, 5, and 8. Note in particular his remark following the triangulation theorem that + deriving it from Schoenflies "is in a way misleading". +- C. Rourke and B. Sanderson, *Introduction to Piecewise-Linear Topology*, chapters 1–3. + The PL vocabulary, already followed by `TauCeti/AlgebraicTopology/SimplicialComplex/`. +- M. H. A. Newman, *Elements of the Topology of Plane Sets of Points*. Classical reference + for the plane material. +- J. R. Munkres, *Elementary Differential Topology*; J. H. C. Whitehead, *On C¹-complexes*. + The smoothing route for layer 8. +- J. Cannon, *Topology as Fluid Geometry*, volume 2. Exposition reference for the + point-set lemmas in layer 0, and the reference for the roadmap-for-a-roadmap above. Note + that it is an idiosyncratic tour rather than a reference text, and its selection principle + is explicitly aesthetic; it should not be used to scope a roadmap. \ No newline at end of file diff --git a/TauCetiRoadmap/PlanarTopology/Suggested.lean b/TauCetiRoadmap/PlanarTopology/Suggested.lean new file mode 100644 index 00000000..d31c332f --- /dev/null +++ b/TauCetiRoadmap/PlanarTopology/Suggested.lean @@ -0,0 +1,267 @@ +import Mathlib +import TauCeti.AlgebraicTopology.SimplicialComplex.Realization +import TauCeti.Geometry.Manifold.LocallyFlat.Basic +import TauCeti.Topology.FilledHull +import TauCeti.Topology.JordanCurve.Basic +import TauCeti.Topology.Triangulable + +/-! +# Planar topology and the PL structure of surfaces: target signatures + +**This file is not the roadmap and is not exhaustive.** The definitive document is +`README.md`. The statements here suggest Lean forms for particular milestones, so that +contributors and reviewers converge on names and signatures; discharging all of them +finishes neither a layer nor the roadmap. `sorry` is allowed in this human-owned roadmap +library: these are targets, not completed proofs. + +The roadmap has two interacting tracks. Layers 0--2 build the planar separation engine +(Jordan curves, crosscuts, accessibility, and two-dimensional invariance of domain). +Layers 3--6 build the simplicial/PL engine (subdivision, PL approximation, Rado, +the two-dimensional Hauptvermutung, and Euler characteristic). Layer 7 proves +Schoenflies and automatic tameness in dimension two; layer 8 identifies the topological, +PL, and smooth categories for compact surfaces. + +Only declarations whose input vocabulary is already meaningful at the current Tau Ceti +pin are compiled below. In particular, do **not** introduce a vacuous `Prop := sorry` for +`Subdivides`, `IsCombinatorialSurface`, relative PL approximation, or the surface classes. +Their intended shapes are recorded as comments and should become compiled targets once +the prerequisite vocabulary is pinned. This follows the roadmap convention that a +condition which cannot yet be stated is omitted rather than replaced by an empty predicate. +-/ + +noncomputable section + +namespace TauCetiRoadmap.PlanarTopology + +open Complex Set Topology + +/-! ## Layer 0: conventions and plane transport -/ + +/-- The fixed identification of the complex plane with Mathlib's two-dimensional +Euclidean model. It is an isometry, so metric statements transport without a separate +comparison theorem. -/ +noncomputable def planeEquiv : ℂ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 2) := + Complex.orthonormalBasisOneI.repr + +/-- Rotation through a right angle in the complex-plane model. -/ +def perp (u : ℂ) : ℂ := Complex.I * u + +/-- The oriented area form used by the polygonal engine. -/ +def det (u v : ℂ) : ℝ := ((starRingEnd ℂ) u * v).im + +/-- Alexander's trick, extension form. The eventual implementation should be +stated dimension-generally even though this roadmap only spends the planar case. -/ +noncomputable def coneExtend {n : ℕ} + (h : Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1 ≃ₜ + Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1) : + Metric.closedBall (0 : EuclideanSpace ℝ (Fin n)) 1 ≃ₜ + Metric.closedBall (0 : EuclideanSpace ℝ (Fin n)) 1 := + sorry + +/-- Alexander's trick preserves radius. -/ +example {n : ℕ} + (h : Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1 ≃ₜ + Metric.sphere (0 : EuclideanSpace ℝ (Fin n)) 1) + (z : Metric.closedBall (0 : EuclideanSpace ℝ (Fin n)) 1) : + ‖(coneExtend h z : EuclideanSpace ℝ (Fin n))‖ = ‖(z : EuclideanSpace ℝ (Fin n))‖ := by + sorry + +/-! +The shared isotopy library should acquire a genuine relative/supported isotopy API before +we compile the isotopy form of Alexander's trick. The intended milestone is: + + theorem isotopicRel_of_eqOn_sphere ... : IsotopicRel (Metric.sphere 0 1) f g + +Likewise, the space-filling, nonrectifiable, and Osgood-curve examples belong to the +roadmap, but their precise constructors are not interface-defining enough to pin here. +-/ + +/-! ## Layer 1: polygonal foundations -/ + +/-- A finite polygonal path. The geometric carrier and simplicity API are deliberately +not baked into the structure: those should be reusable predicates on this object. -/ +structure PolygonalPath where + vertices : List ℂ + ne_nil : vertices ≠ [] + +/-- The carrier of a polygonal path, obtained by joining consecutive vertices by line +segments (and, for a closed path, the final vertex to the first). -/ +noncomputable def PolygonalPath.carrier (P : PolygonalPath) : Set ℂ := + sorry + +/-- Crossing parity is the primitive invariant of the polygonal separation proof. -/ +noncomputable def crossingParity (P : PolygonalPath) (q : ℂ) : ZMod 2 := + sorry + +/-- Integer winding is derived from the same polygonal crossing machinery and compared +with Tau Ceti's analytic winding-number API. -/ +noncomputable def polygonalWinding (P : PolygonalPath) (q : ℂ) : ℤ := + sorry + +/-! +Once the exact finite simplicity/crosscut vocabulary is pinned, representative compiled +targets should be added for: + + -- Polygonal Jordan separation. + theorem complement_connectedComponents_card_eq_two + (P : PolygonalPath) (hP : P.IsSimpleClosed) : + Nat.card (ConnectedComponents ((P.carrier)ᶜ : Set ℂ)) = 2 + + -- The additive identity that drives both tracks. + theorem polygonal_crosscut_parity ... : + crossingParity P = crossingParity (P.splitLeft Q) + crossingParity (P.splitRight Q) + + theorem exists_ear ... : ∃ i, IsEar P i + + -- Polygonal Schoenflies. + theorem exists_plHomeomorph_map_carrier_to_triangleBoundary ... : ... + +The nonplanarity of `K₃,₃` should be stated here only after the common graph-embedding +vocabulary consumed by `SurfaceTopology` has landed; do not introduce a private +`PlanarEmbedding` type in this roadmap. +-/ + +/-! ## Layer 2: Jordan separation, crosscuts, and invariance of domain -/ + +/-- The precise frontier statement consumed by `ConformalMapping`: every point of a +Jordan curve is a limit of points on its bounded side. -/ +example {J : Set ℂ} (hJ : TauCeti.IsJordanCurve J) : + J ⊆ closure (TauCeti.filledHull J \ J) := by + sorry + +/-- Jordan separation, in the component-count form used by lean-eval and as a useful +corollary of the stronger crosscut/frontier package. -/ +example {J : Set ℂ} (hJ : TauCeti.IsJordanCurve J) : + Nat.card (ConnectedComponents ((J : Set ℂ)ᶜ : Set ℂ)) = 2 := by + sorry + +/-- The bounded side of a Jordan curve is connected. -/ +example {J : Set ℂ} (hJ : TauCeti.IsJordanCurve J) : + IsConnected (TauCeti.filledHull J \ J) := by + sorry + +/-- Two-dimensional invariance of domain. This is the input that makes manifold boundary +chart-independent for topological surfaces. -/ +example {U : Set ℂ} (hU : IsOpen U) (f : C(U, ℂ)) (hf : Function.Injective f) : + IsOpen (Set.range f) ∧ IsOpenMap f := by + sorry + +/-! +The crosscut theorem and accessibility package should be compiled when `IsCrosscut` and +its endpoint/arc vocabulary are fixed. The roadmap's target is deliberately stronger than +component count: it must identify the two Jordan curves produced by a crosscut and the +two corresponding inside regions. +-/ + +/-! ## Layer 3: simplicial and PL toolkit -/ + +/-! +The following are architectural targets, but they should not be represented here by +placeholder propositions. Compile them when their actual data is pinned in Tau Ceti: + + def Subdivides {ι' ι : Type*} + (K' : AbstractSimplicialComplex ι') (K : AbstractSimplicialComplex ι) : Prop + + theorem Subdivides.realization_homeomorph (h : Subdivides K' K) : + AbstractSimplicialComplex.Realization K' ≃ₜ AbstractSimplicialComplex.Realization K + + def stellarSubdivision ... + + def IsPLMap ... : Prop + theorem IsPLMap.comp ... + + theorem exists_isomorphic_subdivisions + (h : Realization K ≃ₜ Realization L) (hPL : IsPLMap h) : ... + +`IsCombinatorialSurface` is a particularly important concrete definition: it should use +the dimension-two link condition (vertex links are combinatorial circles or arcs, and +edges lie in one or two triangles), not a dimension-general recognition recursion and not +`Prop := sorry`. Its realization theorem is the bridge consumed by `SurfaceTopology`. +-/ + +/-! ## Layer 4: PL approximation -/ + +/-! +Once `Subdivides`, `IsPLMap`, and `IsCombinatorialSurface` are compiled, pin the local +open-set Moise approximation theorem first, then the compact and relative forms. The +local strongly-positive-control-function statement is the one Radó actually consumes; +the compact epsilon statement is a corollary, not a substitute. +-/ + +/-! ## Layer 5: Radó and the two-dimensional Hauptvermutung -/ + +/-- **Radó's theorem**, closed-surface form: every compact topological surface is +triangulable. This uses Tau Ceti's existing weak `IsTriangulable` notion at the statement +boundary; the construction later supplies a combinatorial-surface witness. -/ +example (M : Type*) [TopologicalSpace M] [CompactSpace M] [T2Space M] + [ChartedSpace (EuclideanSpace ℝ (Fin 2)) M] : + TauCeti.IsTriangulable M := by + sorry + +/-! +The surface-with-boundary Radó theorem and the Hauptvermutung should become compiled +targets once `IsCombinatorialSurface` and heterogeneous `Subdivides` are present: + + theorem compact_surfaceWithBoundary_isTriangulable ... : + ∃ K, IsCombinatorialSurface K ∧ Nonempty (Realization K ≃ₜ M) + + -- The two-dimensional Hauptvermutung. + theorem exists_isomorphic_subdivisions_of_homeomorph_surface ... : ... + + theorem exists_plHomeomorph_of_homeomorph_surface ... : ... +-/ + +/-! ## Layer 6: Euler characteristic -/ + +/-! +Compile the finite-complex Euler characteristic only after the finite-face API and +heterogeneous subdivision relation are settled. The targets are: + + def AbstractSimplicialComplex.eulerChar ... : ℤ + theorem eulerChar_subdivision ... + theorem eulerChar_simplicialIso ... + noncomputable def Surface.eulerChar (M : Type*) [CompactSurface M] : ℤ + theorem Surface.eulerChar_congr ... + +The surface-level definition must be transported from a triangulation using Radó and the +Hauptvermutung, not obtained from classification or singular homology. +-/ + +/-! ## Layer 7: Schoenflies and tameness -/ + +/-- **Schoenflies theorem**, ambient planar form. -/ +example {J : Set ℂ} (hJ : TauCeti.IsJordanCurve J) : + ∃ h : ℂ ≃ₜ ℂ, h '' J = Metric.sphere 0 1 := by + sorry + +/-- Schoenflies for the closed inside: the bounded side together with the curve is a +closed disc. -/ +example {J : Set ℂ} (hJ : TauCeti.IsJordanCurve J) : + Nonempty (closure (TauCeti.filledHull J \ J) ≃ₜ Metric.closedBall (0 : ℂ) 1) := by + sorry + +/-! +Tameness should be stated against Tau Ceti's actual `IsLocallyFlat F F' f`, which is a +predicate on an embedding map with explicit model and complementary model. The schematic +set-valued declarations in the README are intentionally not copied here as if they +compiled. Once the chosen parametrizations of arcs and Jordan curves in a surface are +fixed, add representative targets saying those embeddings are locally flat, followed by +the annulus/Möbius regular-neighbourhood dichotomy. +-/ + +/-! ## Layer 8: uniqueness of PL and smooth structures -/ + +/-! +These targets wait on the shared `PLStructure`/PL-homeomorphism vocabulary owned by +`GeometricTopology` and on relative isotopy: + + theorem plStructure_unique_up_to_isomorphism ... + theorem exists_isotopic_plHomeomorph ... + theorem homeomorph_iff_plHomeomorph ... + theorem exists_unique_smoothing ... + +The isotopy-to-PL theorem is the important interface exported to `SurfaceTopology`'s +mapping-class-group layer. +-/ + +end TauCetiRoadmap.PlanarTopology diff --git a/TauCetiRoadmap/SurfaceTopology/README.md b/TauCetiRoadmap/SurfaceTopology/README.md new file mode 100644 index 00000000..5eedfbd0 --- /dev/null +++ b/TauCetiRoadmap/SurfaceTopology/README.md @@ -0,0 +1,850 @@ +# Roadmap: Surface topology, finite presentations, and classification + +A compact surface admits several finite combinatorial descriptions. A triangulation presents it as finitely many triangles with edge identifications. A generalized map records the same incidence data by three involutions on a finite set of darts. This roadmap proves that the finite and topological descriptions determine one another, develops the finite invariants and moves, and derives the classification of compact surfaces. + +The summits reached by this roadmap are: + +1. **The realization theorem**: an admissible finite generalized map can be realized as a compact surface, and every compact surface has a presentation as a generalized map. +2. **The Heffter–Edmonds–Ringel theorem**: cellular embeddings of a graph correspond to rotation systems in the orientable case, and to signed embedding schemes in general. +3. **The normal-form theorem**: every closed polygonal schema is related by elementary moves to a standard orientable or nonorientable word. Surfaces with boundary are reduced to the closed case by capping. +4. **The classification of compact surfaces**: every compact connected surface, with or without boundary, is homeomorphic to exactly one standard model, determined by Euler characteristic, orientability, and number of boundary components. + +Two later layers are further applications of the core thoery: + +5. **Curves, cutting, and mapping class groups**: Dehn twists, the change-of-coordinates principle, and the Dehn–Lickorish generation theorem. +6. **Planarity**: Kuratowski, Whitney, Mac Lane, Fáry, and the five-colour theorem, as a theorem suite built on the map and embedding theory. + +Layer 10 is best read as a mathematical validation and extension of the finite-map library. It's not part of the proof of surface classificatio, and its not a complete roadmap for graphs on surfaces. + +Each layer below is organized around its principal theorem, mathematical dependencies, and proof route. The Lean declarations are representative interfaces: they expose the intended connections to Tau Ceti without replacing the mathematicalstatements. + +> **Naming.** The directory name `CombinatorialMaps` describes the method; `SurfaceTopology` describes the subject. + +--- + +## Relationship to other roadmaps + +### This roadmap supplies + +| Consumer | What it needs | +|---|---| +| `GeometricTopology` layer 9 | the classification of closed orientable surfaces, for the splitting surface | +| `GeometricTopology` layer 9 | surface mapping classes | +| a future Four Colour roadmap | plane maps, duality, Euler's formula, the five-colour theorem | + +### This roadmap consumes + +From [PlanarTopology](../PlanarTopology/README.md), at the following points: + +| Item | Which layer here | +|---|---| +| `IsCombinatorialSurface` and its realization theorem | 3 | +| Radó: every compact surface is triangulable | 8 | +| the two-dimensional Hauptvermutung | 3, 7, 8 | +| `Surface.eulerChar`, well defined and invariant | 3, 5, 7, 8, 10 | +| the Schoenflies theorem and tameness of arcs and simple closed curves in a surface | 9 | +| Top = PL structure comparison and isotopy to a PL homeomorphism | 9 | + +From Tau Ceti and Mathlib: + +| Item | Location | +|---|---| +| `Equiv.Perm`, orbits, `MulAction`, cycle types | Mathlib | +| `AbstractSimplicialComplex`, `Realization`, `link`, subdivision, `SimplicialMap` | `TauCeti/AlgebraicTopology/SimplicialComplex/` | +| `IsTriangulable` | `TauCeti/Topology/Triangulable.lean` | +| structure theorem for finitely generated modules over a PID | `Mathlib.Algebra.Module.PID` | +| free groups, group presentations, `Subgroup.closure`, abelianization | Mathlib | +| `Isotopic`, `AmbientIsotopic` | `TauCeti/Topology/Homotopy/` | +| the multigraph `Graph α β` | Mathlib, **verify the current API before layer 5** | +| `Combinatorics/SimpleGraph/{Acyclic, BranchComponents, PathGraph}` | Tau Ceti | + +⚠ `TauCeti/LinearAlgebra/Matrix/SmithNormalForm.lean` covers only **square** integer matrices of positive determinant. Boundary matrices are rectangular. Use the PID structure theorem. + + +--- + +## Existing formal foundations and missing theorems + +Verified against Lean `v4.34.0-rc1` and Mathlib `master` at +`05ae0103f49b1ad1248f6039bbbad43d8aeb52a9`. + +**Absent from Tau Ceti** No `GMap`, no `Hypermap`, no `Cellulation`, no `rotationSystem`, no `eulerChar`, no `IsCombinatorialManifold`. `TauCeti/Combinatorics/` +contains Brauer diagrams, enumerative combinatorics, quivers, Young tableaux, and three thin `SimpleGraph` files. **The entire finite-map side of this roadmap is greenfield.** + +**Present and relevant.** `TauCeti/AlgebraicTopology/UniversalCover/` is substantial and includes fundamental groups of the circle, the torus, and the real projective plane, which are useful cross-checks for layer 7. `TauCeti/AlgebraicTopology/SimplicialComplex/` is the target of layer 3's comparison theorem. + + + +--- + +## Mathematical objects and formalization conventions + +### A mathematical hub and several presentations + +**The 2-dimensional generalized map is taken as the foundation.** A dart contains a complete flag, but also natively carries the side-incidence data that a face poset loses. Boundary-ness is recorded by fixed points of the highest order innovation. Non-orientability needs no signed variant. + +Oriented maps, hypermaps, cellulations, and polygonal schemas are **presentations**: each can be bidirectionally translated into the language of generalized maps, and each possesses its own natural operations. This roadmap does not propose a parallel realization theory. Realization, Euler characteristic, orientability, and the operations are defined once, on generalized maps. This is deliberate, and it follows the discipline `GeometricTopology` layer 4 states for knot presentations: pick a hub, do not aim for the complete graph on presentations. + +The six comparison theorems in layer 2 are not a claim that all presentations are co-equal. They state precisely which information each conversion preserves and certify that the chosen hub represents the same finite surface data. + +### Bundled index types and isomorphism closure + +Every finite object bundles its own index type: darts for maps, vertices for complexes, labels for schemas. Every move relation is **closed under isomorphism of that type** before `Relation.ReflTransGen` is applied. + +⚠ This is not cosmetic. The Pachner 1↔3 move adds a vertex and the schema cancellation move removes a letter, so both changes affect the index type. A relation on a fixed index type cannot express them, and `ReflTransGen` demands that intermediate index types line up on the nose. + +### Realization + +`GMap2.realization G` is defined **directly**, as the quotient of `D × Δ²` by the +side-gluings induced by the three involutions. It is always defined, with no hypotheses, and +this object carries the topology. + +⚠ **The flag complex of a generalized map is not in general an abstract simplicial complex.** +Take the projective plane as the word `aa`, with one vertex, one edge, and one face. As a +generalized map on darts `{1,2,3,4}` with + +``` +α₀ = (1 2)(3 4) α₁ = (1 4)(2 3) α₂ = (1 3)(2 4) +``` + +the involutions `α₀` and `α₂` commute, so this is a valid 2-generalized map; all three orbit +groups act transitively, so there is one cell of each dimension and `χ = 1 - 1 + 1 = 1`. The +flag vertex set has three elements and admits exactly one triangle. However the four darts collapse to one simplex. The one-vertex torus fails in a similar way: eight darts, four flag vertices, two distinct triples. + +The bridge to `AbstractSimplicialComplex` is therefore a **theorem about a subdivision**, not +a definition. After the canonical barycentric subdivision of the map, the flag map is +injective and the flag complex is honest. The `aa` map above is the certified counter-witness +recorded in layer 3's examples and mathematical checks. + +### Euler characteristic + +```lean +def GMap2.eulerChar (G : GMap 2 D) : ℤ := + (Nat.card (G.Cell 0) : ℤ) - Nat.card (G.Cell 1) + Nat.card (G.Cell 2) +``` + +with `Cell 0 = Orb⟨α₁,α₂⟩`, `Cell 1 = Orb⟨α₀,α₂⟩`, `Cell 2 = Orb⟨α₀,α₁⟩`. + +**The boundary is recorded entirely by fixed points of `α₂`**. Boundary vertices and edges are already counted by the ordinary orbit cells. A boundary edge has a two-element `⟨α₀,α₂⟩`-orbit and an interior edge a four-element one. This is the decidable boundary test. + +### Invariance + +**Invariance comes from the Hauptvermutung, not from comparison with singular theory.** Every invariant here is defined on a finite presentation and proved invariant under isomorphism, subdivision, and the elementary moves. `PlanarTopology`'s Radó and Hauptvermutung then make it a homeomorphism invariant. + +⚠ This roadmap does not contemplate a comparison theorem with Mathlib's `SingularHomology` or `FundamentalGroup`. None is needed. Moreover Mathlib's singular homology has no excision and no Mayer–Vietoris at the pinned commit, so none is currently provable. + +Consequently, ⚠ **the homology and fundamental group here are named for what they are.** Use `Cellulation2.homology` and `Cellulation2.edgePathGroup`, never bare `H₁` or `π₁`. A theorem reading `H₁_torus : H₁ T² ≅ ℤ × ℤ` would claim too much. When the comparison becomes available it will be a bridge theorem with two well-named sides. + +--- + +## Structure + +``` +L0 finite conventions + | +L1 generalized maps ------------------------------. + | | +L2 presentations and comparison theorems | + | | +L3 realization <---- PlanarTopology L3, L5, L6 | + | | +L4 operations on finite surfaces -----. | + | \ | +L5 embedded graphs and HER L6 schemas and normal forms + | | + | L7 combinatorial homology and edge-path group + | | + | L8 classification <---- PlanarTopology L2, L5, L6 + | | + | L9 mapping class groups (extension) + | | <---- PlanarTopology L7, L8 + '------------------------------- L10 planarity (extension and validation) +``` + +--- + +## Layer 0: Finite conventions + +This layer isolates the finite equivalence relations needed by cyclic words and by moves that change an object's indexing type. + +**Representative formal statements.** + +```lean +/-- Cyclic words. Kept deliberately separate from `CircularOrder` and from the + topological circle: a cyclic word is a finite sequence with repeated labels, + taken modulo rotation. -/ +def CyclicWord (α : Type*) : Type* := Quotient (rotationSetoid α) + +class HasIsoRel (X : Type*) where + IsoRel : X → X → Prop + isEquiv : Equivalence IsoRel + +structure BundledFinite where + ι : Type + fintype : Fintype ι + decEq : DecidableEq ι + +/-- The isomorphism closure of a relation on bundled objects. -/ +def isoClosure {X : Type*} [HasIsoRel X] (r : X → X → Prop) : X → X → Prop := + fun a b => ∃ a' b', IsoRel a a' ∧ IsoRel b b' ∧ r a' b' + +theorem isoClosure_reflTransGen_congr : ... +``` + +**Proof strategy and formalization notes.** `Function.Involutive` and `Commute` in `Equiv.Perm D` are the Mathlib idioms; do not hand-roll `∀ d, f (f d) = d` or `f ∘ g = g ∘ f`. + +**Examples and mathematical checks.** `CyclicWord` equality is `Decidable` and distinguishes `abab` from `aabb` while identifying `abab` with `baba`. + +**Natural intermediate results.** (i) cyclic words; (ii) bundling and isomorphism closure; (iii) `ReflTransGen` lemmas for isomorphism-closed relations. + +--- + +## Layer 1: Generalized maps + +The foundational object for all of the combinatorial topology which follows. + +**Representative formal statements.** + +```lean +structure GMap (n : ℕ) (D : Type*) [Fintype D] [DecidableEq D] where + adj : Fin (n + 1) → Equiv.Perm D + involutive : ∀ i, Function.Involutive (adj i) + commute_of_far : ∀ i j, i.1 + 2 ≤ j.1 → Commute (adj i) (adj j) + + +abbrev GMap2 (D : Type*) [Fintype D] [DecidableEq D] := GMap 2 D + +def GMap.Cell (G : GMap n D) (i : Fin (n + 1)) : Type* := + MulAction.orbitRel.Quotient (Subgroup.closure {G.adj j | j ≠ i}) D + +structure GMap2.Iso {D D' : Type*} [Fintype D] [Fintype D'] + (G : GMap2 D) (G' : GMap2 D') where + toEquiv : D ≃ D' + map_adj : ∀ i d, toEquiv (G.adj i d) = G'.adj i (toEquiv d) + + +def GMap2.eulerChar (G : GMap2 D) : ℤ := ... + +/-- Boundary. -/ +def GMap2.IsBoundaryDart (G : GMap2 D) (d : D) : Prop := G.adj 2 d = d +instance : DecidablePred G.IsBoundaryDart + +/-- Candidate combinatorial surface condition. `IsSurfaceNondegenerate` abbreviates the + exact finite local condition to be settled against Damiand--Lienhardt. It must still + admit standard one-cell presentations such as `aa`. -/ +def IsSurfaceGMap (G : GMap2 D) : Prop := + (∀ d, G.adj 0 d ≠ d) ∧ (∀ d, G.adj 1 d ≠ d) ∧ G.IsSurfaceNondegenerate +instance : DecidablePred (IsSurfaceGMap (D := D)) + +def IsClosedSurfaceGMap (G : GMap2 D) : Prop := + IsSurfaceGMap G ∧ ∀ d, G.adj 2 d ≠ d + +/-- Orientability as a property; fixed points representing boundary do not change side. -/ +def GMap2.IsOrientable (G : GMap2 D) : Prop := + ∃ S : Set D, ∀ i d, G.adj i d ≠ d → (d ∈ S ↔ G.adj i d ∉ S) +structure GMap2.Orientation (G : GMap2 D) where ... +instance : DecidablePred (GMap2.IsOrientable (D := D)) + +def GMap2.boundaryComponentCount (G : GMap2 D) : ℕ +def GMap2.orientableGenus (G : GMap2 D) + (h : G.IsConnected ∧ IsSurfaceGMap G ∧ G.IsOrientable) : ℕ +def GMap2.nonorientableGenus (G : GMap2 D) + (h : G.IsConnected ∧ IsSurfaceGMap G ∧ ¬ G.IsOrientable) : ℕ +``` + +**Proof strategy and formalization notes.** + +- ⚠ **The exact surface condition is the highest-risk definition of the roadmap.** A generalized map permits multi-incidence and folded configurations, so the bare involution axioms describe a wider class than regular cell decompositions. At the same time, valid surface presentations such as the one-face projective-plane word `aa` have repeated incidence and must not be excluded merely for failing regularity. In dimension two the incidence graph generated by two involutions has valence at most two, suggesting that the circle-or-arc link condition follows from a small local non-degeneracy condition. That implication should be proved, and the precise condition should be taken from Damiand–Lienhardt. +- The decisive characterization is the later equivalence between the finite local condition and the statement that every point of the realization has a disc or half-disc neighbourhood. Positive and negative finite examples belong to that theorem's specification. +- Orientability is a bipartition of the darts in which every **non-fixed** adjacency changes side. Fixed points of the final involution encode boundary and must not make orientability impossible. The existence of such a bipartition is a property; a chosen bipartition is additional data. +- The `commute_of_far` condition is stated only for `i + 2 ≤ j`; its symmetric form is an immediate lemma. The two genus numbers are first defined from the finite invariants; their identification with the genera of the standard surfaces is proved in layer 8. + +**Examples and mathematical checks.** The following table is checked by `decide`, with the maps written out explicitly. + +| Map | darts | V | E | F | χ | orientable | +|---|---|---|---|---|---|---| +| sphere, tetrahedral | 24 | 4 | 6 | 4 | 2 | yes | +| projective plane, `aa` | 4 | 1 | 1 | 1 | 1 | no | +| torus, `aba⁻¹b⁻¹` | 8 | 1 | 2 | 1 | 0 | yes | +| Klein bottle, `abab⁻¹` | 8 | 1 | 2 | 1 | 0 | no | +| disc, `n`-gon | 2n | n | n | 1 | 1 | yes | +| annulus | 8 | 2 | 3 | 1 | 0 | yes | +| Möbius band | 8 | 2 | 3 | 1 | 0 | no | + +Counter-witnesses: `IsSurfaceGMap` is **false** for the immediate folded-edge configuration singled out by `IsSurfaceNondegenerate`, and **false** for a map with a fixed point of `α₀` or of `α₁`. `IsOrientable` is **false** for the Klein bottle map and **true** for the torus map, decided by the same procedure. + +**Natural intermediate results.** (i) the structure and basic permutation lemmas; (ii) cells, orbits, and decidability; (iii) Euler characteristic and the example table; (iv) boundary darts and the boundary test; (v) `IsSurfaceGMap` and its counter-witnesses; (vi) orientability; (vii) boundary count and the two genus formulas for connected surface maps. + +--- + +## Layer 2: Presentations and comparison theorems + +Each presentation gets a constructor into generalized maps, accessors out, and its own natural operations. None gets a realization theory. + +**Representative formal statements.** + +```lean +/-- Oriented map: a rotation system. -/ +structure CombinatorialMap (D : Type*) [Fintype D] [DecidableEq D] where + σ : Equiv.Perm D -- rotation at vertices + α : Equiv.Perm D -- edge involution + α_involutive : Function.Involutive α + α_free : ∀ d, α d ≠ d +def CombinatorialMap.toGMap2 : GMap2 (D × Bool) + +/-- Hypermap. -/ +structure Hypermap (D : Type*) [Fintype D] [DecidableEq D] where + σ φ α : Equiv.Perm D + comp : σ * φ * α = 1 +def Hypermap.toGMap2 : GMap2 (D × Bool) + +/-- Cellulation: a presentation, not an independent structure with its own validity theory. -/ +structure Cellulation2 where ... +def Cellulation2.toGMap2 : GMap2 _ + +/-- Polygonal schema. A label occurring twice is glued; a label occurring once + represents a boundary edge. Further compatibility is part of `IsSurface`. -/ +structure PolygonalSchema where + label : Type + fintypeLabel : Fintype label + faces : List (CyclicWord (label × Bool)) + occurs_once_or_twice : ∀ l, (occurrences l).length = 1 ∨ (occurrences l).length = 2 +def PolygonalSchema.toGMap2 : GMap2 _ +``` + +**The six comparison theorems.** These identify the information preserved by the conversions; they do not make the presentations co-equal foundations. + +1. `K.toGMap2.flagComplex ≃ K.barycentricSubdivision` for a combinatorial surface `K`. ⚠ This is the master test. If it holds, the generalized map is not lying about the surface. It is stated here and proved in layer 3, where realization exists. +2. `|flagComplex G| ≃ₜ G.realization`. The two realizations agree. Proved in layer 3. +3. `G.toCellulation.toGMap2 ≃ G`, up to the canonical subdivision. Tests that the cellulation constructor loses no flag data. +4. `M.toGMap2.toCombinatorialMap ≃ M` after choosing the induced orientation. Tests the orientation encoding. +5. `G.dual.dual ≃ G`, with canonically homeomorphic realizations. +6. Converting a schema to a generalized map recovers both its glued edge-pairs and its singleton boundary edges, up to cyclic equivalence and relabelling. + +**Examples and mathematical checks.** ⚠ **Exhibit two non-isomorphic surface cellulations with the same incidence poset.** This answers the question "why is this not just a poset?" and justifies `Cellulation2` carrying side-incidence data. Source: figures in Damiand–Lienhardt. Each conversion is worked out on the layer 1 example table. Degenerate examples show why the hypotheses of the comparison theorems are necessary. + +**Natural intermediate results.** (i) oriented maps and the conversion; (ii) hypermaps and the conversion; (iii) cellulations and the conversion; (iv) polygonal schemas and the conversion; (v) comparison theorems 3, 4, and 6; (vi) the poset counter-example. + +--- + +## Layer 3: Realization + +Where the finite side meets [PlanarTopology](../PlanarTopology/README.md). + +**From PlanarTopology.** `IsCombinatorialSurface`, its realization theorem, the Hauptvermutung. + +**Representative formal statements.** + +```lean +/-- Direct. No hypotheses, no abstract simplicial complex. -/ +def GMap2.realization (G : GMap2 D) : Type* := + Quotient (gluingSetoid G) -- of `D × StandardSimplex (Fin 3)` + +instance : TopologicalSpace (GMap2.realization G) +instance : CompactSpace (GMap2.realization G) + +theorem IsSurfaceGMap.realization_isSurface (h : IsSurfaceGMap G) : + IsCompactSurfaceWithBoundary G.realization + +theorem IsSurfaceGMap.eulerChar_eq (h : IsSurfaceGMap G) : + Surface.eulerChar G.realization = G.eulerChar + +/-- The simplicial bridge: a theorem about a subdivision, not a definition. -/ +theorem GMap2.flagComplex_isSimplicial_of_subdivided (G : GMap2 D) : + Function.Injective (G.barycentricSubdivision.flagTriple) + +theorem GMap2.realization_homeomorph_flagComplex (h : IsSurfaceGMap G) : + G.realization ≃ₜ Realization (G.barycentricSubdivision.flagComplex) + +/-- Every compact surface arises. Uses Rado. -/ +theorem exists_gmap_of_compactSurface (M : Type*) [CompactSurface M] : + ∃ (D : Type) (_ : Fintype D) (G : GMap2 D), IsSurfaceGMap G ∧ + Nonempty (G.realization ≃ₜ M) + +/-- Comparison theorems 1 and 2 from layer 2. -/ +theorem flagComplex_toGMap2 (hK : IsCombinatorialSurface K) : + K.toGMap2.flagComplex ≅ K.barycentricSubdivision +``` + +**Proof strategy and formalization notes.** + +- ⚠ Do not define realization through `AbstractSimplicialComplex`. +- The subdivision needed for the bridge may be one barycentric step or two, depending on the map. + +**Examples and mathematical checks.** The `aa` generalized map from the encoding conventions is a certified counter-witness: it is a valid surface map, its flag triple map is **not** injective, and its unsubdivided flag complex has one triangle where the map has four darts. Realization is checked to produce the correct Euler characteristic on the full layer 1 table, through `PlanarTopology`'s `Surface.eulerChar`, not through `GMap2.eulerChar`. + +**Natural intermediate results.** (i) the gluing setoid and the quotient topology; (ii) compactness and the surface property; (iii) the flag triple, injectivity after subdivision, and the counter-witness; (iv) the homeomorphism with the flag complex realization; (v) `exists_gmap_of_compactSurface`; (vi) Euler characteristic agreement. + +**Consequences.** `GeometricTopology` layer 11's dimension-two case. + +--- + +## Layer 4: Topological operations on generalized maps + +This layer separates two kinds of operation. Subdivision, admissible contraction, and duality preserve the represented surface. Connected sum, cutting, the orientation cover, capping, and doubling change it in controlled ways. Each operation is accompanied by its precise theorem on realizations and invariants, not only by orbit-count identities. + +**Representative formal statements.** + +```lean +def GMap2.subdivideEdge (G : GMap2 D) (e : G.Cell 1) : GMap2 _ +def GMap2.subdivideFace (G : GMap2 D) (f : G.Cell 2) : GMap2 _ +def GMap2.contractEdge (G : GMap2 D) (e : G.Cell 1) (h : e.IsContractible) : GMap2 _ +def GMap2.dual (G : GMap2 D) (h : IsClosedSurfaceGMap G) : GMap2 D +def GMap2.connectedSum (G : GMap2 D) (H : GMap2 E) : GMap2 _ +def GMap2.cutAlong (G : GMap2 D) (c : G.CombinatorialCurve) : GMap2 _ +def GMap2.orientationDoubleCover (G : GMap2 D) : GMap2 (D × Bool) +def GMap2.cap (G : GMap2 D) : GMap2 _ -- glue a disc on each boundary circle +def GMap2.double (G : GMap2 D) : GMap2 (D × Bool) + +theorem GMap2.subdivideEdge_realization : (G.subdivideEdge e).realization ≃ₜ G.realization +theorem GMap2.dual_realization (h : IsClosedSurfaceGMap G) : + (G.dual h).realization ≃ₜ G.realization +theorem GMap2.dual_eulerChar (h : IsClosedSurfaceGMap G) : + (G.dual h).eulerChar = G.eulerChar + +theorem GMap2.orientationDoubleCover_isOrientable : + G.orientationDoubleCover.IsOrientable +theorem GMap2.orientationDoubleCover_eulerChar : + G.orientationDoubleCover.eulerChar = 2 * G.eulerChar +theorem GMap2.orientationDoubleCover_isConnected + (hG : G.IsConnected) (h : ¬ G.IsOrientable) : + IsConnected G.orientationDoubleCover +theorem GMap2.orientationDoubleCover_isCovering : + IsCoveringMap (G.orientationDoubleCover.projection) + +theorem GMap2.cap_eulerChar : + G.cap.eulerChar = G.eulerChar + G.boundaryComponentCount +theorem GMap2.cap_isOrientable : G.cap.IsOrientable ↔ G.IsOrientable +theorem GMap2.cap_isConnected (hG : G.IsConnected) : G.cap.IsConnected + +theorem GMap2.double_eulerChar : G.double.eulerChar = 2 * G.eulerChar +``` + +**Proof strategy and formalization notes.** + +- The **orientation double cover** a covering map for surfaces with boundary. The orientation character is trivial on each boundary component because a collar supplies a two-sided neighbourhood; consequently every boundary circle lifts to two boundary circles, each mapping homeomorphically to the original one. (This behaviour should be included in the covering theorem.) +- ⚠ The **double** `DM = M ∪_∂M M` a quotient by an involution with fixed points, `Fix σ = ∂M` and `DM/σ = M`. Record the double for its Euler characteristic identity and for later use. ⚠ Do not attempt to derive triangulation with boundary from it, that would require an equivariant triangulation theorem. +- An edge contraction preserves the surface only under the appropriate link or non-degeneracy condition. Its realization theorem should state the exact admissibility hypothesis (being a non-loop is not sufficient). +- Ordinary duality preserves the class of surface maps cleanly in the closed case. With boundary, reversing the involutions moves fixed points from `α₂` to `α₀`, so a relative or capped dual version is needed. +- **Capping** is the operation that simplifies the classification with boundary: every compact surface with boundary is a closed surface minus `b` open discs. That reduction is layer 8's main structural simplification. +- Do not build the Petrie dual or higher-dimensional operations. + +**Examples and mathematical checks.** `dual (dual G) ≃ G` is checked on the closed maps in the layer 1 table (comparison theorem 5). `orientationDoubleCover` of the projective plane is the sphere map, of the Klein bottle map is the torus map, and of an already orientable map is disconnected. `cap` of the disc map is the sphere map. `double` of the Möbius band map is the Klein bottle map. All by `decide` on the explicit maps. + +**Natural intermediate results.** (i) subdivision operations; (ii) contraction and deletion; (iii) duality; (iv) connected sum; (v) cutting along a combinatorial curve; (vi) orientation double cover; (vii) capping and doubling. + +--- + +## Layer 5: Embedded graphs and the Heffter–Edmonds–Ringel theorem + +This externally validates the finite model. It says the maps are not merely an adequate encoding of embedded graphs but the right one. + +**From Mathlib.** the multigraph `Graph α β`; ⚠ verify its API first. + +**Representative formal statements.** + +```lean +def GMap2.underlyingGraph (G : GMap2 D) : Graph (G.Cell 0) (G.Cell 1) + +structure GraphEmbedding (Γ : Graph α β) (M : Type*) [Surface M] where ... +def GraphEmbedding.IsCellular : Prop -- every face is an open disc + +def RotationSystem (Γ : Graph α β) : Type* := ... +def SignedRotationSystem (Γ : Graph α β) : Type* := ... + +theorem cellularEmbeddings_equiv_gmaps (Γ : Graph α β) (hΓ : Γ.Connected) : + CellularEmbeddings Γ / EquivalenceOfEmbeddings + ≃ {G : BundledGMap2 // G.underlyingGraph ≃ Γ} / GMap2.Iso + +/-- Heffter--Edmonds--Ringel, orientable form. -/ +theorem orientedCellularEmbeddings_equiv_rotationSystems + (Γ : Graph α β) (hΓ : Γ.Connected) : + OrientedCellularEmbeddings Γ / EquivalenceOfOrientedEmbeddings + ≃ RotationSystem Γ / EquivalenceOfRotations + +/-- General-surface form, using signed rotation systems (embedding schemes). -/ +theorem cellularEmbeddings_equiv_signedRotationSystems + (Γ : Graph α β) (hΓ : Γ.Connected) : + CellularEmbeddings Γ / EquivalenceOfEmbeddings + ≃ SignedRotationSystem Γ / EquivalenceOfSignedRotations + +/-- Euler's formula for a cellular embedding. -/ +theorem eulerFormula_cellular {Γ : Graph α β} (e : GraphEmbedding Γ M) (h : e.IsCellular) : + (Γ.vertexCount : ℤ) - Γ.edgeCount + e.faceCount = Surface.eulerChar M + +def Graph.genus (Γ : Graph α β) : ℕ -- needs layer 8 +def Graph.nonorientableGenus (Γ : Graph α β) : ℕ +``` + +**Proof strategy and formalization notes.** + +- ⚠ The correspondence is only for **cellular** embeddings. A graph embedded in a torus with a non-disc face is the counter-witness and is given in the examples and mathematical checks. +- The general case needs the signed or generalized-map version. The standard theorem for the orientable case is stated in terms of `CombinatorialMap` (rotation systems). Derive the latter from the former +- `Graph.genus` minimises over surfaces and therefore waits on layer 8; the HER correspondence and Euler formula do not. + +**Examples and mathematical checks.** `K₅` and `K₃,₃` have genus 1 and embed cellularly in the torus. +`IsCellular` is **false** for `K₄` drawn inside a disc in the torus. Euler's formula is +checked on the layer 1 table. + +**Natural intermediate results.** (i) the underlying multigraph; (ii) embeddings and cellularity; +(iii) rotation systems; (iv) the orientable HER correspondence; (v) the general HER +correspondence; (vi) Euler's formula; (vii) genus, after layer 8. + +--- + +## Layer 6: Polygonal schemas and normal forms + +The classification theorem is stated for closed schemas. The classification with boundary in layer 8 uses capping to reduce to this theorem. + +**Representative formal statements.** + +```lean +inductive ElementarySchemaMove : PolygonalSchema → PolygonalSchema → Prop + | cancel : ... -- `a a⁻¹` adjacent, removes a label + | relabel : ... + | cut : ... + | paste : ... + +def SchemaMove := isoClosure ElementarySchemaMove + +def normalFormOrientable (g : ℕ) : PolygonalSchema +def normalFormNonorientable (k : ℕ) (hk : 0 < k) : PolygonalSchema + +theorem closedSchema_reduces_to_normalForm + (S : PolygonalSchema) (hS : S.IsSurface) (hclosed : S.IsClosed) : + ∃ N, IsClosedNormalForm N ∧ Relation.ReflTransGen SchemaMove S N + +/-- Relative form used after capping: the distinguished cap faces remain identifiable + through the reduction and become standard disjoint discs in the normal form. -/ +theorem closedSchema_reduces_to_normalForm_rel_caps + (S : PolygonalSchema) (caps : Finset S.Face) + (hS : S.IsSurface) (hclosed : S.IsClosed) (hcaps : PairwiseDisjointCaps caps) : ... + +theorem SchemaMove.realization_homeomorph (h : SchemaMove S T) : + S.toGMap2.realization ≃ₜ T.toGMap2.realization +``` + +**Proof strategy and formalization notes.** + +- ⚠ Every move changes the label type. The isomorphism closure from layer 0 is what makes `ReflTransGen` usable. Do not fix an alphabet. +- The reduction is the classical closed-surface algorithm: merge to one polygon, cancel adjacent inverse pairs, make the schema have a single vertex class, group crosscaps, group handles, and convert a handle plus a crosscap into three crosscaps (Dyck's theorem). Each step needs its realization theore, from `SchemaMove.realization_homeomorph`, not a separate argument. + +**Examples and mathematical checks.** The reduction is run on `abab⁻¹` (the Klein bottle), `aabb` (the same surface, reaching the same normal form), and `abca⁻¹b⁻¹c⁻¹` (a nontrivial six-edge schema). A label occurring once is accepted as a boundary edge; a label occurring three times, or a pairing with an invalid local incidence, must fail `IsSurface`. + +**Natural intermediate results.** (i) schemas and the surface condition; (ii) the moves and isomorphism closure; (iii) realization invariance of each move; (iv) reduction to a single vertex class; (v) handle and crosscap grouping; (vi) Dyck's theorem; (vii) the closed orientable and nonorientable normal forms; (viii) the relative theorem for distinguished cap faces. + +--- + +## Layer 7: Cellulation homology and the edge-path group + +This layer attaches finite chain complexes and finite group presentations to a cellulation. The chain complex and its homology are needed for classification. The edge-path group is a natural companion that records the nonabelian presentation before abelianization. Both are combinatorial models of familiar topological invariants, but their comparison with singular homology and the topological fundamental group is out of scope. + +**Representative formal statements.** + +```lean +/-- Three finite free modules and two matrices. -/ +def Cellulation2.chainComplex (C : Cellulation2) (R : Type*) [CommRing R] : + ChainComplex (ModuleCat R) ℕ + +theorem Cellulation2.d_comp_d (C : Cellulation2) : C.boundary₁ ∘ₗ C.boundary₂ = 0 + +def Cellulation2.homology (C : Cellulation2) (R : Type*) [CommRing R] (i : ℕ) : ModuleCat R + +theorem Cellulation2.eulerPoincare (C : Cellulation2) (F : Type*) [Field F] : + C.eulerChar = ∑ i, (-1 : ℤ) ^ i * Module.finrank F (C.homology F i) + +theorem Cellulation2.homology_zero_iff_connected : ... +theorem Cellulation2.homology_two_iff_orientable + (h : C.IsClosed ∧ C.IsConnected) : + Nontrivial (C.homology ℤ 2) ↔ C.IsOrientable + +/-- The combinatorial fundamental group. -/ +def Cellulation2.edgePathGroup (C : Cellulation2) : Group -- presented + +theorem Cellulation2.edgePathGroup_presentation (C : Cellulation2) (T : C.SpanningTree) : + C.edgePathGroup ≃* PresentedGroup (generators := edges off T) (relations := face words) + +theorem Cellulation2.abelianization_edgePathGroup : + Abelianization C.edgePathGroup ≃* C.homology ℤ 1 + +theorem Graph.edgePathGroup_free (Γ : Graph α β) (h : Γ.Connected) : + IsFreeGroup Γ.edgePathGroup ∧ Nat.card (FreeGroup.basis Γ.edgePathGroup) = 1 - Γ.eulerChar + +/-- Invariance, from the moves and nothing else. -/ +theorem Cellulation2.homology_subdivision : (C.subdivide).homology R i ≅ C.homology R i +theorem Cellulation2.edgePathGroup_subdivision : (C.subdivide).edgePathGroup ≃* C.edgePathGroup + +/-- The normal forms. Uses the PID structure theorem, not Smith normal form. -/ +theorem homology_normalFormOrientable (g : ℕ) : + (normalFormOrientable g).homology ℤ 1 ≅ (ℤ : Type) ^ (2 * g) +theorem homology_normalFormNonorientable (k : ℕ) (hk : 0 < k) : + (normalFormNonorientable k hk).homology ℤ 1 ≅ (ℤ : Type) ^ (k - 1) × ZMod 2 +``` + +**Proof strategy and formalization notes.** + +- Abelianizing a presentation turns relators into the columns of the boundary matrix, so `abelianization_edgePathGroup` is a mechanical algebraic theorem and not a topological one. This is Munkres' strategy with the topology removed. +- ⚠ Use `Mathlib.Algebra.Module.PID`, not `TauCeti/LinearAlgebra/Matrix/SmithNormalForm.lean`, which handles only square matrices of positive determinant. +- ⚠ van Kampen is out of scope. The edge-path group is defined combinatorially and its invariance comes from the moves, so no comparison with `π₁` of the realization is needed. +- Cross-check opportunity: `TauCeti/AlgebraicTopology/UniversalCover/` already computes the fundamental groups of the circle, the torus, and the real projective plane. Comparing those against `edgePathGroup` of the corresponding normal forms is not a required but it would be strong independent evidence and is worth attempting for these models. + +**Examples and mathematical checks.** The chain complexes of the layer 1 table are written out explicitly and `d_comp_d` is checked by `decide`. `homology_two_iff_orientable` is checked **false** for the Klein bottle and **true** for the torus. The `ZMod 2` torsion class in `homology_normalFormNonorientable` is exhibited, not merely asserted, since it is what distinguishes the nonorientable normal forms and an off-by-one here would be invisible. + +**Natural intermediate results.** (i) the chain complex and `d ∘ d = 0`; (ii) homology and Euler-Poincaré; +(iii) `H₀` and connectedness; (iv) `H₂` and orientability; (v) the edge-path group and its presentation; (vi) abelianization; (vii) free groups for graphs; (viii) the normal-form computations; (ix) invariance under the moves. + +--- + +## Layer 8: The classification of compact surfaces + + +**Representative formal statements.** + +```lean +inductive StandardSurface + | orientable (g : ℕ) (b : ℕ) + | nonorientable (k : ℕ) (hk : 0 < k) (b : ℕ) + +def StandardSurface.model : StandardSurface → Type +def StandardSurface.eulerChar : StandardSurface → ℤ + -- orientable g b => 2 - 2*g - b ; nonorientable k hk b => 2 - k - b + +/-- Existence. -/ +theorem exists_standard_homeomorph (M : Type*) [CompactConnectedSurface M] : + ∃ S : StandardSurface, Nonempty (M ≃ₜ S.model) + +/-- Uniqueness. -/ +theorem standard_homeomorph_unique {S T : StandardSurface} + (h : Nonempty (S.model ≃ₜ T.model)) : S = T + +/-- The library statement. -/ +theorem classification_of_surfaces (M : Type*) [CompactConnectedSurface M] : + ∃! S : StandardSurface, Nonempty (M ≃ₜ S.model) + +/-- The complete invariant. -/ +theorem homeomorph_iff_invariants {M N : Type*} + [CompactConnectedSurface M] [CompactConnectedSurface N] : + Nonempty (M ≃ₜ N) ↔ + Surface.eulerChar M = Surface.eulerChar N ∧ + (IsOrientable M ↔ IsOrientable N) ∧ + boundaryComponentCount M = boundaryComponentCount N + +/-- The reduction that makes the boundary case cheap. -/ +theorem exists_closed_minus_discs (M : Type*) [CompactConnectedSurface M] : + ∃ (N : Type) (_ : ClosedConnectedSurface N) (b : ℕ), Nonempty (M ≃ₜ N.minusDiscs b) +``` + +**Proof strategy and formalization notes.** + +- Existence: Radó gives a triangulation, layer 3 gives a generalized map, layer 6 reduces the schema to normal form, and layer 4's realization theorems transport the homeomorphism back. +- Uniqueness: layer 7's invariants separate the normal forms. Euler characteristic separates within each family, orientability separates the families, and boundary count is preserved because ⚠ `∂M` is a topological invariant only by `PlanarTopology`'s + `invarianceOfDomain₂`. +- ⚠ The `∃!` form is the form for the library. A quotient-and-representative form, of the kind lean-eval statements use, is a a bridge if it appears at all. +- The boundary case leverages `exists_closed_minus_discs`, via layer 4's `cap`, but the attached discs cannot simply be forgotten. One must either carry the cap faces as marked faces through the relative normal-form theorem of layer 6, or prove an ambient theorem that any two finite families of disjoint discs in a connected surface are equivalent. In any case, avoid using Schoenflies for the classification, it's not needed. + +**Examples and mathematical checks.** The classification is instantiated on a surface presented only by charts, with no combinatorial data supplied, and produces the correct `StandardSurface`. The completeness statement is accompanied by a sharpness table. If Euler characteristic is dropped, the torus and the closed orientable genus-two surface agree on orientability and boundary count. If orientability is dropped, the torus and Klein bottle agree on Euler characteristic and boundary count. If boundary count is dropped, the torus and annulus agree on Euler characteristic and orientability. Dyck's theorem is exercised by identifying a torus connected-summed with a projective plane with the nonorientable genus-three surface. + +**Natural intermediate results.** (i) `StandardSurface` and its models; (ii) existence in the closed case; (iii) capping with marked cap faces; (iv) relative reduction and uncapping; (v) existence with boundary; (vi) uniqueness; (vii) the complete invariant and its sharpness table. + +**Consequences.** `GeometricTopology` layer 9. Layer 5's `Graph.genus`. + +--- + +## Follow-on layer 9: Curves, cutting, and mapping class groups + +To fix the convention that the theorem statements use: For oriented surfaces, Dehn twists and the Lickorish theorem concern orientation-preserving mapping classes. For surfaces with boundary, the standard base cases use homeomorphisms and isotopies fixing the boundary pointwise. The full mapping class group is stated separately. + +**From PlanarTopology.** Schoenflies, tameness of arcs and simple closed curves in a surface, and isotopy to a PL homeomorphism. + +**Representative formal statements.** + +```lean +def SimpleClosedCurve (M : Type*) [Surface M] : Type* +def IsEssential {M} [Surface M] (c : SimpleClosedCurve M) : Prop +def IsSeparating {M} [Surface M] (c : SimpleClosedCurve M) : Prop + +def cutAlong {M} [Surface M] (c : SimpleClosedCurve M) : Type* +theorem eulerChar_cutAlong : Surface.eulerChar (cutAlong c) = Surface.eulerChar M + +/-- Full mapping classes, with no orientation restriction. -/ +def MappingClassGroupFull (M : Type*) [Surface M] : Type* := + Homeomorph M M ⧸ isotopicSetoid + +/-- Orientation-preserving mapping classes; in the boundary case the maps and isotopies + fix the boundary pointwise. -/ +def MappingClassGroupPlus (M : Type*) [OrientedSurface M] : Type* := ... + +/-- Base cases, with conventions made explicit. -/ +theorem mcg_disc_rel_boundary : MappingClassGroupPlus Disc ≃* Unit +theorem mcg_annulus_rel_boundary : MappingClassGroupPlus Annulus ≃* Multiplicative ℤ +theorem mcg_sphere_plus : MappingClassGroupPlus Sphere2 ≃* Unit +theorem mcg_sphere_full : MappingClassGroupFull Sphere2 ≃* ZMod 2 + +def dehnTwist {M} [OrientedSurface M] (c : SimpleClosedCurve M) : + MappingClassGroupPlus M + +/-- The workhorse of the induction. -/ +theorem change_of_coordinates {M} [ClosedConnectedOrientedSurface M] + (c d : SimpleClosedCurve M) (hc : ¬ IsSeparating c) (hd : ¬ IsSeparating d) : + ∃ f : OrientationPreservingHomeomorph M M, f '' c.carrier = d.carrier + +theorem mcg_torus_plus : + MappingClassGroupPlus Torus ≃* Matrix.SpecialLinearGroup (Fin 2) ℤ +theorem mcg_torus_full : + MappingClassGroupFull Torus ≃* Matrix.GeneralLinearGroup (Fin 2) ℤ + +/-- Dehn--Lickorish, for a closed connected oriented surface of positive genus. -/ +theorem dehn_lickorish {M} [ClosedConnectedOrientedSurface M] (hg : 0 < genus M) : + Subgroup.closure (Set.range (dehnTwist (M := M))) = ⊤ ∧ + ∃ S : Finset (SimpleClosedCurve M), S.card = 3 * genus M - 1 ∧ + Subgroup.closure (dehnTwist '' S) = ⊤ + +/-- Category comparisons, for the same orientation and boundary convention. -/ +theorem mcg_top_eq_pl {M} [CompactOrientedSurface M] : + MappingClassGroupTopPlus M ≃* MappingClassGroupPLPlus M +theorem mcg_pl_eq_smooth {M} [CompactOrientedSurface M] : + MappingClassGroupPLPlus M ≃* MappingClassGroupSmoothPlus M +``` + +**Proof strategy and formalization notes.** + +- A **Dehn twist** about a simple closed curve is supported in an annular neighbourhood, rotates once across the annulus, and is the identity outside. Tameness and the collar theorem from `PlanarTopology` provide the annulus, while the isotopy class is independent of the chosen collar. +- The distinction between `MappingClassGroupPlus` and `MappingClassGroupFull` is essential. Dehn twists generate the orientation-preserving group: for the torus this is `SL(2,ℤ)`, whereas the full group is `GL(2,ℤ)`. Likewise, the usual disc and annulus base cases require the boundary to be fixed pointwise. +- Target Lickorish's generating set of `3g - 1` twists. Humphries' minimal `2g + 1` set and its minimality proof are a separate theorem and remain out of scope. +- Do not write “of finite type” for compact surfaces. In this literature the phrase normally signals punctures as well as boundary components, leading to the Birman exact sequence and point-pushing, which are out of scope. + +**Examples and mathematical checks.** On the torus, twists about the two standard curves map to the elementary generators of `SL(2,ℤ)`. A separating and a nonseparating curve on a genus-two surface show that the nonseparating hypothesis in the change-of-coordinates principle is necessary. A twist about a curve bounding a disc represents the identity mapping class. + +**Natural intermediate results.** (i) simple closed curves, essentiality, and separation; (ii) cutting and its Euler characteristic; (iii) full, positive, and relative-boundary mapping class groups; (iv) the base cases; (v) Dehn twists; (vi) the change-of-coordinates principle; (vii) the torus computations; (viii) the Lickorish induction; (ix) the category comparisons. + +**Consequences.** `GeometricTopology` layer 9. + +--- + +## Follow-on layer 10: Planarity + +This layer is not needed for the classification theorem. It is a substantial mathematical extension that tests the embedding, duality, and cellulation theories against the classical theorems of planar graph theory: Kuratowski tests embeddings, Whitney tests the interaction between connectivity and duality, Mac Lane compares cycle-space algebra with planarity, and the five-colour theorem carries the plane-map theory to a nontrivial conclusion. + +The intended scope is **Mohar and Thomassen, *Graphs on Surfaces*, chapter 2**, together with Fáry's theorem and Wagner's theorem. This is not intended to be a full roadmap of topological graph theory. + +**Out of scope:** planarity-testing algorithms such as Hopcroft–Tarjan and LR-planarity (the theorems are the target, not the algorithms); Steinitz's theorem (a convexity theorem needing polytope machinery not built here); embeddings in general surfaces, face-width, edge-width, embedding extension, and Robertson–Seymour (a separate subject and a separate roadmap); Grötzsch's theorem (named as a known gap rather than silently omitted); the four colour theorem and the Heawood/Ringel–Youngs map colour theorem (see the roadmap-for-a-roadmap below). + +**Representative formal statements.** + +```lean +theorem eulerFormula_plane {Γ : Graph α β} (e : PlaneEmbedding Γ) (h : Γ.Connected) : + (Γ.vertexCount : ℤ) - Γ.edgeCount + e.faceCount = 2 +theorem edge_bound_of_planar (Γ : Graph α β) (h : Γ.IsPlanar) (hs : Γ.IsSimple) + (h3 : 3 ≤ Γ.vertexCount) : Γ.edgeCount ≤ 3 * Γ.vertexCount - 6 +theorem exists_vertex_degree_le_five (Γ : Graph α β) (h : Γ.IsPlanar) + (hs : Γ.IsSimple) (hV : 0 < Γ.vertexCount) : ∃ v, Γ.degree v ≤ 5 + +/-- Connectivity machinery. -/ +/-- Tutte's Wheel Theorem. -/ +theorem exists_wheel_reduction (Γ : Graph α β) (h : Γ.IsThreeConnected) : ... +theorem exists_contractible_edge (Γ : Graph α β) (h : Γ.IsThreeConnected) + (h5 : 5 ≤ Γ.vertexCount) : ∃ e, (Γ.contract e).IsThreeConnected + +/-- Kuratowski, via Thomassen's 3-connectivity induction. -/ +theorem isPlanar_iff_no_K5_K33_topologicalMinor (Γ : Graph α β) (hs : Γ.IsSimple) : + Γ.IsPlanar ↔ ¬ Γ.HasTopologicalMinor (completeGraph 5) ∧ + ¬ Γ.HasTopologicalMinor (completeBipartiteGraph 3 3) + +/-- Wagner's Theorem. -/ + +theorem isPlanar_iff_no_K5_K33_minor (Γ : Graph α β) (hs : Γ.IsSimple) : + Γ.IsPlanar ↔ ¬ Γ.HasMinor (completeGraph 5) ∧ + ¬ Γ.HasMinor (completeBipartiteGraph 3 3) +theorem isPlanar_minorClosed : Γ.IsPlanar → Δ.IsMinorOf Γ → Δ.IsPlanar + +/-- Tutte's Peripheral Cycle Theorem. -/ +theorem isPeripheral_iff_isFacial (Γ : Graph α β) (h : Γ.IsThreeConnected) (e : PlaneEmbedding Γ) : + ∀ C, C.IsPeripheral ↔ e.IsFacial C + +/-- Whitney's Unique Embedding Theorem. -/ +theorem planeEmbedding_unique_up_to_equivalence (Γ : Graph α β) (h : Γ.IsThreeConnected) + (h' : Γ.IsPlanar) : Subsingleton (PlaneEmbedding Γ / EquivalenceOfEmbeddings) + +/-- Whitney's 2-Isomorphism Theorem. -/ +theorem cycleMatroid_iso_iff_twoIsomorphic (Γ Δ : Graph α β) : ... + +/-- Cycle space, cut space, duality, Mac Lane. -/ +def Graph.cycleSpace (Γ : Graph α β) : Submodule (ZMod 2) (β → ZMod 2) +def Graph.cutSpace (Γ : Graph α β) : Submodule (ZMod 2) (β → ZMod 2) +theorem cycleSpace_finrank : Module.finrank (ZMod 2) Γ.cycleSpace + = Γ.edgeCount - Γ.vertexCount + Γ.componentCount +theorem cycleSpace_orthogonal_cutSpace : ... +theorem planar_dual_cycleSpace_eq_cutSpace (e : PlaneEmbedding Γ) : ... + +/-- Mac Lane's Planarity Criterion. -/ +def Graph.HasTwoBasis (Γ : Graph α β) : Prop := ... + +theorem isPlanar_iff_hasTwoBasis (Γ : Graph α β) (hs : Γ.IsSimple) : + Γ.IsPlanar ↔ Γ.HasTwoBasis + +/-- Straight-line and convex embeddings. -/ +/-- Fáry's Theorem. -/ +theorem exists_straightLine_planeEmbedding (Γ : Graph α β) (hs : Γ.IsSimple) (h : Γ.IsPlanar) : + ∃ e : PlaneEmbedding Γ, e.IsStraightLine + +/-- Tutte's Spring Embedding Theorem. -/ +theorem exists_convex_planeEmbedding (Γ : Graph α β) (h : Γ.IsThreeConnected) (h' : Γ.IsPlanar) : + ∃ e : PlaneEmbedding Γ, e.IsConvex + +/-- The Five Color Theorem -/ + +theorem colorable_five_of_isPlanar (Γ : Graph α β) (hs : Γ.IsSimple) (h : Γ.IsPlanar) : + Γ.Colorable 5 +``` + +**Proof strategy and formalization notes.** + +- ⚠ Use **Thomassen's** proof of Kuratowski, via contracting an edge in a 3-connected graph. It is shorter and considerably more formalization-friendly than the Tutte and Bondy–Murty's approach using bridges and conflict graphs. Also, the 3-connectivity machinery it needs (the wheel theorem, contractible edges) is shared with Whitney. +- The dual of a simple plane graph need not be simple, which is why duality lives on multigraphs and why layer 1 didn't build on `SimpleGraph` as the foundation. +- Tutte's spring embedding is a linear-algebra argument and is unusually formalization-friendly for its strength. Its precise form fixes a facial cycle as a convex outer polygon and produces a straight-line embedding with convex faces. It is the natural bridge toward Steinitz. +- Prove Fáry via Tutte. Given simple planar Γ on at least 4 vertices, add edges within a fixed embedding until it is maximal planar. Maximal planar graphs on at least 4 vertices are 3-connected. Apply Tutte, then delete the added edges. The remaining segments are still non-crossing. +- Whitney's unique-embedding theorem and Whitney's 2-isomorphism theorem are different results. Target both, and do not cite the 2-isomorphism paper for the unique-embedding statement. The unique-embedding theorem is uniqueness up to a homeomorphism of the sphere, allowing orientation reversal; with orientation-preserving equivalence, the two mirror-image embeddings remain distinct. + +**Examples and mathematical checks.** Explicit finite models verify that `K₅` and `K₃,₃` +are non-planar and that `K₄` is planar. `edge_bound_of_planar` is checked to **fail** for a multigraph with parallel edges, exhibiting the necessity of `IsSimple`. `whitney_unique_embedding` is checked to **fail** for a 2-connected but not 3-connected planar graph, with two inequivalent embeddings exhibited. `maclane` is checked against `K₅`, whose cycle space has no sparse basis. Five-colouring is computed on a concrete triangulation with a degree-5 vertex requiring a Kempe chain interchange. + +**Natural intermediate results.** (i) plane embeddings, faces, and Euler's formula; (ii) the edge bound and the degree-5 lemma; (iii) minors, topological minors, and minor-closure; (iv) the 3-connectivity machinery; (v) Kuratowski; (vi) Wagner and the equivalence; (vii) peripheral cycles; (viii) Whitney unique embedding; (ix) Whitney 2-isomorphism; (x) cycle and cut spaces; (xi) planar duality of the two spaces; (xii) Mac Lane; (xiii) Tutte's spring embedding;(xiv) Fáry; (xv) the five-colour theorem. + +--- + +## Roadmap-for-a-roadmap: map colouring + +This section is motivation for a separate future roadmap and is not work here. + +With plane maps, duality, Euler's formula, and the five-colour theorem in place, the four colour theorem becomes a specification problem rather than a foundations problem: an unavoidable set, discharging configurations, and a verified reducibility check. Gonthier's Coq development is the reference for how the statement and the discharging argument should be +encoded, and its use of hypermaps is the reason this roadmap on permutations rather than on `SimpleGraph`. The Heawood map colour theorem and the Ringel–Youngs solution for higher genus are the natural companions, and they consume layer 5's `Graph.genus`. + +--- + +## Out of scope + +- Everything in [PlanarTopology](../PlanarTopology/README.md): the Jordan curve theorem, Schoenflies, Radó, the Hauptvermutung, the PL toolkit, invariance of domain, tameness. +- Punctured surfaces, the Birman exact sequence, point pushing, and the mapping class groups of surfaces with marked points. +- Humphries' minimal generating set and the presentation of the mapping class group. +- Teichmüller theory, hyperbolic structures, and geodesic representatives. +- Non-compact surfaces and their classification. +- Singular homology, van Kampen, Mayer–Vietoris, cohomology, duality. See the encoding + conventions on invariance. +- Higher-dimensional generalized maps beyond the dimension-polymorphic definition itself. +- Planarity-testing algorithms and the other layer 10 exclusions listed above. +- Dessins d'enfants, ribbon graphs, and the Galois action, which are natural follow-ons to + layers 1 through 5 but are a different subject. + +- +## References + +- G. Damiand and P. Lienhardt, *Combinatorial Maps: Efficient Data Structures for Computer Graphics and Image Processing*. The definition of generalized maps, the non-degeneracy conditions, and the operations in layer 4. +- J.-F. Dufourd and collaborators, and Dehlinger–Dufourd, *Formalizing generalized maps in Coq*. The prior formalization experience. +- G. Gonthier, *Formal proof: the four-color theorem*, Notices AMS **55** (2008). The hypermap encoding and the discipline of deriving graphs from maps. +- S. Lando and A. Zvonkin, *Graphs on Surfaces and Their Applications*, chapter 1. The identification of embedded graphs with combinatorial maps, which is layer 5. +- B. Mohar and C. Thomassen, *Graphs on Surfaces*, chapter 2. The scope statement for layer 10, and the proof strategy for Whitney and Mac Lane. +- C. Thomassen, *Kuratowski's theorem*, J. Graph Theory **5** (1981). Kuratowski reference for layer 10. +- W. B. R. Lickorish, *A finite set of generators for the homeotopy group of a 2-manifold*, Proc. Cambridge Philos. Soc. **60** (1964). The generating set targeted in layer 9. +- B. Farb and D. Margalit, *A Primer on Mapping Class Groups*, chapters 1–4. The change-of-coordinates principle and the Lickorish induction as presented for a modern reader. +- J. R. Munkres, *Topology*, chapter 12. The classification via normal forms and abelianization, which is the proof strategy in layers 6 through 8 with the topology replaced by the Hauptvermutung. +- E. Moise, *Geometric Topology in Dimensions 2 and 3*, chapter 8, and A. Gallier and D. Xu, *A Guide to the Classification Theorem for Compact Surfaces*. The classification itself. \ No newline at end of file diff --git a/TauCetiRoadmap/SurfaceTopology/Suggested.lean b/TauCetiRoadmap/SurfaceTopology/Suggested.lean new file mode 100644 index 00000000..6ffdc484 --- /dev/null +++ b/TauCetiRoadmap/SurfaceTopology/Suggested.lean @@ -0,0 +1,429 @@ +import Mathlib +import TauCeti.AlgebraicTopology.SimplicialComplex.Realization +import TauCeti.Topology.JordanCurve.Basic +import TauCeti.Topology.Triangulable + +/-! +# Surface topology, finite presentations, and classification: target signatures + +**This file is not the roadmap and is not exhaustive.** The definitive document is +`README.md`. The declarations here suggest Lean forms for load-bearing objects and +particular milestones, so that contributors and reviewers converge on names and +signatures; discharging all of them finishes neither a layer nor the roadmap. `sorry` is +allowed in this human-owned roadmap library: these are targets, not completed proofs. + +This roadmap deliberately chooses two-dimensional generalized maps as the finite hub. +Oriented maps, hypermaps, cellulations, and polygonal schemas are presentations of the +same finite surface data; realization, Euler characteristic, orientability, and the main +operations are defined at the hub and compared to the other presentations. The core +layers culminate in classification; mapping class groups and planarity are substantial +follow-on layers. + +The file therefore pins more object-level vocabulary than many roadmaps do. Where the +README itself marks a definition as unresolved -- most importantly the exact local +nondegeneracy condition characterizing surface generalized maps -- this file does **not** +replace it by `Prop := sorry`. Such conditions remain comments until they can be stated +honestly. Likewise, graph-facing targets remain schematic until the current multigraph +API has been verified, as required by the roadmap. +-/ + +noncomputable section + +namespace TauCetiRoadmap.SurfaceTopology + +open Function Set + +universe u v w + +/-! ## Layer 0: finite conventions -/ + +/-- A finite cyclic word with repeated labels, modulo cyclic rotation. The implementation +should remain separate from `CircularOrder` and from the topological circle. -/ +def CyclicWord (α : Type u) : Type u := + sorry + +/-- A bundled finite indexing type. Moves which add or remove cells must not pretend to +live on a fixed ambient type. -/ +structure BundledFinite where + ι : Type u + fintype : Fintype ι + decEq : DecidableEq ι + +/-! +The isomorphism closure used by move relations should be compiled once the concrete +bundled object is known. The important constraint is that `Relation.ReflTransGen` is +applied *after* closing the elementary relation under isomorphism of the bundled index +type; Pachner/schema moves change that type. +-/ + +/-! ## Layer 1: generalized maps -/ + +/-- An `n`-dimensional generalized map: `n+1` involutions, with non-neighbouring +involutions commuting. This definition is dimension-polymorphic even though the roadmap +only develops the two-dimensional theory. -/ +structure GMap (n : ℕ) (D : Type u) [Fintype D] [DecidableEq D] where + adj : Fin (n + 1) → Equiv.Perm D + involutive : ∀ i, Function.Involutive (adj i) + commute_of_far : ∀ i j, i.1 + 2 ≤ j.1 → Function.Commute (adj i) (adj j) + +abbrev GMap2 (D : Type u) [Fintype D] [DecidableEq D] := GMap 2 D + +/-- The `i`-cells are the orbits generated by all adjacencies except `αᵢ`. +The implementation should use Mathlib's orbit/subgroup machinery rather than a private +reachability relation. -/ +noncomputable def GMap.Cell {n : ℕ} {D : Type u} [Fintype D] [DecidableEq D] + (G : GMap n D) (i : Fin (n + 1)) : Type u := + sorry + +/-- Cells of a finite generalized map are finite orbit quotients. -/ +noncomputable instance GMap.instFiniteCell {n : ℕ} {D : Type u} + [Fintype D] [DecidableEq D] (G : GMap n D) (i : Fin (n + 1)) : + Finite (G.Cell i) := + sorry + +/-- Isomorphism of two-dimensional generalized maps, allowing the dart type to change. -/ +structure GMap2.Iso {D : Type u} {D' : Type v} + [Fintype D] [DecidableEq D] [Fintype D'] [DecidableEq D'] + (G : GMap2 D) (G' : GMap2 D') where + toEquiv : D ≃ D' + map_adj : ∀ i d, toEquiv (G.adj i d) = G'.adj i (toEquiv d) + +/-- Euler characteristic from orbit cells. -/ +def GMap2.eulerChar {D : Type u} [Fintype D] [DecidableEq D] (G : GMap2 D) : ℤ := + (Nat.card (G.Cell 0) : ℤ) - Nat.card (G.Cell 1) + Nat.card (G.Cell 2) + +/-- A boundary dart is a fixed point of the highest-order involution. -/ +def GMap2.IsBoundaryDart {D : Type u} [Fintype D] [DecidableEq D] + (G : GMap2 D) (d : D) : Prop := + G.adj 2 d = d + +/-- Orientability as bipartiteness of the dart-adjacency graph, ignoring fixed +adjacencies representing boundary. -/ +def GMap2.IsOrientable {D : Type u} [Fintype D] [DecidableEq D] (G : GMap2 D) : Prop := + ∃ S : Set D, ∀ i d, G.adj i d ≠ d → (d ∈ S ↔ G.adj i d ∉ S) + +/-- A chosen orientation is extra data; `IsOrientable` is only the existence property. -/ +structure GMap2.Orientation {D : Type u} [Fintype D] [DecidableEq D] (G : GMap2 D) where + side : Set D + flips : ∀ i d, G.adj i d ≠ d → (d ∈ side ↔ G.adj i d ∉ side) + +/-- A generalized map with its finite dart type bundled. This is the codomain of moves +which change the number or type of darts. -/ +structure BundledGMap2 where + D : Type u + fintypeD : Fintype D + decEqD : DecidableEq D + map : @GMap 2 D fintypeD decEqD + +/-! +**Do not compile `IsSurfaceGMap` yet as a placeholder proposition.** The exact finite +local nondegeneracy condition is the highest-risk definition in the roadmap. It must be +settled against Damiand--Lienhardt, must admit one-cell presentations such as the +projective-plane word `aa`, and must be proved equivalent to the realization having only +disc or half-disc neighbourhoods. Once pinned, add: + + def IsSurfaceGMap (G : GMap2 D) : Prop := + (∀ d, G.adj 0 d ≠ d) ∧ (∀ d, G.adj 1 d ≠ d) ∧ + + def IsClosedSurfaceGMap (G : GMap2 D) : Prop := + IsSurfaceGMap G ∧ ∀ d, G.adj 2 d ≠ d + +and the boundary-component count, connectedness API, and orientable/nonorientable genus +formulas. The explicit sphere/projective-plane/torus/Klein-bottle/disc/annulus/Möbius +examples belong in the implementation as decidable tests of this definition. +-/ + +/-! ## Layer 2: presentations and comparison theorems -/ + +/-- An oriented combinatorial map / rotation system. -/ +structure CombinatorialMap (D : Type u) [Fintype D] [DecidableEq D] where + sigma : Equiv.Perm D + alpha : Equiv.Perm D + alpha_involutive : Function.Involutive alpha + alpha_free : ∀ d, alpha d ≠ d + +/-- Passing from an oriented map to the unoriented generalized-map hub doubles darts. -/ +noncomputable def CombinatorialMap.toGMap2 {D : Type u} [Fintype D] [DecidableEq D] + (M : CombinatorialMap D) : GMap2 (D × Bool) := + sorry + +/-- A hypermap in the three-permutation presentation. -/ +structure Hypermap (D : Type u) [Fintype D] [DecidableEq D] where + sigma : Equiv.Perm D + phi : Equiv.Perm D + alpha : Equiv.Perm D + comp : sigma * phi * alpha = 1 + +/-- Conversion from a hypermap to the generalized-map hub. -/ +noncomputable def Hypermap.toGMap2 {D : Type u} [Fintype D] [DecidableEq D] + (H : Hypermap D) : GMap2 (D × Bool) := + sorry + +/-- Polygonal schemas are bundled because relabelling and cancellation change the label +type. Surface validity is a separate predicate; do not hide it in an unconstrained field. -/ +structure PolygonalSchema where + label : Type u + fintypeLabel : Fintype label + decEqLabel : DecidableEq label + faces : List (CyclicWord (label × Bool)) + +/-! +`Cellulation2` should be compiled only after its side-incidence representation is pinned. +It is not merely an incidence poset: the roadmap requires a concrete counterexample of +two non-isomorphic cellulations with the same incidence poset. + +The six comparison theorems are central targets, but most wait on the realization and +subdivision APIs. Representative forms are: + + -- After canonical subdivision, the generalized-map flag complex agrees with the + -- barycentric subdivision of a combinatorial surface. + theorem flagComplex_toGMap2 ... : ... + + theorem realization_homeomorph_flagComplex ... : ... + theorem toCellulation_toGMap2 ... : ... + theorem toGMap2_toCombinatorialMap ... : ... + theorem dual_dual ... : ... + theorem schema_conversion_recovers_gluings ... : ... +-/ + +/-! ## Layer 3: realization -/ + +/-- Direct topological realization of a generalized map as triangles modulo side gluings. +It is intentionally defined for every generalized map, before imposing the surface +condition, and not through an abstract simplicial complex. -/ +noncomputable def GMap2.realization {D : Type u} [Fintype D] [DecidableEq D] + (G : GMap2 D) : Type u := + sorry + +/-- The quotient realization carries its quotient topology. -/ +noncomputable instance GMap2.realizationTopologicalSpace + {D : Type u} [Fintype D] [DecidableEq D] (G : GMap2 D) : + TopologicalSpace G.realization := + sorry + +/-- The direct realization of a finite generalized map is compact. -/ +instance GMap2.realizationCompactSpace + {D : Type u} [Fintype D] [DecidableEq D] (G : GMap2 D) : + CompactSpace G.realization := + sorry + +/-! +Once `IsSurfaceGMap` and the simplicial subdivision bridge exist, add the decisive +milestones: + + theorem IsSurfaceGMap.realization_isSurface ... + theorem IsSurfaceGMap.eulerChar_eq ... + theorem flagComplex_isSimplicial_of_subdivided ... + theorem realization_homeomorph_flagComplex ... + theorem exists_gmap_of_compactSurface ... + +The projective-plane `aa` map must remain an explicit counter-witness to defining +realization through the unsubdivided flag complex. +-/ + +/-! ## Layer 4: operations on finite surfaces -/ + +/-- Edge subdivision changes the dart type, hence returns a bundled map. -/ +noncomputable def GMap2.subdivideEdge {D : Type u} [Fintype D] [DecidableEq D] + (G : GMap2 D) (e : G.Cell 1) : BundledGMap2 := + sorry + +/-- Face subdivision likewise changes the dart type. -/ +noncomputable def GMap2.subdivideFace {D : Type u} [Fintype D] [DecidableEq D] + (G : GMap2 D) (f : G.Cell 2) : BundledGMap2 := + sorry + +/-- Ordinary duality reverses the three adjacencies. It is defined combinatorially for +all maps; preservation of the chosen surface-with-boundary convention is asserted only +under the appropriate closedness hypothesis. -/ +noncomputable def GMap2.dual {D : Type u} [Fintype D] [DecidableEq D] + (G : GMap2 D) : GMap2 D := + sorry + +/-- The orientation double cover has two sheets indexed by `Bool`. -/ +noncomputable def GMap2.orientationDoubleCover + {D : Type u} [Fintype D] [DecidableEq D] (G : GMap2 D) : GMap2 (D × Bool) := + sorry + +/-- Capping all boundary circles may change the dart type. -/ +noncomputable def GMap2.cap {D : Type u} [Fintype D] [DecidableEq D] + (G : GMap2 D) : BundledGMap2 := + sorry + +/-- Doubling along the boundary uses two copies of the dart set. -/ +noncomputable def GMap2.double {D : Type u} [Fintype D] [DecidableEq D] + (G : GMap2 D) : GMap2 (D × Bool) := + sorry + +/-- Connected sum is another index-changing operation. -/ +noncomputable def GMap2.connectedSum + {D : Type u} {E : Type v} + [Fintype D] [DecidableEq D] [Fintype E] [DecidableEq E] + (G : GMap2 D) (H : GMap2 E) : BundledGMap2 := + sorry + +/-! +Admissible edge contraction and cutting along a combinatorial curve should be compiled +only after `IsContractible` and `CombinatorialCurve` are real predicates/types. Their +realization theorems, not merely orbit-count identities, are the milestones. + +Likewise add the precise covering theorem for `orientationDoubleCover`, including the +boundary behaviour, and the Euler-characteristic/orientability/connectedness formulas for +capping and doubling. +-/ + +/-! ## Layer 5: embedded graphs and the Heffter--Edmonds--Ringel correspondence -/ + +/-! +The README explicitly requires verification of Mathlib's current multigraph `Graph α β` +API before this layer. Until that check is done, do not create a private graph synonym +merely to make the targets parse. Once verified, pin: + + def GMap2.underlyingGraph ... + structure GraphEmbedding ... + def GraphEmbedding.IsCellular : Prop := ... + def RotationSystem ... + def SignedRotationSystem ... + + theorem cellularEmbeddings_equiv_gmaps ... + theorem orientedCellularEmbeddings_equiv_rotationSystems ... + theorem cellularEmbeddings_equiv_signedRotationSystems ... + theorem vertexCount_sub_edgeCount_add_faceCount_eq_eulerChar ... + +The cellularity hypothesis is essential and should have the torus/non-disc-face +counterexample beside the implementation. +-/ + +/-! ## Layer 6: polygonal schemas and normal forms -/ + +/-! +Once `PolygonalSchema.IsSurface`, schema relabelling, and the isomorphism closure are +concrete, compile the elementary move relation and the two headline targets: + + theorem closedSchema_reduces_to_normalForm ... + theorem closedSchema_reduces_to_normalForm_rel_caps ... + theorem SchemaMove.realization_homeomorph ... + +The relative theorem preserving distinguished cap faces is not optional bookkeeping: it +is what makes classification with boundary reduce cleanly to the closed case. +-/ + +/-! ## Layer 7: cellulation homology and the edge-path group -/ + +/-! +This layer waits on `Cellulation2`. When that presentation is pinned, representative +targets should include the finite chain complex, `d ∘ d = 0`, Euler--Poincaré, the +combinatorial edge-path-group presentation, abelianization, subdivision invariance, and +the two normal-form computations. Use the PID structure theorem for the rectangular +boundary matrices; do not route through the current square-matrix Smith-normal-form file. + +Keep the names presentation-specific (`Cellulation2.homology`, +`Cellulation2.edgePathGroup`) until comparison with singular homology / topological `π₁` +actually exists. +-/ + +/-! ## Layer 8: classification of compact surfaces -/ + +/-- The standard connected compact surfaces, including boundary. -/ +inductive StandardSurface where + | orientable (g : ℕ) (b : ℕ) + | nonorientable (k : ℕ) (hk : 0 < k) (b : ℕ) + +/-- A topological model of each standard surface. The concrete models are fixed by the +implementation, not by the classification theorem. -/ +noncomputable def StandardSurface.model : StandardSurface → Type := + sorry + +/-- Euler characteristic of the standard model. -/ +def StandardSurface.eulerChar : StandardSurface → ℤ + | .orientable g b => 2 - 2 * (g : ℤ) - (b : ℤ) + | .nonorientable k _ b => 2 - (k : ℤ) - (b : ℤ) + +/-! +Once the shared surface classes and boundary-component API exist, compile the library +statements rather than a quotient-of-presentations surrogate: + + theorem exists_standard_homeomorph ... + theorem standard_homeomorph_unique ... + theorem classification_of_surfaces ... : ∃! S : StandardSurface, ... + theorem homeomorph_iff_invariants ... + theorem exists_closed_minus_discs ... + +Uniqueness must use Euler characteristic, orientability, and boundary-component count; +the boundary count is topological only after `PlanarTopology` supplies two-dimensional +invariance of domain. +-/ + +/-! ## Follow-on layer 9: curves, cutting, and mapping class groups -/ + +/-! +This layer should consume the actual topological/PL isotopy and surface vocabulary rather +than prototype private replacements. Once those types exist, pin the full and +orientation-preserving mapping-class groups, relative-boundary base cases, Dehn twists, +the change-of-coordinates principle, and the torus computations. + +For the Dehn--Lickorish result, prefer two functional theorem targets rather than one +eponymous conjunction: + + -- All Dehn twists generate the positive mapping-class group. + theorem dehnTwist_closure_eq_top ... + + -- Lickorish's explicit `3g - 1` finite generating set. + theorem exists_dehnTwist_generatingSet_card_eq_three_mul_genus_sub_one ... + +The prose/docstrings should still call these the Dehn--Lickorish theorem. +-/ + +/-! ## Follow-on layer 10: planarity -/ + +/-! +This theorem suite waits on the verified common multigraph/embedding API from layer 5. +When that vocabulary is available, use descriptive Lean names and keep the historical +names in docstrings. The intended representative targets are: + + /-- Tutte's Wheel Theorem. -/ + theorem ... + + /-- Kuratowski's Theorem. -/ + theorem isPlanar_iff_no_K5_K33_topologicalMinor ... + + /-- Wagner's Theorem. -/ + theorem isPlanar_iff_no_K5_K33_minor ... + + /-- Tutte's Peripheral Cycle Theorem. -/ + theorem isPeripheral_iff_isFacial ... + + /-- Whitney's Unique Embedding Theorem. -/ + theorem planeEmbedding_unique_up_to_equivalence ... + + /-- Whitney's 2-Isomorphism Theorem. -/ + theorem cycleMatroid_iso_iff_twoIsomorphic ... + + def Graph.cycleSpace ... + def Graph.cutSpace ... + theorem cycleSpace_finrank ... + theorem cycleSpace_orthogonal_cutSpace ... + theorem planar_dual_cycleSpace_eq_cutSpace ... + + -- A 2-basis means that each edge occurs in at most two basis cycles. Pin the exact + -- finite-support expression against the eventual cycle-space representation. + def Graph.HasTwoBasis ... + + /-- Mac Lane's Planarity Criterion. -/ + theorem isPlanar_iff_hasTwoBasis ... + + /-- Fáry's Theorem. -/ + theorem exists_straightLine_planeEmbedding ... + + /-- Tutte's Spring Embedding Theorem. -/ + theorem exists_convex_planeEmbedding ... + + /-- The Five Colour Theorem. -/ + theorem colorable_five_of_isPlanar ... + +The exact wheel and Whitney-2-isomorphism signatures should be named only after their +statements are fully expanded; the README currently leaves the former schematic and the +latter as `...`, so this file should not pretend otherwise. +-/ + +end TauCetiRoadmap.SurfaceTopology