Smooth transition between radial–stereographic boundary charts

Proved

SPC4Disk.contDiffOn_boundaryToBoundary

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

differentialgeometryexplicitdiskatlasmanifoldswithboundary

Let m be a nonnegative integer, p and p′ points of the unit m-sphere, and k any differentiability order. The change of boundary coordinates keeps the first, radial coordinate and applies the sphere’s stereographic change of angular coordinates to the remaining coordinates. Its Euclidean extension is C^k on the set where the inner product of −p′ with the inverse-stereographic unit vector from the p-chart is not 1.

The domain explicitly excludes the second projection’s pole. This is the analytic compatibility result used in the disk atlas assembly.

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_boundaryToBoundary
    (p p' : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) {k : ℕ∞ω} :
    ContDiffOn ℝ k
      (fun y : EuclideanSpace ℝ (Fin (m + 1)) =>
        (WithLp.toLp 2 (Fin.cons (y 0)
          (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)))
              (stereoInvFunAux (((-p) : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) :
                  EuclideanSpace ℝ (Fin (m + 1)))
                (((OrthonormalBasis.fromOrthogonalSpanSingleton m
                    (ne_zero_of_mem_unit_sphere (-p))).repr.symm
                  (WithLp.toLp 2 (Fin.tail (fun j => y j)))) :
                    EuclideanSpace ℝ (Fin (m + 1)))))) i)) :
          EuclideanSpace ℝ (Fin (m + 1))))
      { y : EuclideanSpace ℝ (Fin (m + 1)) |
        innerSL ℝ (((-p') : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) :
            EuclideanSpace ℝ (Fin (m + 1)))
          (stereoInvFunAux (((-p) : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) :
              EuclideanSpace ℝ (Fin (m + 1)))
            (((OrthonormalBasis.fromOrthogonalSpanSingleton m
                (ne_zero_of_mem_unit_sphere (-p))).repr.symm
              (WithLp.toLp 2 (Fin.tail (fun j => y j)))) :
                EuclideanSpace ℝ (Fin (m + 1)))) ≠ (1 : ℝ) } := by sorry

Source

Unpublished archived Disk.lean, original lines 603–668; 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 pair of unit vectors $p,p'\in\mathbb R^{m+1}$ , and every differentiability order $k$ that is a nonnegative integer, $\infty$ , or $\omega$ , let $L_p,L_{p'}$ be the coordinate isometries to $\mathbb R^m$ from the orthonormal bases selected by the construction for $(-p)^\perp$ and $(-p')^\perp$ . Put $U_p(t)=\frac{4L_p^{-1}(t)+(4-\|t\|^2)p}{\|t\|^2+4}$ and $S_{p'}(u)=L_{p'}\bigl(\frac{2}{1+\langle p',u\rangle}(u-\langle p',u\rangle p')\bigr)$ , assigning zero to division by zero. The map $(a,t)\mapsto(a,S_{p'}(U_p(t)))$ from $\mathbb R^{m+1}$ to itself is of class $C^k$ on the set $\{(a,t):\langle-p',U_p(t)\rangle\ne1\}$ . The inverse-stereographic denominator $\|t\|^2+4$ never vanishes, and the displayed set excludes the zero denominator in the forward-stereographic factor. There is no restriction on the real first coordinate $a$ , and $p=p'$ is allowed. The case $m=0$ and any resulting empty domain are included, with the regularity assertion vacuous on an empty domain; $k=0$ , $\infty$ , and $\omega$ denote continuity, smoothness, and analyticity.

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