The exact image of the radial disk collar

Proved

SPC4Disk.range_diskCollar

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

collarsdifferentialgeometryexplicitdiskatlasmanifoldswithboundary

For every nonnegative integer m, the image of c(u,t)=(1−t/2)u from the unit m-sphere times the closed interval [0,1] into the closed unit ball D is exactly the subset of D consisting of points of norm at least 1/2. Both radii 1/2 and 1 are included; the upper bound comes from membership in D.

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.range_diskCollar :
    Set.range (SPC4Disk.diskCollar (m := m)) =
      { z : closedBall (0 : EuclideanSpace ℝ (Fin (m + 1))) 1 |
        1 / 2 ≤ ‖z.val‖ } := by sorry

Source

Ryan Shin, unpublished Disk.lean, original lines 1081–1106; 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 range of the map $c:S^m\times[0,1]\to D$ defined by $c(u,t)=(1-t/2)u$ is exactly $\{z\in D:1/2\leq\|z\|\}$ . Thus, for each $z\in D$ , there exist $u\in E$ with $\|u\|=1$ and a real $t$ with $0\leq t\leq1$ such that $z=(1-t/2)u$ if and only if $1/2\leq\|z\|$ ; the upper bound $\|z\|\leq1$ comes from $z\in D$ . Both radii $1/2$ and $1$ are included, the origin is excluded, and the equality is of subsets of $D$ .

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