The explicit radial disk collar is a closed embedding

Proved

SPC4Disk.diskCollar_isClosedEmbedding

by ryanshin · Sep 6, 2026 · Mathlib 0df444a (Lean v4.33.1)

collarsdifferentialgeometryexplicitdiskatlasmanifoldswithboundary

For every nonnegative integer m, let D be the closed unit ball in real Euclidean (m+1)-space, S its unit sphere, and c : S × [0,1] → D the map c(u,t)=(1−t/2)u. Then c is a closed topological embedding. The interval includes both endpoints, and m=0 is included. This is the stated explicit disk map, not a collar theorem for arbitrary manifolds.

Preamble

import Mathlib
import Definitions.Def_SPC4DiskCharts
import Definitions.Def_SPC4DiskCollar

set_option autoImplicit false

open Set Metric SPC4Disk
open scoped ContDiff Manifold

noncomputable section
variable {m : ℕ}

local instance : Fact (Module.finrank ℝ (EuclideanSpace ℝ (Fin (m + 1))) = m + 1) :=
  ⟨finrank_euclideanSpace_fin⟩

Formal statement

theorem SPC4Disk.diskCollar_isClosedEmbedding :
    Topology.IsClosedEmbedding (SPC4Disk.diskCollar (m := m)) := by sorry

Source

Ryan Shin, unpublished Disk.lean, original lines 1074–1078; source SHA-256 889a9eccf9d2350aee7051ab7b6895e565f9f1a0c84e7120fb45c15acae0097e. Original declaration/proof ranges and reference edits come from the supplied Lean graph and sketch oracle; all four elaborated types (original, refactored, exact draft, solution) were compared.

Read-back

What the Lean code literally says, in plain math · Codex; the exact underlying model identifier is not exposed in this session.

For every natural number $m$ , including $m=0$ , let $E=\mathbb R^{m+1}$ with its Euclidean norm, $D=\{x\in E:\|x\|\leq1\}$ , and $S^m=\{u\in E:\|u\|=1\}$ , with their subspace topologies. The map $c:S^m\times[0,1]\to D$ , $c(u,t)=(1-t/2)u$ , where the domain has the product of the indicated subspace topologies, is a closed topological embedding: it is injective, identifies its domain homeomorphically with its image equipped with the topology inherited from $D$ , and that image is closed in $D$ . The entire closed interval of parameters is used, including $t=0$ and $t=1$ ; when $m=0$ the sphere is the two-point unit sphere in $\mathbb R$ .

Human review

Endorsed by Shuze Chen · Sep 6, 2026
Endorsed by ryanshin · Sep 6, 2026
Confirmed by the mission captain (proposal self-audit).

View graph