On a minimal disc in $\mathbb R^4$ the radial function has no interior local maximum

Proved

SliceRibbon.radialSq_not_isLocalMax_of_minimal

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

4-manifoldsknot-theoryslice-knotstopology

Let $F:\mathbb R^2\to\mathbb R^4$ be $C^\infty$ with injective differential $dF_z$ at every point of the open unit disc $\{\|z\|<1\}$ , and suppose $F$ is a minimal surface there (its mean curvature vector vanishes, in the sense of IsMinimalOnDisk). Then for every $z$ with $\|z\|<1$ , the squared radial function $r_F(w)=\|F(w)\|^2$ does not have a local maximum at $z$ :

\|z\|<1\ \Longrightarrow\ z \text{ is not a local maximum of } r_F.

This is the maximum-principle step in the minimal-surface approach to the slice–ribbon problem: on a minimal surface the Laplace–Beltrami operator of $\|x\|^2$ equals $4$ , so the radial function is strictly subharmonic.

Formalization Note Local maximum is IsLocalMax for $r_F$ as a function on $\mathbb R^2$ ; no boundary behaviour or embeddedness is assumed.

Preamble

import Mathlib
import Definitions.Def_SliceRibbon_basic

open Real Metric
open scoped ContDiff

Formal statement

namespace SliceRibbon

theorem radialSq_not_isLocalMax_of_minimal (F : R2 → R4) (hF : ContDiff ℝ ∞ F)
    (himm : ∀ z : R2, ‖z‖ < 1 → Function.Injective (fderiv ℝ F z))
    (hmin : IsMinimalOnDisk F) (z : R2) (hz : ‖z‖ < 1) :
    ¬ IsLocalMax (radialSq F) z := by sorry

end SliceRibbon

Source

Open Problem Garden, 'Slice-ribbon problem' (posted by rybu, Nov 7 2009), http://www.openproblemgarden.org/op/slice_ribbon_problem; supporting lemma for [H] J. Hass, The geometry of the slice-ribbon problem, Math. Proc. Cambridge Philos. Soc. 94 (1983) 101-108 (maximum principle for the radial function on a minimal surface).

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

On a minimal disc in R4\mathbb R^4R4 the radial function has no interior local maximum

On a minimal disc in $\mathbb R^4$ the radial function has no interior local maximum