Watanabe's disproof of the 4-dimensional Smale conjecture

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

Notes

Resolves [Kir97, Problems 4.34 and 4.126] negatively: the 4-dimensional generalized Smale conjecture (O(5) ↪ Diff(S⁴) is a homotopy equivalence, equivalently Diff(D⁴ rel ∂) is contractible) is false. Watanabe showed πₖ(Diff(D⁴ rel ∂)) ⊗ ℚ ≠ 0 for many k, including k = 1, via configuration-space integrals. We state this as the negation of the exact four-dimensional analogue of the (true) S³ Smale conjecture in SmaleConjecture.lean — relative parameterized form, because Mathlib has no C^∞ topology on diffeomorphism groups yet.

Formal statement

/-- **Watanabe's theorem (2018): the 4-dimensional Smale conjecture is false**,
answering `[Kir97, Problems 4.34 and 4.126]`. The relative parameterized
statement that `O(5) ↪ Diff(S⁴)` is a homotopy equivalence — the exact
four-dimensional analogue of the (true) Smale conjecture for `S³` — does not
hold. -/
theorem watanabe_four_dim_smale_disproof :
    ¬ (∀ {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 5)) 1 →
                sphere (0 : EuclideanSpace ℝ (Fin 5)) 1),
        ContMDiff ((𝓡∂ n).prod (𝓡 4)) (𝓡 4) ∞ F →
        ContMDiff ((𝓡∂ n).prod (𝓡 4)) (𝓡 4) ∞ F' →
        (∀ x p, F  (x, F' (x, p)) = p) →
        (∀ x p, F' (x, F  (x, p)) = p) →
        ∀ (ψ_bdry : (𝓡∂ n).boundary X → Matrix.orthogonalGroup (Fin 5) ℝ),
        Continuous ψ_bdry →
        (∀ (b : (𝓡∂ n).boundary X)
           (p : sphere (0 : EuclideanSpace ℝ (Fin 5)) 1),
              (F ((b : X), p) : EuclideanSpace ℝ (Fin 5)) =
                Matrix.UnitaryGroup.toLinearEquiv (ψ_bdry b)
                  (p : EuclideanSpace ℝ (Fin 5))) →
        ∃ (ψ : X → Matrix.orthogonalGroup (Fin 5) ℝ)
          (H H' : X × unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 5)) 1 →
                  sphere (0 : EuclideanSpace ℝ (Fin 5)) 1),
          Continuous ψ ∧
          (∀ b : (𝓡∂ n).boundary X, ψ (b : X) = ψ_bdry b) ∧
          ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 4))) (𝓡 4) ∞ H ∧
          ContMDiff ((𝓡∂ n).prod ((𝓡∂ 1).prod (𝓡 4))) (𝓡 4) ∞ 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 5)) 1),
              (H (x, 1, p) : EuclideanSpace ℝ (Fin 5)) =
              Matrix.UnitaryGroup.toLinearEquiv (ψ x)
                (p : EuclideanSpace ℝ (Fin 5))) ∧
          (∀ (b : (𝓡∂ n).boundary X)
             (t : unitInterval)
             (p : sphere (0 : EuclideanSpace ℝ (Fin 5)) 1),
              H ((b : X), t, p) = F ((b : X), p))) := by
  sorry

Informal solution sketch

No formalization is feasible today: this needs the C^∞ topology on diffeomorphism groups, configuration-space integrals / Kontsevich classes, and the graph-cohomology machinery Watanabe uses. The statement is the negation of the parameterized homotopy-equivalence claim, which Watanabe's nontriviality result refutes.

Source

T. Watanabe, Some exotic nontrivial elements of the rational homotopy groups of Diff(S⁴), arXiv:1812.02448 (2018). Pairs with the positive S³ statement of Hatcher (Ann. of Math. 117, 1983) in SmaleConjecture.lean.

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: watanabe_four_dim_smale_disproof
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Kim Morrison.