Casson–Harer: $L(m^2, mk-1)$ bounds a rational homology ball

Open

HomologySpheresBoundBalls.hsbb_casson_harer_lens

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

4-manifoldslens-spacestopology

Let $m, k$ be natural numbers with $0 < k < m$ and $\gcd(m,k) = 1$ . Then the lens space

L(m^2,\ mk-1)

bounds a compact smooth rational homology 4-ball.

This is the family of lens spaces in the title of Casson–Harer's paper; Lisca later classified all sums of lens spaces bounding rational balls.

Preamble

import Definitions.Def_hsbb_homology_balls
import Definitions.Def_hsbb_spaces

open scoped Manifold

Formal statement

namespace HomologySpheresBoundBalls

/-- (Casson–Harer) For coprime `0 < k < m`, the lens space `L(m², mk - 1)` bounds a smooth
rational homology 4-ball. -/
theorem hsbb_casson_harer_lens (m k : ℕ) (hk : 0 < k) (hkm : k < m) (hcop : Nat.Coprime m k) :
    BoundsRatHomologyBall (LensSpace (m ^ 2) (m * k - 1)) := 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

Casson–Harer: L(m2,mk−1)L(m^2, mk-1)L(m2,mk−1) bounds a rational homology ball

Casson–Harer: $L(m^2, mk-1)$ bounds a rational homology ball