feat: add Smale conjecture eval problem

LeanEval.lean

@@ -16,3 +16,4 @@ import LeanEval.NumberTheory.Lagarias
 import LeanEval.NumberTheory.SmallHouse
 import LeanEval.Topology.CerfGammaFour
 import LeanEval.Topology.HomotopyGroups
+import LeanEval.Topology.SmaleConjecture

LeanEval/Topology/SmaleConjecture.lean

@@ -0,0 +1,89 @@
+import Mathlib.Geometry.Manifold.Diffeomorph
+import Mathlib.Geometry.Manifold.Instances.Sphere
+import Mathlib.Geometry.Manifold.Instances.Real
+import Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
+import Mathlib.LinearAlgebra.UnitaryGroup
+import EvalTools.Markers
+
+namespace LeanEval
+namespace Topology
+
+open scoped Manifold ContDiff
+open Metric (sphere)
+
+/-!
+# Smale conjecture (Hatcher, 1983), relative parameterized form
+
+Hatcher's theorem says the inclusion `O(4) ↪ Diff(S³)` (restriction of the linear action
+on ℝ⁴) is a homotopy equivalence of topological spaces. Stating it in that form would
+require mathlib to carry the C^∞ topology on `Diffeomorph S³ S³`, which it does not yet
+have.
+
+We state the equivalent **relative parameterized** form: for every compact smooth
+manifold-with-boundary X and every smooth family of self-diffeomorphisms
+`F : X × S³ → S³` whose restriction to `∂X × S³` already comes from a continuous map
+`ψ_bdry : ∂X → O(4)` (acting by the linear action), there is a continuous extension
+`ψ : X → O(4)` with `ψ|∂X = ψ_bdry` and a smooth isotopy rel `∂X` from `F` to the
+family induced by `ψ`.
+
+For `X = D^k`, `∂X = S^{k-1}`, this says `π_k(Diff(S³), O(4)) = 0` for all `k ≥ 0`,
+which (modulo smoothing theory translating between smooth families parameterized by X
+and continuous maps `X → Diff(S³)` with the C^∞ topology) is equivalent to
+`O(4) ↪ Diff(S³)` being a homotopy equivalence.
+
+The Cerf case `X = pt` (so `∂X = ∅`, the relative hypothesis is vacuous) is
+Cerf's theorem Γ₄ = 0 (see `CerfGammaFour.lean`).
+
+**Desired future improvement.** Once mathlib gains a C^∞ topology on `Diffeomorph M N`
+(making it a topological group, with smooth families ↔ continuous maps into it), this
+statement should be rewritten in the direct form: the continuous group homomorphism
+`O(4) ↪ Diff(S³)` is a homotopy equivalence of topological spaces. Until then, the
+relative parameterized form below is the most faithful statement available.
+-/
+
+/-- **Smale conjecture (Hatcher 1983), relative parameterized form.**
+For every compact smooth manifold-with-boundary `X` and every smooth family `F` of
+self-diffeomorphisms of `S³` parameterized by `X` whose boundary restriction already
+factors through the linear action of `O(4)`, there is a smooth isotopy of `F`, rel
+`∂X`, to a family fully factoring through `O(4)`. -/
+@[eval_problem]
+theorem smale_conjecture
+    {n : ℕ} [NeZero n]
+    (X : Type) [TopologicalSpace X] [T2Space X] [SecondCountableTopology X]
+    [ChartedSpace (EuclideanHalfSpace n) X] [IsManifold (𝓡∂ n) ∞ X]
+    [CompactSpace X]
+    (F F' : X × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
+            sphere (0 : EuclideanSpace ℝ (Fin 4)) 1)
+    (hF  : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F)
+    (hF' : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F')
+    (hFinv₁ : ∀ x p, F  (x, F' (x, p)) = p)
+    (hFinv₂ : ∀ x p, F' (x, F  (x, p)) = p)
+    (ψ_bdry : (𝓡∂ n).boundary X → Matrix.orthogonalGroup (Fin 4) ℝ)
+    (hψ_bdry_cont : Continuous ψ_bdry)
+    (hF_bdry : ∀ (b : (𝓡∂ n).boundary X)
+                 (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              (F ((b : X), p) : EuclideanSpace ℝ (Fin 4)) =
+                Matrix.UnitaryGroup.toLinearEquiv (ψ_bdry b)
+                  (p : EuclideanSpace ℝ (Fin 4))) :
+    ∃ (ψ : X → Matrix.orthogonalGroup (Fin 4) ℝ)
+      (H H' : X × unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
+              sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+      Continuous ψ ∧
+      (∀ b : (𝓡∂ n).boundary X, ψ (b : X) = ψ_bdry b) ∧
+      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H ∧
+      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H' ∧
+      (∀ x t p, H  (x, t, H' (x, t, p)) = p) ∧
+      (∀ x t p, H' (x, t, H  (x, t, p)) = p) ∧
+      (∀ x p, H (x, 0, p) = F (x, p)) ∧
+      (∀ x (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              (H (x, 1, p) : EuclideanSpace ℝ (Fin 4)) =
+              Matrix.UnitaryGroup.toLinearEquiv (ψ x)
+                (p : EuclideanSpace ℝ (Fin 4))) ∧
+      (∀ (b : (𝓡∂ n).boundary X)
+         (t : unitInterval)
+         (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              H ((b : X), t, p) = F ((b : X), p)) := by
+  sorry
+
+end Topology
+end LeanEval

generated/index.json

@@ -151,5 +151,104 @@
     "module": "LeanEval.Topology.HomotopyGroups",
     "theorem": "pi_succ_sphere_n_mulEquiv_zmod_two",
     "generated_path": "generated/pi_succ_sphere_n_mulEquiv_zmod_two"
+  },
+  {
+    "id": "substInv_X_sub_X_sq_eq_catalan",
+    "title": "Catalan generating function via compositional inversion",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.Combinatorics.CatalanSubstInv",
+    "theorem": "substInv_X_sub_X_sq_eq_catalan",
+    "generated_path": "generated/substInv_X_sub_X_sq_eq_catalan"
+  },
+  {
+    "id": "isStarNormal_mul_of_commute",
+    "title": "Product of commuting normal elements is normal",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.Algebra.NormalProduct",
+    "theorem": "isStarNormal_mul_of_commute",
+    "generated_path": "generated/isStarNormal_mul_of_commute"
+  },
+  {
+    "id": "posSemidef_map_exp",
+    "title": "Entrywise exponential of a PSD matrix is PSD",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.LinearAlgebra.EntrywiseExpPSD",
+    "theorem": "posSemidef_map_exp",
+    "generated_path": "generated/posSemidef_map_exp"
+  },
+  {
+    "id": "mulCayley_connected_iff_closure_eq_top",
+    "title": "Cayley graph connected iff generators generate the group",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.Combinatorics.CayleyConnected",
+    "theorem": "mulCayley_connected_iff_closure_eq_top",
+    "generated_path": "generated/mulCayley_connected_iff_closure_eq_top"
+  },
+  {
+    "id": "oppenheim_inequality",
+    "title": "Oppenheim's inequality for Hadamard products",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.LinearAlgebra.Oppenheim",
+    "theorem": "oppenheim_inequality",
+    "generated_path": "generated/oppenheim_inequality"
+  },
+  {
+    "id": "symAction_range_eq_centralizer_glAction",
+    "title": "Schur-Weyl duality: S_k image equals centralizer of GL(V) image",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.RepresentationTheory.SchurWeyl",
+    "theorem": "symAction_range_eq_centralizer_glAction",
+    "generated_path": "generated/symAction_range_eq_centralizer_glAction"
+  },
+  {
+    "id": "glAction_range_eq_centralizer_symAction",
+    "title": "Schur-Weyl duality: GL(V) image equals centralizer of S_k image",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.RepresentationTheory.SchurWeyl",
+    "theorem": "glAction_range_eq_centralizer_symAction",
+    "generated_path": "generated/glAction_range_eq_centralizer_symAction"
+  },
+  {
+    "id": "g2_irrep_tensor_square_decomp",
+    "title": "Tensor square decomposition of a 64-dim irreducible g\u2082-representation",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.RepresentationTheory.ExceptionalLieTensorSquare",
+    "theorem": "g2_irrep_tensor_square_decomp",
+    "generated_path": "generated/g2_irrep_tensor_square_decomp"
+  },
+  {
+    "id": "e8_irrep_tensor_square_decomp",
+    "title": "Tensor square decomposition of a 779247-dim irreducible e\u2088-representation",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.RepresentationTheory.ExceptionalLieTensorSquare",
+    "theorem": "e8_irrep_tensor_square_decomp",
+    "generated_path": "generated/e8_irrep_tensor_square_decomp"
+  },
+  {
+    "id": "cerf_gamma_four",
+    "title": "Cerf's theorem: every self-diffeomorphism of S3 is smoothly isotopic to a linear isometry",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.Topology.CerfGammaFour",
+    "theorem": "cerf_gamma_four",
+    "generated_path": "generated/cerf_gamma_four"
+  },
+  {
+    "id": "smale_conjecture",
+    "title": "Smale conjecture (Hatcher) in relative parameterized form",
+    "test": false,
+    "submitter": "Kim Morrison",
+    "module": "LeanEval.Topology.SmaleConjecture",
+    "theorem": "smale_conjecture",
+    "generated_path": "generated/smale_conjecture"
   }
 ]

generated/pi1_circle_mulEquiv_int/lakefile.toml

@@ -8,7 +8,7 @@ autoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.30.0-rc1"
+rev = "50d5513e83c"
 
 [[lean_lib]]
 name = "Challenge"

generated/pi3_sphere_two_mulEquiv_int/lakefile.toml

@@ -8,7 +8,7 @@ autoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.30.0-rc1"
+rev = "50d5513e83c"
 
 [[lean_lib]]
 name = "Challenge"

generated/pi_succ_sphere_n_mulEquiv_zmod_two/lakefile.toml

@@ -8,7 +8,7 @@ autoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.30.0-rc1"
+rev = "50d5513e83c"
 
 [[lean_lib]]
 name = "Challenge"

generated/pin_sphere_n_mulEquiv_int/lakefile.toml

@@ -8,7 +8,7 @@ autoImplicit = false
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4.git"
-rev = "v4.30.0-rc1"
+rev = "50d5513e83c"
 
 [[lean_lib]]
 name = "Challenge"

generated/smale_conjecture/Challenge.lean

@@ -0,0 +1,41 @@
+import Mathlib
+
+open scoped Manifold ContDiff
+open Metric (sphere)
+
+theorem smale_conjecture {n : ℕ} [NeZero n]
+    (X : Type) [TopologicalSpace X] [T2Space X] [SecondCountableTopology X]
+    [ChartedSpace (EuclideanHalfSpace n) X] [IsManifold (𝓡∂ n) ∞ X]
+    [CompactSpace X]
+    (F F' : X × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
+            sphere (0 : EuclideanSpace ℝ (Fin 4)) 1)
+    (hF  : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F)
+    (hF' : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F')
+    (hFinv₁ : ∀ x p, F  (x, F' (x, p)) = p)
+    (hFinv₂ : ∀ x p, F' (x, F  (x, p)) = p)
+    (ψ_bdry : (𝓡∂ n).boundary X → Matrix.orthogonalGroup (Fin 4) ℝ)
+    (hψ_bdry_cont : Continuous ψ_bdry)
+    (hF_bdry : ∀ (b : (𝓡∂ n).boundary X)
+                 (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              (F ((b : X), p) : EuclideanSpace ℝ (Fin 4)) =
+                Matrix.UnitaryGroup.toLinearEquiv (ψ_bdry b)
+                  (p : EuclideanSpace ℝ (Fin 4))) :
+    ∃ (ψ : X → Matrix.orthogonalGroup (Fin 4) ℝ)
+      (H H' : X × unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
+              sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+      Continuous ψ ∧
+      (∀ b : (𝓡∂ n).boundary X, ψ (b : X) = ψ_bdry b) ∧
+      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H ∧
+      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H' ∧
+      (∀ x t p, H  (x, t, H' (x, t, p)) = p) ∧
+      (∀ x t p, H' (x, t, H  (x, t, p)) = p) ∧
+      (∀ x p, H (x, 0, p) = F (x, p)) ∧
+      (∀ x (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              (H (x, 1, p) : EuclideanSpace ℝ (Fin 4)) =
+              Matrix.UnitaryGroup.toLinearEquiv (ψ x)
+                (p : EuclideanSpace ℝ (Fin 4))) ∧
+      (∀ (b : (𝓡∂ n).boundary X)
+         (t : unitInterval)
+         (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              H ((b : X), t, p) = F ((b : X), p)) := by
+  sorry

generated/smale_conjecture/README.md

@@ -0,0 +1,25 @@
+# `smale_conjecture`
+
+Smale conjecture (Hatcher) in relative parameterized form
+
+- Problem ID: `smale_conjecture`
+- Test Problem: no
+- Submitter: Kim Morrison
+- Notes: Hatcher's 1983 theorem that Diff(S3) is homotopy equivalent to O(4), stated in the relative-parameterized-family form (families on a compact manifold-with-boundary X whose boundary already factors through O(4) deform rel boundary to a family fully factoring through O(4)). Mathlib does not yet carry the C-infinity topology on Diffeomorph, which would be needed for the direct homotopy-equivalence formulation.
+- Source: A. Hatcher, A proof of the Smale conjecture, Diff(S3) = O(4), Ann. of Math. 117 (1983).
+- Informal solution: Hatcher proves Diff(S3) is homotopy equivalent to O(4) by analyzing configurations of 2-spheres in S3 (the bigon criterion) and deducing by induction that every self-diffeomorphism is isotopic to a linear one, with all higher parameterized versions handled by the same incompressible-surface machinery.
+
+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/smale_conjecture/Solution.lean

@@ -0,0 +1,42 @@
+import Mathlib
+import Submission
+
+open scoped Manifold ContDiff
+open Metric (sphere)
+
+theorem smale_conjecture {n : ℕ} [NeZero n]
+    (X : Type) [TopologicalSpace X] [T2Space X] [SecondCountableTopology X]
+    [ChartedSpace (EuclideanHalfSpace n) X] [IsManifold (𝓡∂ n) ∞ X]
+    [CompactSpace X]
+    (F F' : X × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
+            sphere (0 : EuclideanSpace ℝ (Fin 4)) 1)
+    (hF  : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F)
+    (hF' : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F')
+    (hFinv₁ : ∀ x p, F  (x, F' (x, p)) = p)
+    (hFinv₂ : ∀ x p, F' (x, F  (x, p)) = p)
+    (ψ_bdry : (𝓡∂ n).boundary X → Matrix.orthogonalGroup (Fin 4) ℝ)
+    (hψ_bdry_cont : Continuous ψ_bdry)
+    (hF_bdry : ∀ (b : (𝓡∂ n).boundary X)
+                 (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              (F ((b : X), p) : EuclideanSpace ℝ (Fin 4)) =
+                Matrix.UnitaryGroup.toLinearEquiv (ψ_bdry b)
+                  (p : EuclideanSpace ℝ (Fin 4))) :
+    ∃ (ψ : X → Matrix.orthogonalGroup (Fin 4) ℝ)
+      (H H' : X × unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
+              sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+      Continuous ψ ∧
+      (∀ b : (𝓡∂ n).boundary X, ψ (b : X) = ψ_bdry b) ∧
+      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H ∧
+      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H' ∧
+      (∀ x t p, H  (x, t, H' (x, t, p)) = p) ∧
+      (∀ x t p, H' (x, t, H  (x, t, p)) = p) ∧
+      (∀ x p, H (x, 0, p) = F (x, p)) ∧
+      (∀ x (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              (H (x, 1, p) : EuclideanSpace ℝ (Fin 4)) =
+              Matrix.UnitaryGroup.toLinearEquiv (ψ x)
+                (p : EuclideanSpace ℝ (Fin 4))) ∧
+      (∀ (b : (𝓡∂ n).boundary X)
+         (t : unitInterval)
+         (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              H ((b : X), t, p) = F ((b : X), p)) := by
+  exact Submission.smale_conjecture X F F' hF hF' hFinv₁ hFinv₂ ψ_bdry hψ_bdry_cont hF_bdry

generated/smale_conjecture/Submission.lean

@@ -0,0 +1,46 @@
+import Mathlib
+import Submission.Helpers
+
+open scoped Manifold ContDiff
+open Metric (sphere)
+
+namespace Submission
+
+theorem smale_conjecture {n : ℕ} [NeZero n]
+    (X : Type) [TopologicalSpace X] [T2Space X] [SecondCountableTopology X]
+    [ChartedSpace (EuclideanHalfSpace n) X] [IsManifold (𝓡∂ n) ∞ X]
+    [CompactSpace X]
+    (F F' : X × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
+            sphere (0 : EuclideanSpace ℝ (Fin 4)) 1)
+    (hF  : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F)
+    (hF' : ContMDiff ((𝓡∂ n).prod (𝓡 3)) (𝓡 3) ∞ F')
+    (hFinv₁ : ∀ x p, F  (x, F' (x, p)) = p)
+    (hFinv₂ : ∀ x p, F' (x, F  (x, p)) = p)
+    (ψ_bdry : (𝓡∂ n).boundary X → Matrix.orthogonalGroup (Fin 4) ℝ)
+    (hψ_bdry_cont : Continuous ψ_bdry)
+    (hF_bdry : ∀ (b : (𝓡∂ n).boundary X)
+                 (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              (F ((b : X), p) : EuclideanSpace ℝ (Fin 4)) =
+                Matrix.UnitaryGroup.toLinearEquiv (ψ_bdry b)
+                  (p : EuclideanSpace ℝ (Fin 4))) :
+    ∃ (ψ : X → Matrix.orthogonalGroup (Fin 4) ℝ)
+      (H H' : X × unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
+              sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+      Continuous ψ ∧
+      (∀ b : (𝓡∂ n).boundary X, ψ (b : X) = ψ_bdry b) ∧
+      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H ∧
+      ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 3))) (𝓡 3) ∞ H' ∧
+      (∀ x t p, H  (x, t, H' (x, t, p)) = p) ∧
+      (∀ x t p, H' (x, t, H  (x, t, p)) = p) ∧
+      (∀ x p, H (x, 0, p) = F (x, p)) ∧
+      (∀ x (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              (H (x, 1, p) : EuclideanSpace ℝ (Fin 4)) =
+              Matrix.UnitaryGroup.toLinearEquiv (ψ x)
+                (p : EuclideanSpace ℝ (Fin 4))) ∧
+      (∀ (b : (𝓡∂ n).boundary X)
+         (t : unitInterval)
+         (p : sphere (0 : EuclideanSpace ℝ (Fin 4)) 1),
+              H ((b : X), t, p) = F ((b : X), p)) := by
+  sorry
+
+end Submission

generated/smale_conjecture/Submission/Helpers.lean

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