The zero section of the radial collar is the boundary inclusion

Proved

SPC4Disk.diskCollar_zero

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

collarsdifferentialgeometryexplicitdiskatlasmanifoldswithboundary

For every nonnegative integer m and every point u of the unit m-sphere, evaluating the explicit collar at (u,0) equals the underlying disk point of the inverse image of u under SPC4Disk.diskBoundaryHomeoSphere. That homeomorphism identifies the boundary determined by the explicit disk charts with the unit sphere, without moving the ambient point. The assertion preserves the specific boundary-identification map, not merely the existence of some boundary parametrization.

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_zero (u : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) :
    SPC4Disk.diskCollar (u, ⟨0, by norm_num⟩) =
      ((SPC4Disk.diskBoundaryHomeoSphere (m := m)).symm u).val := by sorry

Source

Ryan Shin, unpublished Disk.lean, original lines 1120–1127; 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 $u\in S^m$ , the value at $(u,0)$ of $c:S^m\times[0,1]\to D$ , $c(u,t)=(1-t/2)u$ , equals the point of $D$ underlying the inverse image of $u$ under the specified boundary homeomorphism $\partial D\cong S^m$ . Here $\partial D$ is the boundary for the specified disk half-space chart structure, explicitly $\{z\in D:\|z\|=1\}$ , and that homeomorphism and its inverse preserve the underlying vector. The asserted equality is therefore $c(u,0)=u$ as an equality of points of $D$ , with the right-hand side obtained through the boundary inclusion; $0$ is the left endpoint of the allowed parameter interval.

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