$P \# (-P)$ bounds a smooth integral homology ball

Open

HomologySpheresBoundBalls.hsbb_poincare_double_bounds

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

4-manifoldstopology

Equip the Poincaré homology sphere $P = \Sigma(2,3,5)$ with any atlas modelled on $\mathbb R^3$ (compatible with its topology). Let $x \in P$ , $r > 0$ , and let $\varphi$ be the chart at $x$ , with the closed ball $\overline{B}(\varphi x, r)$ contained in the chart's target. Let $B = \varphi^{-1}(B(\varphi x, r))$ . Then the double

D(P \setminus B) \;\cong\; P \# (-P)

bounds a smooth integral homology 4-ball.

This shows that the obstruction in the previous milestone does not survive connected sum with the orientation reverse, illustrating that bounding is a group-theoretic question in homology cobordism.

Preamble

import Definitions.Def_hsbb_homology_balls
import Definitions.Def_hsbb_spaces

open scoped Manifold

Formal statement

namespace HomologySpheresBoundBalls

/-- `P # (-P)`, realized as the double of `P` minus an open chart ball, bounds a smooth
integral homology 4-ball (namely `(P ∖ B) × [0,1]`). -/
theorem hsbb_poincare_double_bounds [ChartedSpace (EuclideanSpace ℝ (Fin 3)) PoincareSphere]
    (x : PoincareSphere) (r : ℝ) (hr : 0 < r)
    (hball : Metric.closedBall (chartAt (EuclideanSpace ℝ (Fin 3)) x x) r ⊆
      (chartAt (EuclideanSpace ℝ (Fin 3)) x).target) :
    BoundsIntHomologyBall (PuncturedDouble x r) := 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

P#(−P)P \# (-P)P#(−P) bounds a smooth integral homology ball

$P \# (-P)$ bounds a smooth integral homology ball