Budney--Gabai knotted three-spheres in S¹ × S³
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) := x₀:↑(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)
All goals completed! 🐙