From 83d522db88d0e36e99a92174a0688bf0becbc955 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 17 Apr 2026 16:07:37 +1000 Subject: [PATCH] =?UTF-8?q?feat:=20add=20Cerf's=20theorem=20=CE=93?= =?UTF-8?q?=E2=82=84=20=3D=200=20eval=20problem?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Cerf's 1968 theorem: every self-diffeomorphism of S³ is smoothly isotopic to the restriction of a linear isometry of ℝ⁴. Stated as the existence of a smooth isotopy [0,1] × S³ → S³ from f to a linear isometry, with smooth slice-inverse encoding the diffeomorphism property of each time-slice. Co-Authored-By: Claude Opus 4.6 (1M context) --- LeanEval.lean | 1 + LeanEval/Topology/CerfGammaFour.lean | 56 +++++++++++++++++++ generated/cerf_gamma_four/Challenge.lean | 19 +++++++ generated/cerf_gamma_four/README.md | 25 +++++++++ generated/cerf_gamma_four/Solution.lean | 20 +++++++ generated/cerf_gamma_four/Submission.lean | 24 ++++++++ .../cerf_gamma_four/Submission/Helpers.lean | 3 + generated/cerf_gamma_four/WorkspaceTest.lean | 38 +++++++++++++ generated/cerf_gamma_four/config.json | 13 +++++ generated/cerf_gamma_four/lakefile.toml | 24 ++++++++ generated/cerf_gamma_four/lean-toolchain | 2 + manifests/problems.toml | 11 ++++ 12 files changed, 236 insertions(+) create mode 100644 LeanEval/Topology/CerfGammaFour.lean create mode 100644 generated/cerf_gamma_four/Challenge.lean create mode 100644 generated/cerf_gamma_four/README.md create mode 100644 generated/cerf_gamma_four/Solution.lean create mode 100644 generated/cerf_gamma_four/Submission.lean create mode 100644 generated/cerf_gamma_four/Submission/Helpers.lean create mode 100644 generated/cerf_gamma_four/WorkspaceTest.lean create mode 100644 generated/cerf_gamma_four/config.json create mode 100644 generated/cerf_gamma_four/lakefile.toml create mode 100644 generated/cerf_gamma_four/lean-toolchain diff --git a/LeanEval.lean b/LeanEval.lean index d3fbe1e76..dc4a846e8 100644 --- a/LeanEval.lean +++ b/LeanEval.lean @@ -14,4 +14,5 @@ import LeanEval.LinearAlgebra.Oppenheim import LeanEval.LinearAlgebra.PerronFrobenius import LeanEval.NumberTheory.Lagarias import LeanEval.NumberTheory.SmallHouse +import LeanEval.Topology.CerfGammaFour import LeanEval.Topology.HomotopyGroups diff --git a/LeanEval/Topology/CerfGammaFour.lean b/LeanEval/Topology/CerfGammaFour.lean new file mode 100644 index 000000000..54e373104 --- /dev/null +++ b/LeanEval/Topology/CerfGammaFour.lean @@ -0,0 +1,56 @@ +import Mathlib.Geometry.Manifold.Diffeomorph +import Mathlib.Geometry.Manifold.Instances.Sphere +import Mathlib.Geometry.Manifold.Instances.Real +import Mathlib.LinearAlgebra.UnitaryGroup +import EvalTools.Markers + +namespace LeanEval +namespace Topology + +open scoped Manifold ContDiff +open Metric (sphere) + +/-! +# Cerf's theorem Γ₄ = 0 (1968) + +Cerf's theorem states that every self-diffeomorphism of the standard 3-sphere is +smoothly isotopic to the restriction of a linear isometry of ℝ⁴ — equivalently, +the inclusion `O(4) ↪ Diff(S³)` (acting by restriction of the linear action on ℝ⁴) is +surjective on π₀. The classical name `Γ₄ = 0` refers to Cerf's group of pseudo-isotopies +in dimension 4 (originally formulated as the obstruction to extending self-diffeomorphisms +of S³ across D⁴). + +This is the unparameterized (X = point) case of the Smale conjecture (Hatcher 1983, see +`SmaleConjecture.lean`). It is historically and technically distinct from the full Smale +conjecture: Cerf's original proof predates Hatcher's by 15 years and uses pseudo-isotopy +theory rather than the bigon / 2-sphere configuration analysis Hatcher employs. + +We state isotopy as a smooth map `[0, 1] × S³ → S³` whose every time slice is a +diffeomorphism, witnessed by an explicit smooth slice-inverse `F'`. Smoothness of `F` +and `F'` together with the pointwise-inverse identities forces each time-slice +`p ↦ F(t, p)` to be a diffeomorphism (its slice-inverse `p ↦ F'(t, p)` is smooth as a +composition with the smooth inclusion `p ↦ (t, p)`). This avoids the need for a topology +on `Diffeomorph S³ S³` (which mathlib does not yet have). +-/ + +/-- **Cerf's theorem Γ₄ = 0.** Every self-diffeomorphism of S³ is smoothly isotopic to +the restriction of a linear isometry of ℝ⁴. -/ +@[eval_problem] +theorem cerf_gamma_four + (f : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 ≃ₘ⟮𝓡 3, 𝓡 3⟯ + sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) : + ∃ (A : Matrix.orthogonalGroup (Fin 4) ℝ) + (F F' : unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 → + sphere (0 : EuclideanSpace ℝ (Fin 4)) 1), + ContMDiff ((𝓡∂ 1).prod (𝓡 3)) (𝓡 3) ∞ F ∧ + ContMDiff ((𝓡∂ 1).prod (𝓡 3)) (𝓡 3) ∞ F' ∧ + (∀ t p, F (t, F' (t, p)) = p) ∧ + (∀ t p, F' (t, F (t, p)) = p) ∧ + (∀ p, F (0, p) = f p) ∧ + (∀ p, (F (1, p) : EuclideanSpace ℝ (Fin 4)) = + Matrix.UnitaryGroup.toLinearEquiv A + (p : EuclideanSpace ℝ (Fin 4))) := by + sorry + +end Topology +end LeanEval diff --git a/generated/cerf_gamma_four/Challenge.lean b/generated/cerf_gamma_four/Challenge.lean new file mode 100644 index 000000000..c9c27327d --- /dev/null +++ b/generated/cerf_gamma_four/Challenge.lean @@ -0,0 +1,19 @@ +import Mathlib + +open scoped Manifold ContDiff +open Metric (sphere) + +theorem cerf_gamma_four (f : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 ≃ₘ⟮𝓡 3, 𝓡 3⟯ + sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) : + ∃ (A : Matrix.orthogonalGroup (Fin 4) ℝ) + (F F' : unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 → + sphere (0 : EuclideanSpace ℝ (Fin 4)) 1), + ContMDiff ((𝓡∂ 1).prod (𝓡 3)) (𝓡 3) ∞ F ∧ + ContMDiff ((𝓡∂ 1).prod (𝓡 3)) (𝓡 3) ∞ F' ∧ + (∀ t p, F (t, F' (t, p)) = p) ∧ + (∀ t p, F' (t, F (t, p)) = p) ∧ + (∀ p, F (0, p) = f p) ∧ + (∀ p, (F (1, p) : EuclideanSpace ℝ (Fin 4)) = + Matrix.UnitaryGroup.toLinearEquiv A + (p : EuclideanSpace ℝ (Fin 4))) := by + sorry diff --git a/generated/cerf_gamma_four/README.md b/generated/cerf_gamma_four/README.md new file mode 100644 index 000000000..e224a7f75 --- /dev/null +++ b/generated/cerf_gamma_four/README.md @@ -0,0 +1,25 @@ +# `cerf_gamma_four` + +Cerf's theorem: every self-diffeomorphism of S3 is smoothly isotopic to a linear isometry + +- Problem ID: `cerf_gamma_four` +- Test Problem: no +- Submitter: Kim Morrison +- Notes: Cerf's 1968 theorem, the X = point (unparameterized) case of the Smale conjecture. Stated as the existence of a smooth isotopy [0,1] x S3 -> S3 from f to a linear isometry, witnessed by a smooth slice-inverse to encode the diffeomorphism property of each slice without needing a topology on Diffeomorph. +- Source: J. Cerf, Sur les diffeomorphismes de la sphere de dimension trois, Lecture Notes in Mathematics 53, Springer (1968). +- Informal solution: Cerf's original proof uses pseudo-isotopy theory: a self-diffeomorphism of S3 extends to a pseudo-isotopy of D4, and Cerf's theorem on the triviality of pi_0 of the pseudo-isotopy space in dimension 4 implies the extension is isotopic to a genuine isotopy. Hatcher (1983) reproved this as a corollary of the full Smale conjecture using configurations of 2-spheres. + +Do not modify `Challenge.lean` or `Solution.lean`. Those files are part of the +trusted benchmark and fixed by the repository. + +Write your solution in `Submission.lean` and any additional local modules under +`Submission/`. + +Participants may use Mathlib freely. Any helper code not already available in +Mathlib must be inlined into the submission workspace. + +Multi-file submissions are allowed through `Submission.lean` and additional local +modules under `Submission/`. + +`lake test` runs comparator for this problem. The command expects a comparator +binary in `PATH`, or in the `COMPARATOR_BIN` environment variable. diff --git a/generated/cerf_gamma_four/Solution.lean b/generated/cerf_gamma_four/Solution.lean new file mode 100644 index 000000000..bccce186a --- /dev/null +++ b/generated/cerf_gamma_four/Solution.lean @@ -0,0 +1,20 @@ +import Mathlib +import Submission + +open scoped Manifold ContDiff +open Metric (sphere) + +theorem cerf_gamma_four (f : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 ≃ₘ⟮𝓡 3, 𝓡 3⟯ + sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) : + ∃ (A : Matrix.orthogonalGroup (Fin 4) ℝ) + (F F' : unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 → + sphere (0 : EuclideanSpace ℝ (Fin 4)) 1), + ContMDiff ((𝓡∂ 1).prod (𝓡 3)) (𝓡 3) ∞ F ∧ + ContMDiff ((𝓡∂ 1).prod (𝓡 3)) (𝓡 3) ∞ F' ∧ + (∀ t p, F (t, F' (t, p)) = p) ∧ + (∀ t p, F' (t, F (t, p)) = p) ∧ + (∀ p, F (0, p) = f p) ∧ + (∀ p, (F (1, p) : EuclideanSpace ℝ (Fin 4)) = + Matrix.UnitaryGroup.toLinearEquiv A + (p : EuclideanSpace ℝ (Fin 4))) := by + exact Submission.cerf_gamma_four f diff --git a/generated/cerf_gamma_four/Submission.lean b/generated/cerf_gamma_four/Submission.lean new file mode 100644 index 000000000..ef74503b1 --- /dev/null +++ b/generated/cerf_gamma_four/Submission.lean @@ -0,0 +1,24 @@ +import Mathlib +import Submission.Helpers + +open scoped Manifold ContDiff +open Metric (sphere) + +namespace Submission + +theorem cerf_gamma_four (f : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 ≃ₘ⟮𝓡 3, 𝓡 3⟯ + sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) : + ∃ (A : Matrix.orthogonalGroup (Fin 4) ℝ) + (F F' : unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 → + sphere (0 : EuclideanSpace ℝ (Fin 4)) 1), + ContMDiff ((𝓡∂ 1).prod (𝓡 3)) (𝓡 3) ∞ F ∧ + ContMDiff ((𝓡∂ 1).prod (𝓡 3)) (𝓡 3) ∞ F' ∧ + (∀ t p, F (t, F' (t, p)) = p) ∧ + (∀ t p, F' (t, F (t, p)) = p) ∧ + (∀ p, F (0, p) = f p) ∧ + (∀ p, (F (1, p) : EuclideanSpace ℝ (Fin 4)) = + Matrix.UnitaryGroup.toLinearEquiv A + (p : EuclideanSpace ℝ (Fin 4))) := by + sorry + +end Submission diff --git a/generated/cerf_gamma_four/Submission/Helpers.lean b/generated/cerf_gamma_four/Submission/Helpers.lean new file mode 100644 index 000000000..1561e7c8a --- /dev/null +++ b/generated/cerf_gamma_four/Submission/Helpers.lean @@ -0,0 +1,3 @@ +namespace Submission.Helpers + +end Submission.Helpers diff --git a/generated/cerf_gamma_four/WorkspaceTest.lean b/generated/cerf_gamma_four/WorkspaceTest.lean new file mode 100644 index 000000000..ecb65777d --- /dev/null +++ b/generated/cerf_gamma_four/WorkspaceTest.lean @@ -0,0 +1,38 @@ +import Lean + +open Lean + +def comparatorExists (comparatorBin : String) : IO Bool := do + if comparatorBin.contains '/' then + return (← System.FilePath.pathExists comparatorBin) + try + let child ← IO.Process.spawn { + cmd := "sh" + args := #["-c", "command -v \"$1\" >/dev/null 2>&1", "sh", comparatorBin] + } + let exitCode ← child.wait + return exitCode == 0 + catch _ => + return false + +def main : IO UInt32 := do + let comparatorBin := (← IO.getEnv "COMPARATOR_BIN").getD "comparator" + if !(← comparatorExists comparatorBin) then + IO.eprintln s!"Failed to run comparator via `{comparatorBin}`." + IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`." + IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export." + pure 1 + else + try + let child ← IO.Process.spawn { + cmd := "lake" + args := #["env", comparatorBin, "config.json"] + } + let exitCode ← child.wait + pure exitCode + catch err => + IO.eprintln s!"Failed to run comparator via `{comparatorBin}`." + IO.eprintln "Make sure `comparator` is installed and on your `PATH`, or set `COMPARATOR_BIN=/path/to/comparator`." + IO.eprintln "See the root repository README for comparator setup details, including landrun and lean4export." + IO.eprintln s!"Original error: {err}" + pure 1 diff --git a/generated/cerf_gamma_four/config.json b/generated/cerf_gamma_four/config.json new file mode 100644 index 000000000..acd4ba42e --- /dev/null +++ b/generated/cerf_gamma_four/config.json @@ -0,0 +1,13 @@ +{ + "challenge_module": "Challenge", + "solution_module": "Solution", + "theorem_names": [ + "cerf_gamma_four" + ], + "permitted_axioms": [ + "propext", + "Quot.sound", + "Classical.choice" + ], + "enable_nanoda": false +} diff --git a/generated/cerf_gamma_four/lakefile.toml b/generated/cerf_gamma_four/lakefile.toml new file mode 100644 index 000000000..8ec5e4abf --- /dev/null +++ b/generated/cerf_gamma_four/lakefile.toml @@ -0,0 +1,24 @@ +name = "cerf_gamma_four" +testDriver = "workspace_test" +defaultTargets = ["Challenge", "Solution", "Submission"] + +[leanOptions] +autoImplicit = false + +[[require]] +name = "mathlib" +git = "https://github.com/leanprover-community/mathlib4.git" +rev = "50d5513e83c" + +[[lean_lib]] +name = "Challenge" + +[[lean_lib]] +name = "Solution" + +[[lean_lib]] +name = "Submission" + +[[lean_exe]] +name = "workspace_test" +root = "WorkspaceTest" diff --git a/generated/cerf_gamma_four/lean-toolchain b/generated/cerf_gamma_four/lean-toolchain new file mode 100644 index 000000000..e7e267fe4 --- /dev/null +++ b/generated/cerf_gamma_four/lean-toolchain @@ -0,0 +1,2 @@ +leanprover/lean4:v4.30.0-rc1 + diff --git a/manifests/problems.toml b/manifests/problems.toml index 4b0f68da2..6f1056815 100644 --- a/manifests/problems.toml +++ b/manifests/problems.toml @@ -285,3 +285,14 @@ submitter = "Kim Morrison" notes = "e₈ is the largest exceptional Lie algebra (dim 248), defined here by the Serre construction (Mathlib's `LieAlgebra.e₈`). The relevant irreducible representation has highest weight ω₁ + ω₈ (the sum of the first and last fundamental weights, in Bourbaki labelling), dimension 779247; its tensor square decomposes into 40 isomorphism classes of irreducible Lie submodules. The U(g)-module structure on V ⊗ V used in the statement comes from lifting the Lie action via the universal enveloping algebra." source = "Classical: representation theory of the exceptional Lie algebra e₈." informal_solution = "Construct V as V(ω₁+ω₈), the unique 779247-dim irrep of e₈. Tensor square (LiE-verified) has 40 distinct simple summand isomorphism classes (155 components with multiplicity), with the smallest being the trivial 1-dim, the 248-dim adjoint (mult 2), the 3875-dim V(ω₁), and so on up to the 85,424,220,000-dim summand." + +[[problem]] +id = "cerf_gamma_four" +title = "Cerf's theorem: every self-diffeomorphism of S3 is smoothly isotopic to a linear isometry" +test = false +module = "LeanEval.Topology.CerfGammaFour" +theorem = "cerf_gamma_four" +submitter = "Kim Morrison" +notes = "Cerf's 1968 theorem, the X = point (unparameterized) case of the Smale conjecture. Stated as the existence of a smooth isotopy [0,1] x S3 -> S3 from f to a linear isometry, witnessed by a smooth slice-inverse to encode the diffeomorphism property of each slice without needing a topology on Diffeomorph." +source = "J. Cerf, Sur les diffeomorphismes de la sphere de dimension trois, Lecture Notes in Mathematics 53, Springer (1968)." +informal_solution = "Cerf's original proof uses pseudo-isotopy theory: a self-diffeomorphism of S3 extends to a pseudo-isotopy of D4, and Cerf's theorem on the triviality of pi_0 of the pseudo-isotopy space in dimension 4 implies the extension is isotopic to a genuine isotopy. Hatcher (1983) reproved this as a corollary of the full Smale conjecture using configurations of 2-spheres."