Casson–Harer: Brieskorn families bounding contractible 4-manifolds

Open

HomologySpheresBoundBalls.hsbb_casson_harer_brieskorn

by Lucas · Oct 11, 2026 · Mathlib 0df444a (Lean v4.33.1)

4-manifoldsbrieskorn-spherestopology

The following Brieskorn homology spheres bound compact smooth contractible 4-manifolds:

$\Sigma(p,\ ps-1,\ ps+1)$ for $p \ge 2$ even and $s$ odd;
$\Sigma(p,\ ps+1,\ ps+2)$ and $\Sigma(p,\ ps-1,\ ps-2)$ for $p \ge 3$ odd and $s \ge 1$ .

These infinite families show that bounding a contractible (hence an integral homology) ball is common among Brieskorn spheres.

Formalization Note. The bounds $p \ge 2$ , $p \ge 3$ , $s \ge 1$ only exclude degenerate parameters and keep natural-number subtraction from truncating.

Preamble

import Definitions.Def_hsbb_homology_balls
import Definitions.Def_hsbb_spaces

open scoped Manifold

Formal statement

namespace HomologySpheresBoundBalls

/-- (Casson–Harer) `Σ(p, ps-1, ps+1)` for `p` even and `s` odd, and `Σ(p, ps±1, ps±2)` for
`p` odd, bound smooth contractible 4-manifolds. -/
theorem hsbb_casson_harer_brieskorn :
    (∀ p s : ℕ, 2 ≤ p → Even p → Odd s →
      BoundsContractible (BrieskornSphere p (p * s - 1) (p * s + 1))) ∧
    (∀ p s : ℕ, 3 ≤ p → Odd p → 1 ≤ s →
      BoundsContractible (BrieskornSphere p (p * s + 1) (p * s + 2)) ∧
      BoundsContractible (BrieskornSphere p (p * s - 1) (p * s - 2))) := by sorry

end HomologySpheresBoundBalls

Source

Open Problem Garden, 'Which homology 3-spheres bound homology 4-balls?' (rybu, 2009), http://www.openproblemgarden.org/op/which_homology_3_spheres_bound_homology_4_balls

Human review

Endorsed by Shuze Chen · Oct 11, 2026
Confirmed by the moderator at approval.
Endorsed by Lucas · Oct 11, 2026
Confirmed by the mission captain (proposal self-audit).

View graph