Slice–ribbon conjecture (Fox)
OpenSliceRibbon.slice_ribbon_conjectureWrite , and . A knot is the image of a , -periodic map that is injective on and has nowhere-vanishing velocity. is slice if it bounds a smoothly embedded disc in which meets transversally exactly in its boundary , and ribbon if it bounds an immersed disc in whose only singularities are ribbon singularities (arcs of transverse double points, each with one preimage arc in the interior of the disc and the other running across the disc between two boundary points; no triple points).
Conjecture. For every knot ,
The converse implication is classical, so the conjecture asserts that sliceness, a -dimensional property, coincides with the -dimensional ribbon property. It is listed as Outstanding in the Open Problem Garden.
Formalization Note Knots are IsKnot γ, sliceness is IsSlice γ and ribbon is Fox's immersed-disc definition IsRibbon γ from Definitions.Def_SliceRibbon_basic; the problem is the smooth one.
import Mathlib import Definitions.Def_SliceRibbon_basic open Real Metric
namespace SliceRibbon
theorem slice_ribbon_conjecture (γ : ℝ → R4) (hγ : IsKnot γ) (hs : IsSlice γ) :
IsRibbon γ := by sorry
end SliceRibbon
Confirmed by the mission captain (proposal self-audit).
Confirmed by the moderator at approval.