classifying compact connected 1-manifolds

A Lean 4 and mathlib proof of the classification of compact connected 1-manifolds with boundary:

Theorem (classification, in OneMfld/Classification.lean). Every compact, connected, Hausdorff topological space charted on ℝ≥0 is homeomorphic to the circle or to the closed unit interval.

noncomputable def classification [TopologicalSpace M] [ConnectedSpace M]
    [T2Space M] [CompactSpace M] (ht : ChartedSpace NNReal M) :
    (M ≃ₜ Circle) ⊕ (M ≃ₜ ↑UnitInterval)

#print axioms classification reports only [propext, Classical.choice, Quot.sound]

There are no sorrys in the repository.

Structure of the proof

Following Gale's "take-home exam" argument:

1. Normalization (NiceCharts, ClassifyInterval, IntervalCharts, FiniteIntervalCharts): every chart can be shrunk so its target is an open interval Ioo x y (interior chart) or Iio x (boundary chart) in ℝ≥0, and compactness yields a finite atlas of such charts.
2. Induction on atlas size (Classification): repeatedly merge two overlapping charts into one, or recognize the terminal cases.
3. The outer-overlap lemma (Outer): the image of any component of the overlap of two interval charts is an end-segment of the chart target — otherwise its closure would be trapped in the chart by a compactness argument, contradicting that it must escape into the other chart (ClosureOverlap).
4. End-matching (GlueCore, TwoComponents): the transition map on a component is strictly monotone in the direction forced by which interval-ends are interior; the wrong direction would give the overlap two distinct limit points at once, contradicting Hausdorffness.
5. Gluing (GlueNNReal, GlueUI, ClassifyOverlaps): two charts with connected overlap merge via OpenPartialHomeomorph.piecewise; two boundary charts glue onto the closed unit interval, exhibiting M ≃ₜ [0,1].
6. The circle (TwoComponents, CircleBlocks, CircleGlue): a disconnected overlap has exactly two components, one at each end of each chart; the two charts then embed as overlapping arcs of AddCircle 1 and glue to a chart of M onto the whole circle, exhibiting M ≃ₜ Circle.

Building

With elan installed:

lake exe cache get   # fetch mathlib build cache
lake build

The toolchain (lean-toolchain) and mathlib version (lake-manifest.json) are pinned.