Smooth Euclidean extension of the inverse boundary chart

Proved

SPC4Disk.contDiff_boundaryInv

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

differentialgeometryexplicitdiskatlasmanifoldswithboundary

Let m be a nonnegative integer, p a point of the unit m-sphere, and k any differentiability order. Write u_p for the everywhere-defined inverse stereographic map used by the boundary chart centered in direction p. The Euclidean-coordinate map

y\longmapsto(1-y_0)u_p(y_1,\ldots,y_m)+2e_0

is C^k on all of Euclidean (m+1)-space. This is the unclamped extension of the boundary-to-interior transition formula, and is not a claim that the globally clamped chart inverse is everywhere smooth.

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.contDiff_boundaryInv
    (p : sphere (0 : EuclideanSpace ℝ (Fin (m + 1))) 1) {k : ℕ∞ω} :
    ContDiff ℝ k (fun y : EuclideanSpace ℝ (Fin (m + 1)) =>
      (1 - y 0) • 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 i => y i)))) :
            EuclideanSpace ℝ (Fin (m + 1))) + diskShift (m + 1)) := by sorry

Source

Unpublished archived Disk.lean, original lines 547–577; 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$ , let $L_p:(-p)^\perp\to\mathbb R^m$ be the coordinate isometry from the orthonormal basis selected by the construction and let $s=2e_0$ , twice the first standard basis vector. The function on all of $\mathbb R^{m+1}$ given, for $y=(a,t)\in\mathbb R\times\mathbb R^m$ , by $y\mapsto(1-a)\frac{4L_p^{-1}(t)+(4-\|t\|^2)p}{\|t\|^2+4}+s$ is of class $C^k$ as a map into $\mathbb R^{m+1}$ . Its denominator is strictly positive for every $t$ . The factor $1-a$ is not clipped: every real $a$ , including negative values, $a=1$ , and $a>1$ , is covered, and the codomain is the whole Euclidean space. The case $m=0$ is included, while $k=0$ , $\infty$ , and $\omega$ mean continuity, smoothness, and analyticity respectively.

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