Smooth transition from the translated interior chart to a boundary chart

Proved

SPC4Disk.contDiffOn_interiorToBoundaryFull

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

differentialgeometryexplicitdiskatlasmanifoldswithboundary

Let m be a nonnegative integer, p a unit-sphere direction, and k any differentiability order. After translating v by −2e₀, form its radial coordinate 1−‖v−2e₀‖ and its stereographic angular coordinates in the p-boundary chart. This Euclidean map is C^k where v−2e₀ is nonzero and the normalized vector has inner product different from 1 with −p.

The two exclusions are the origin and the stereographic pole. The statement concerns the explicit transition formula on this domain, not a global smoothness claim for normalization at the origin.

Preamble

import Mathlib
import Definitions.Def_SPC4DiskCharts

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.contDiffOn_interiorToBoundaryFull
    (p : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) {k : ℕ∞ω} :
    ContDiffOn ℝ k
      (fun v : EuclideanSpace ℝ (Fin (m + 1)) =>
        (WithLp.toLp 2 (Fin.cons (1 - ‖v - diskShift (m + 1)‖)
          (fun i => ((OrthonormalBasis.fromOrthogonalSpanSingleton m
              (ne_zero_of_mem_unit_sphere (-p))).repr
            (stereoToFun (((-p) : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) :
                EuclideanSpace ℝ (Fin (m + 1)))
              (‖v - diskShift (m + 1)‖⁻¹ • (v - diskShift (m + 1))))) i)) :
          EuclideanSpace ℝ (Fin (m + 1))))
      { v : EuclideanSpace ℝ (Fin (m + 1)) | v - diskShift (m + 1) ≠ 0 ∧
        innerSL ℝ (((-p) : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) :
          EuclideanSpace ℝ (Fin (m + 1)))
          (‖v - diskShift (m + 1)‖⁻¹ • (v - diskShift (m + 1))) ≠ (1 : ℝ) } := by sorry

Source

Unpublished archived Disk.lean, original lines 670–709; SHA-256 889a9eccf9d2350aee7051ab7b6895e565f9f1a0c84e7120fb45c15acae0097e. Declaration and proof ranges were extracted by the supplied Lean graph and sketch oracle.

Read-back

What the Lean code literally says, in plain math · Codex independent blind auditor; exact model identifier unavailable

For every natural number $m$ , every unit vector $p\in\mathbb R^{m+1}$ , and every differentiability order $k$ that is a nonnegative integer, $\infty$ , or $\omega$ , put $s=2e_0$ , where $e_0$ is the first standard basis vector. Let $L_p:(-p)^\perp\to\mathbb R^m$ be the coordinate isometry from the orthonormal basis selected by the construction, and define $S_p(u)=L_p\bigl(\frac{2}{1+\langle p,u\rangle}(u-\langle p,u\rangle p)\bigr)$ , with division by zero interpreted as zero. The ambient Euclidean-space map $v\mapsto\bigl(1-\|v-s\|,S_p((v-s)/\|v-s\|)\bigr)$ is of class $C^k$ on the set of all $v\in\mathbb R^{m+1}$ for which $v-s\ne0$ and $\langle-p,(v-s)/\|v-s\|\rangle\ne1$ . The normalizing reciprocal is also total, taking the value zero at a zero denominator, although that case is excluded from the stated set. No bound on $\|v-s\|$ and no half-space condition on $v$ is assumed. The case $m=0$ is included; $k=0$ asserts continuity, $k=\infty$ smoothness, and $k=\omega$ analyticity on the displayed set.

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