The collar image is a neighborhood of every disk boundary point

Proved

SPC4Disk.range_diskCollar_mem_nhds

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

collarsdifferentialgeometryexplicitdiskatlasmanifoldswithboundary

For every nonnegative integer m and every point z of the closed unit ball D that lies in its manifold boundary for the explicit half-space atlas, the image of c(u,t)=(1−t/2)u belongs to the neighborhood filter of z in D. The neighborhood topology is the disk subtype topology, not the ambient Euclidean topology.

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_mem_nhds
    {z : closedBall (0 : EuclideanSpace ℝ (Fin (m + 1))) 1}
    (hz : z ∈ (𝓡∂ (m + 1)).boundary
      (closedBall (0 : EuclideanSpace ℝ (Fin (m + 1))) 1)) :
    Set.range (SPC4Disk.diskCollar (m := m)) ∈ nhds z := by sorry

Source

Ryan Shin, unpublished Disk.lean, original lines 1130–1155; 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. For every $z\in D$ assumed to lie in the manifold boundary for the specified disk half-space chart structure, namely satisfying $\|z\|=1$ , the range of $c:S^m\times[0,1]\to D$ , $c(u,t)=(1-t/2)u$ , is a neighborhood of $z$ in the subspace topology on $D$ . Explicitly, there exists a set $U$ open in $D$ such that $z\in U$ and $U\subseteq\{(1-t/2)u:u\in S^m,\ 0\leq t\leq1\}$ . This uses the closed interval of parameters, including both endpoints, and applies also to the boundary points of the one-dimensional disk when $m=0$ ; the neighborhood is relative to $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