feat: add Cerf's theorem Γ₄ = 0 eval problem

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

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

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

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.

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

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

generated/cerf_gamma_four/Submission/Helpers.lean

@@ -0,0 +1,3 @@
+namespace Submission.Helpers
+
+end Submission.Helpers

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

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
+}

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"

generated/cerf_gamma_four/lean-toolchain

@@ -0,0 +1,2 @@
+leanprover/lean4:v4.30.0-rc1
+

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."