Smale conjecture (Hatcher) in relative parameterized form

smale_conjecture — a formalization challenge from the lean-eval benchmark.

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.

Formal statement

/-- **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)`. -/
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

Informal solution sketch

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.

Source

A. Hatcher, A proof of the Smale conjecture, Diff(S3) = O(4), Ann. of Math. 117 (1983).

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: smale_conjecture
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.