From f9efa4681dc0f2a8379ec37d815d4f6b78de8dd0 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 23 May 2026 15:26:41 +0000 Subject: [PATCH] =?UTF-8?q?feat:=20add=20generalized=20topological=20Poinc?= =?UTF-8?q?ar=C3=A9=20conjecture=20in=20dim=20=E2=89=A5=205=20(Smale)=20ev?= =?UTF-8?q?al=20problem?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds Smale's generalized topological Poincaré conjecture in dimensions n ≥ 5 as a new eval problem: every Hausdorff n-manifold homotopy-equivalent to 𝕊ⁿ is homeomorphic to 𝕊ⁿ. Specialization to n ≥ 5 of mathlib's generalized `proof_wanted`. Smale 1961 (Fields Medal 1966) for smooth M via the h-cobordism theorem; topological version completed by Newman 1966 and Connell 1967. Co-Authored-By: Claude Opus 4.7 (1M context) --- .../Topology/PoincareHighDimTopological.lean | 45 +++++++++++++++++++ .../poincare_high_dim_topological.toml | 9 ++++ 2 files changed, 54 insertions(+) create mode 100644 LeanEval/Topology/PoincareHighDimTopological.lean create mode 100644 manifests/problems/poincare_high_dim_topological.toml diff --git a/LeanEval/Topology/PoincareHighDimTopological.lean b/LeanEval/Topology/PoincareHighDimTopological.lean new file mode 100644 index 0000000..6e8c89f --- /dev/null +++ b/LeanEval/Topology/PoincareHighDimTopological.lean @@ -0,0 +1,45 @@ +import Mathlib +import EvalTools.Markers + +namespace LeanEval +namespace Topology + +/-! +# Generalized topological Poincaré conjecture in dimensions ≥ 5 (Smale) + +A specialization of mathlib's generalized `proof_wanted +ContinuousMap.HomotopyEquiv.nonempty_homeomorph_sphere` in +`Mathlib/Geometry/Manifold/PoincareConjecture.lean`, restricted to +dimension `n ≥ 5`: every Hausdorff `n`-manifold homotopy-equivalent to the +standard `n`-sphere `𝕊ⁿ` is homeomorphic to `𝕊ⁿ`. + +This is **Stephen Smale's 1961 theorem**, originally proved for `n ≥ 5` +assuming a smooth structure on `M` (via the `h`-cobordism theorem). The +**topological** version (no smoothness assumption) was completed by +Newman in 1966 and Connell in 1967. Smale received the Fields Medal in +1966. + +mathlib has homotopy equivalences (`≃ₕ`), homeomorphisms (`≃ₜ`), +`ChartedSpace`, and the unit sphere as a topological space — but no +`h`-cobordism theorem, no handle decompositions, and no Poincaré +conjecture in any dimension. +-/ + +open Metric (sphere) +open ContinuousMap + +/-- **Generalized topological Poincaré conjecture in dimensions ≥ 5** +(Smale 1961; topological case Newman 1966 / Connell 1967). For `n ≥ 5`, +every Hausdorff `n`-manifold homotopy-equivalent to the standard `n`-sphere +`𝕊ⁿ` is homeomorphic to `𝕊ⁿ`. -/ +@[eval_problem] +theorem poincare_high_dim_topological + {n : ℕ} (_h5 : 5 ≤ n) + {M : Type*} [TopologicalSpace M] [T2Space M] + [ChartedSpace (EuclideanSpace ℝ (Fin n)) M] + (_h : M ≃ₕ sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) : + Nonempty (M ≃ₜ sphere (0 : EuclideanSpace ℝ (Fin (n + 1))) 1) := by + sorry + +end Topology +end LeanEval diff --git a/manifests/problems/poincare_high_dim_topological.toml b/manifests/problems/poincare_high_dim_topological.toml new file mode 100644 index 0000000..c109188 --- /dev/null +++ b/manifests/problems/poincare_high_dim_topological.toml @@ -0,0 +1,9 @@ +id = "poincare_high_dim_topological" +title = "Generalized topological Poincaré conjecture in dimensions ≥ 5 (Smale)" +test = false +module = "LeanEval.Topology.PoincareHighDimTopological" +holes = ["poincare_high_dim_topological"] +submitter = "Kim Morrison" +notes = "For n ≥ 5, every Hausdorff n-manifold homotopy-equivalent to 𝕊ⁿ is homeomorphic to 𝕊ⁿ. Specialization to n ≥ 5 of mathlib's generalized `proof_wanted ContinuousMap.HomotopyEquiv.nonempty_homeomorph_sphere` in `Mathlib/Geometry/Manifold/PoincareConjecture.lean`. Stephen Smale 1961 (Bull. AMS 66, Ann. of Math. 74) originally for smooth M via the h-cobordism theorem; topological version completed by Newman 1966 and Connell 1967. Smale received the Fields Medal in 1966. Mathlib has the homotopy-equiv / homeo / ChartedSpace scaffolding but no h-cobordism theorem, no handle decompositions, and no Poincaré conjecture in any dimension." +source = "S. Smale, Generalized Poincaré's conjecture in dimensions greater than four, Ann. of Math. 74 (1961), 391-406. Topological case: M. H. A. Newman, The engulfing theorem for topological manifolds, Ann. of Math. 84 (1966) and E. H. Connell, A topological h-cobordism theorem for n ≥ 5, Illinois J. Math. 11 (1967). Specialization of `proof_wanted ContinuousMap.HomotopyEquiv.nonempty_homeomorph_sphere` in Mathlib/Geometry/Manifold/PoincareConjecture.lean." +informal_solution = "Smale's smooth proof: a smooth homotopy n-sphere M (n ≥ 5) bounds a smooth contractible (n+1)-manifold W via Whitehead's theorem and a Mayer-Vietoris computation; apply the h-cobordism theorem (Smale's main contribution) to W minus two small balls to conclude W ≃ D^{n+1}, hence M = ∂W ≃ S^n smoothly. The topological version (Newman/Connell) replaces the h-cobordism step with the topological engulfing theorem and a topological h-cobordism theorem, proving the same conclusion without the smoothness hypothesis. The dim ≥ 5 hypothesis is crucial: it allows the Whitney trick to remove pairs of intersections, which fails in dim 4 (requiring Casson handles, Freedman 1982) and below."