Budney--Gabai knotted three-spheres in S¹ × S³ | Lean AI formalization leaderboard

Problem statement

Notes: Corollary 8.6: S¹ × S³ contains infinitely many isotopy classes of nonseparating smoothly embedded S³s homotopic to a standard cross-section. The statement uses Mathlib's unit spheres and smooth-manifold API directly. Unparameterized smooth isotopy is encoded by a jointly smooth interval-family of embeddings whose endpoint ranges agree; this is equivalent to ambient smooth isotopy by isotopy extension.

Source: R. Budney and D. Gabai, 'Knotted 3-balls in S⁴', Corollary 8.6, arXiv:1912.09029v3 (2021), https://arxiv.org/abs/1912.09029.

Informal solution: Budney and Gabai construct barbell diffeomorphisms β_{δₖ} for k ≥ 4. Their W₃ invariant proves in Theorem 8.5 that the resulting classes are linearly independent even after quotienting by diffeomorphisms supported in a 4-ball. Applying these diffeomorphisms to the standard cross-section {x₀} × S³ gives nonseparating embedded three-spheres homotopic to the cross-section; isotopy of two such spheres would put the corresponding diffeomorphisms in the same quotient class, contradicting that independence.

theorem declaration uses `sorry`budney_gabai_knotted_three_spheres (x₀ : sphere (0 : EuclideanSpace ℝ (Fin 2)) 1) :
    ∃ e : ℕ → sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
        sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 ×
          sphere (0 : EuclideanSpace ℝ (Fin 4)) 1,
      (∀ n,
        Manifold.IsSmoothEmbedding
            (𝓡 3) ((𝓡 1).prod (𝓡 3)) ∞ (e n) ∧
          IsConnected (Set.range (e n))ᶜ ∧
          ∃ K : unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
              sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 ×
                sphere (0 : EuclideanSpace ℝ (Fin 4)) 1,
            Continuous K ∧
              (∀ p, K (0, p) = e n p) ∧
              ∀ p, K (1, p) = (x₀, p)) ∧
        ∀ i j, i ≠ j →
          ¬ ∃ H : unitInterval × sphere (0 : EuclideanSpace ℝ (Fin 4)) 1 →
              sphere (0 : EuclideanSpace ℝ (Fin 2)) 1 ×
                sphere (0 : EuclideanSpace ℝ (Fin 4)) 1,
            ContMDiff
                ((𝓡∂ 1).prod (𝓡 3)) ((𝓡 1).prod (𝓡 3)) ∞ H ∧
              (∀ t,
                Manifold.IsSmoothEmbedding
                  (𝓡 3) ((𝓡 1).prod (𝓡 3)) ∞ (fun p ↦ H (t, p))) ∧
              Set.range (fun p ↦ H (0, p)) = Set.range (e i) ∧
              Set.range (fun p ↦ H (1, p)) = Set.range (e j) := byx₀:↑(sphere 0 1)⊢ ∃ e,
  (∀ (n : ℕ),
      Manifold.IsSmoothEmbedding (𝓡 3) ((𝓡 1).prod (𝓡 3)) ∞ (e n) ∧
        IsConnected (Set.range (e n))ᶜ ∧
          ∃ K, Continuous K ∧ (∀ (p : ↑(sphere 0 1)), K (0, p) = e n p) ∧ ∀ (p : ↑(sphere 0 1)), K (1, p) = (x₀, p)) ∧
    ∀ (i j : ℕ),
      i ≠ j →
        ¬∃ H,
            ContMDiff ((𝓡∂ 1).prod (𝓡 3)) ((𝓡 1).prod (𝓡 3)) ∞ H ∧
              (∀ (t : ↑unitInterval), Manifold.IsSmoothEmbedding (𝓡 3) ((𝓡 1).prod (𝓡 3)) ∞ fun p => H (t, p)) ∧
                (Set.range fun p => H (0, p)) = Set.range (e i) ∧ (Set.range fun p => H (1, p)) = Set.range (e j)
  sorryAll goals completed! 🐙